[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h : p
⊢ 0 < if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h : ¬p
⊢ 0 < if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h : p
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h : ¬p
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : p
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : ¬p
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ min a b ≠ c
[PROOFSTEP]
rw [min_def]
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then a else b) ≠ c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : a ≤ b
⊢ a ≠ c
[PROOFSTEP]
assumption
[GOAL]
case neg
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : ¬a ≤ b
⊢ b ≠ c
[PROOFSTEP]
assumption
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ max a b ≠ c
[PROOFSTEP]
rw [max_def]
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then b else a) ≠ c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : a ≤ b
⊢ b ≠ c
[PROOFSTEP]
assumption
[GOAL]
case neg
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : ¬a ≤ b
⊢ a ≠ c
[PROOFSTEP]
assumption
[GOAL]
a : ℤ
ha : 0 < a
⊢ 0 < a / a
[PROOFSTEP]
{rw [Int.ediv_self ha.ne']; exact zero_lt_one
}
[GOAL]
a : ℤ
ha : 0 < a
⊢ 0 < a / a
[PROOFSTEP]
rw [Int.ediv_self ha.ne']
[GOAL]
a : ℤ
ha : 0 < a
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
n : ℕ
x✝ : PUnit
m : Q(ℕ)
this✝ : «$b» =Q bit0 «$m»
_a : Q(LinearOrderedRing «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q StrictOrderedRing.toPartialOrder
⊢ Strictness zα pα e
[PROOFSTEP]
exact .nonnegative q(pow_bit0_nonneg $a $m)
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
result : Strictness zα pα e
ra : Strictness zα pα a
pa : Q(0 ≤ «$a»)
_oα : Q(OrderedSemiring «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q OrderedSemiring.toPartialOrder
⊢ Strictness zα pα e
[PROOFSTEP]
exact .nonnegative (q(pow_nonneg $pa $b))
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
result : Strictness zα pα e
ra : Strictness zα pα a
ofNonneg : Q(0 ≤ «$a») → Q(OrderedSemiring «$α») → MetaM (Strictness zα pα e) :=
  fun pa _oα =>
    let_fun zα_eq := (_ : «$zα» =Q MonoidWithZero.toZero);
    let_fun pα_eq := (_ : «$pα» =Q OrderedSemiring.toPartialOrder);
    pure (Strictness.nonnegative q((_ : 0 ≤ «$a» ^ «$b»)))
pa : Q(«$a» ≠ 0)
_oα : Q(OrderedSemiring «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q OrderedSemiring.toPartialOrder
_a : Q(NoZeroDivisors «$α»)
⊢ Q(«$e» ≠ 0)
[PROOFSTEP]
exact q(pow_ne_zero $b $pa)
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
result : Strictness zα pα e
ra : Strictness zα pα a
ofNonneg : Q(0 ≤ «$a») → Q(OrderedSemiring «$α») → MetaM (Strictness zα pα e) :=
  fun pa _oα =>
    let_fun zα_eq := (_ : «$zα» =Q MonoidWithZero.toZero);
    let_fun pα_eq := (_ : «$pα» =Q OrderedSemiring.toPartialOrder);
    pure (Strictness.nonnegative q((_ : 0 ≤ «$a» ^ «$b»)))
ofNonzero : Q(«$a» ≠ 0) → Q(OrderedSemiring «$α») → MetaM (Strictness zα pα e) :=
  fun pa _oα =>
    let_fun zα_eq := (_ : «$zα» =Q MonoidWithZero.toZero);
    let_fun pα_eq := (_ : «$pα» =Q OrderedSemiring.toPartialOrder);
    do
    let _a ← synthInstanceQ q(NoZeroDivisors «$α»)
    pure (Strictness.nonzero q((_ : «$a» ^ «$b» ≠ 0)))
pa : Q(0 < «$a»)
_a : Q(StrictOrderedSemiring «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q StrictOrderedSemiring.toPartialOrder
⊢ Strictness zα pα e
[PROOFSTEP]
exact .positive (q(pow_pos $pa $b))
