awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : WithTop R
⊢ ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0

Tactic:
have : ∀ z, map f z = 0 ↔ z = 0 := fun z =>
        (Option.map_injective hf).eq_iff' f.toZeroHom.withTopMap.map_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
inl :
  map (⇑f : (a : R) → S) (0 * y) =
    HMul.hMul (α := WithTop S) (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) 0) (map (⇑f : (a : R) → S) y)
inr :
  ∀ (hx : x ≠ 0),
    map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)

Tactic:
rcases Decidable.eq_or_ne x 0 with (rfl | hx)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
⊢ map (⇑f : (a : R) → S) (0 * y) =
    HMul.hMul (α := WithTop S) (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) 0) (map (⇑f : (a : R) → S) y)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
hx : x ≠ 0
inr :
  map (⇑f : (a : R) → S) (x * 0) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) 0)
inr₁ :
  ∀ (hy : y ≠ 0),
    map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)

Tactic:
rcases Decidable.eq_or_ne y 0 with (rfl | hy)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f : (a : R) → S) (x * 0) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
hy : y ≠ 0
hx : Ne.{u_2 + 1} (α := WithTop R) ⊤ 0
⊢ map (⇑f : (a : R) → S) (⊤ * y) =
    HMul.hMul (α := WithTop S) (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) ⊤) (map (⇑f : (a : R) → S) y)

Tactic:
simp [hy, this]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
hy : y ≠ 0
x : R
hx : (↑x : WithTop R) ≠ 0
⊢ map (⇑f : (a : R) → S) ((↑x : WithTop R) * y) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R)) (map (⇑f : (a : R) → S) y)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
inr :
  ∀ (x : R) (hx : (↑x : WithTop R) ≠ 0),
    map (⇑f : (a : R) → S) ((↑x : WithTop R) * y) =
      HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R)) (map (⇑f : (a : R) → S) y)
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)

Tactic:
cases x with | top => simp [hy, this] | coe x => ?_

Premises used: WithTop.top, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
x : R
hx : (↑x : WithTop R) ≠ 0
hy : Ne.{u_2 + 1} (α := WithTop R) ⊤ 0
⊢ Ne.{u_3 + 1} (α := WithTop S) ((↑((f : (a : R) → S) x) : WithTop S) : WithTop S) (0 : WithTop S)

Tactic:
simpa [hf.eq_iff' (map_zero f)] using hx

Premises used: map_zero, Function.Injective.eq_iff'
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
x : R
hx : (↑x : WithTop R) ≠ 0
hy : Ne.{u_2 + 1} (α := WithTop R) ⊤ 0
⊢ Ne.{u_3 + 1} (α := WithTop S) ((↑((f : (a : R) → S) x) : WithTop S) : WithTop S) (0 : WithTop S)

Tactic:
have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
x : R
hx : (↑x : WithTop R) ≠ 0
hy : Ne.{u_2 + 1} (α := WithTop R) ⊤ 0
this : Ne.{u_3 + 1} (α := WithTop S) ((↑((f : (a : R) → S) x) : WithTop S) : WithTop S) (0 : WithTop S)
⊢ map (⇑f : (a : R) → S) ((↑x : WithTop R) * ⊤) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R)) (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) ⊤)

Tactic:
simp [mul_top hx, mul_top this]

Premises used: WithTop.mul_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
x : R
hx : (↑x : WithTop R) ≠ 0
y : R
hy : (↑y : WithTop R) ≠ 0
⊢ map (⇑f : (a : R) → S) ((↑x : WithTop R) * (↑y : WithTop R)) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R)) (map (⇑f : (a : R) → S) (↑y : WithTop R))

Tactic:
simp [← coe_mul]

Premises used: WithTop.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
R : Type u_2
S : Type u_3
inst_1 : MulZeroOneClass R
inst_2 : DecidableEq R
inst_3 : Nontrivial R
inst_4 : MulZeroOneClass S
inst_5 : DecidableEq S
inst_6 : Nontrivial S
f : R →*₀ S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : WithTop R
this : ∀ (z : WithTop R), Eq.{u_3 + 1} (α := WithTop S) (map (⇑f : (a : R) → S) z) 0 ↔ z = 0
hy : y ≠ 0
x : R
hx : (↑x : WithTop R) ≠ 0
inr :
  ∀ (hy : Ne.{u_2 + 1} (α := WithTop R) ⊤ 0),
    map (⇑f : (a : R) → S) ((↑x : WithTop R) * ⊤) =
      HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R))
        (map.{u_2, u_3} (α := R) (⇑f : (a : R) → S) ⊤)
inr₁ :
  ∀ (y : R) (hy : (↑y : WithTop R) ≠ 0),
    map (⇑f : (a : R) → S) ((↑x : WithTop R) * (↑y : WithTop R)) =
      HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R)) (map (⇑f : (a : R) → S) (↑y : WithTop R))
⊢ map (⇑f : (a : R) → S) ((↑x : WithTop R) * y) =
    HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) (↑x : WithTop R)) (map (⇑f : (a : R) → S) y)

Tactic:
cases y with
      | top =>
        have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
        simp [mul_top hx, mul_top this]
      | coe y => simp [← coe_mul]

Premises used: WithTop.mul_top, WithTop.top, WithTop.coe_mul, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
inl : 0 * b * c = 0 * (b * c)
inr : ∀ (ha : a ≠ 0), a * b * c = a * (b * c)
⊢ a * b * c = a * (b * c)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)

Tactic:
simp only [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
inr : a * 0 * c = a * (0 * c)
inr₁ : ∀ (hb : b ≠ 0), a * b * c = a * (b * c)
⊢ a * b * c = a * (b * c)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a c : WithTop α
ha : a ≠ 0
⊢ a * 0 * c = a * (0 * c)

Tactic:
simp only [zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
inr : a * b * 0 = a * (b * 0)
inr₁ : ∀ (hc : c ≠ 0), a * b * c = a * (b * c)
⊢ a * b * c = a * (b * c)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)

Tactic:
simp only [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
ha : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0
⊢ ⊤ * b * c = ⊤ * (b * c)

Tactic:
simp [hb, hc]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
⊢ (↑a : WithTop α) * b * c = (↑a : WithTop α) * (b * c)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
inr : ∀ (a : α) (ha : (↑a : WithTop α) ≠ 0), (↑a : WithTop α) * b * c = (↑a : WithTop α) * (b * c)
⊢ a * b * c = a * (b * c)

Tactic:
cases a with | top => simp [hb, hc] | coe a => ?_

Premises used: WithTop.top, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
hb : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0
⊢ (↑a : WithTop α) * ⊤ * c = (↑a : WithTop α) * (⊤ * c)

Tactic:
simp [mul_top ha, top_mul hc]

Premises used: WithTop.top_mul, WithTop.mul_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
⊢ (↑a : WithTop α) * (↑b : WithTop α) * c = (↑a : WithTop α) * ((↑b : WithTop α) * c)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
inr :
  ∀ (b : α) (hb : (↑b : WithTop α) ≠ 0),
    (↑a : WithTop α) * (↑b : WithTop α) * c = (↑a : WithTop α) * ((↑b : WithTop α) * c)
⊢ (↑a : WithTop α) * b * c = (↑a : WithTop α) * (b * c)

Tactic:
cases b with | top => simp [mul_top ha, top_mul hc] | coe b => ?_

Premises used: WithTop.top_mul, WithTop.mul_top, WithTop.top, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0
inr : (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤
⊢ (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = (↑a : WithTop α) * ((↑b : WithTop α) * ⊤)

Tactic:
rw [mul_top hb, mul_top ha]

Premises used: WithTop.mul_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0
inr :
  ∀ (ha : ¬a = 0) (b : α) (hb : ¬b = 0) (hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0),
    (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤
⊢ (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤

Tactic:
rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb

Premises used: WithTop.coe_zero, ne_eq, WithTop.coe_eq_coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a : α
ha : ¬a = 0
b : α
hb : ¬b = 0
hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0
⊢ (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤

Tactic:
simp [ha, hb]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
c : α
hc : (↑c : WithTop α) ≠ 0
⊢ (↑a : WithTop α) * (↑b : WithTop α) * (↑c : WithTop α) = (↑a : WithTop α) * ((↑b : WithTop α) * (↑c : WithTop α))

Tactic:
simp only [← coe_mul, mul_assoc]

Premises used: mul_assoc, WithTop.coe_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
inr :
  ∀ (hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0),
    (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = (↑a : WithTop α) * ((↑b : WithTop α) * ⊤)
inr₁ :
  ∀ (c : α) (hc : (↑c : WithTop α) ≠ 0),
    (↑a : WithTop α) * (↑b : WithTop α) * (↑c : WithTop α) = (↑a : WithTop α) * ((↑b : WithTop α) * (↑c : WithTop α))
⊢ (↑a : WithTop α) * (↑b : WithTop α) * c = (↑a : WithTop α) * ((↑b : WithTop α) * c)

Tactic:
cases c with
    | top =>
      rw [mul_top hb, mul_top ha]
      rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
      simp [ha, hb]
    | coe c => simp only [← coe_mul, mul_assoc]

Premises used: WithTop.mul_top, mul_assoc, WithTop.coe_zero, ne_eq, WithTop.coe_eq_coe, WithTop.top, WithTop.coe_mul, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
top :
  Eq.{u_1 + 1} (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)
coe :
  ∀ (a : α),
    Eq (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (1 : WithTop α)
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
⊢ Eq.{u_1 + 1} (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : α
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n_1 n : ℕ
a : WithTop α
zero :
  (match (motive := WithTop α → ℕ → WithTop α) a, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
succ :
  ∀ (n : ℕ),
    (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 + 1 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤) =
      HMul.hMul (α := WithTop α)
        (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
          | Option.some a, n => (↑(a ^ n) : WithTop α)
          | none, 0 => 1
          | none, _n.succ => ⊤ :
          WithTop α)
        a
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
zero :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
zero₁ :
  ∀ (a : α),
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), HAdd.hAdd (α := ℕ) 0 1 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤) =
      HMul.hMul (α := WithTop α)
        (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
          | Option.some a, n => (↑(a ^ n) : WithTop α)
          | none, 0 => 1
          | none, _n.succ => ⊤ :
          WithTop α)
        (↑a : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n_1 : ℕ
succ :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, n_1 + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n_1 + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
succ₁ :
  ∀ (a : α),
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n_1 + 1 + 1 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤) =
      HMul.hMul (α := WithTop α)
        (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n_1 + 1 with
          | Option.some a, n => (↑(a ^ n) : WithTop α)
          | none, 0 => 1
          | none, _n.succ => ⊤ :
          WithTop α)
        (↑a : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n_1 + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n_1 + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)

Tactic:
simp [pow_succ]

Premises used: pow_succ