awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a : α
ha : ¬(↑a : WithTop α) = 0
neg :
  ∀ (hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0), untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
⊢ untopD 0 ((↑a : WithTop α) * b) = untopD 0 (↑a : WithTop α) * untopD 0 b
have neg₁ : ∀ (a_1 : α) (hb : ¬(↑a_1 : WithTop α) = 0),
  untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
Tactic: cases b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
⊢ untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
have neg : untopD 0 ⊤ = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
Tactic: rw [mul_top ha, untopD_top, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
neg : untopD 0 ⊤ = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
⊢ untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
have neg₁ : 0 = untopD 0 (↑a : WithTop α) * 0
Tactic: rw [mul_top ha, untopD_top, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
neg : untopD 0 ⊤ = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
neg₁ : 0 = untopD 0 (↑a : WithTop α) * 0
⊢ untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
have neg₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [mul_top ha, untopD_top, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
a_1 : α
hb : ¬(↑a_1 : WithTop α) = 0
⊢ untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
have neg : untopD 0 (↑(a * a_1) : WithTop α) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
Tactic: rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
a_1 : α
hb : ¬(↑a_1 : WithTop α) = 0
neg : untopD 0 (↑(a * a_1) : WithTop α) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
⊢ untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
have neg₁ : a * a_1 = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
Tactic: rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
a_1 : α
hb : ¬(↑a_1 : WithTop α) = 0
neg : untopD 0 (↑(a * a_1) : WithTop α) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
neg₁ : a * a_1 = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
⊢ untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
have neg₂ : a * a_1 = a * untopD 0 (↑a_1 : WithTop α)
Tactic: rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithTop α) = 0
a_1 : α
hb : ¬(↑a_1 : WithTop α) = 0
neg : untopD 0 (↑(a * a_1) : WithTop α) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
neg₁ : a * a_1 = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
neg₂ : a * a_1 = a * untopD 0 (↑a_1 : WithTop α)
⊢ untopD 0 ((↑a : WithTop α) * (↑a_1 : WithTop α)) = untopD 0 (↑a : WithTop α) * untopD 0 (↑a_1 : WithTop α)
have neg₃ : a * a_1 = a * a_1
Tactic: rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : LT α
a b : WithTop α
ha : a < ⊤
hb : b < ⊤
⊢ a * b < ⊤
have rw : ∀ (ha : a ≠ ⊤) (hb : b ≠ ⊤), a * b ≠ ⊤
Tactic: rw [WithTop.lt_top_iff_ne_top] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
⊢ NoZeroDivisors.{u_1} (WithTop α)
have refine : ∀ {a b : WithTop α} (h₁ : a * b = 0) (h₂ : ¬(a = 0 ∨ b = 0)), False
Tactic: refine ⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
a_1 b_1 : WithTop α
h₁ : a_1 * b_1 = 0
h₂ : ¬(a_1 = 0 ∨ b_1 = 0)
⊢ False
have h₃ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) a_1 b_1) 0
Tactic: rw [mul_def, if_neg h₂] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
inst_2 : NoZeroDivisors α
a_1 b_1 : WithTop α
h₁ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) a_1 b_1) 0
h₂ : ¬(a_1 = 0 ∨ b_1 = 0)
⊢ False
have rcases : ∀ (a b : α) (hab : a * b = 0)
  (h₁ : Eq (α := WithTop α) (map₂ (fun (x1 x2 : α) ↦ x1 * x2) (Option.some a) (Option.some b)) 0)
  (h₂ : ¬(Option.some a = 0 ∨ Option.some b = 0)), False
Tactic: rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩
Cleared hypotheses: a_1, b_1, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ StrictMono (β := WithTop α) fun (x : WithTop α) ↦ a * x
have lift : ∀ (a : α) (h₀ : 0 < (↑a : WithTop α)), StrictMono (β := WithTop α) fun (x : WithTop α) ↦ (↑a : WithTop α) * x
Tactic: lift a to α using hinf
Cleared hypotheses: a, h₀, hinf
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
b c : WithTop α
hbc : b < c
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) b)
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) c)
have lift : ∀ (b : α) (hbc : (↑b : WithTop α) < c),
  LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) c)
Tactic: lift b to α using hbc.ne_top
Cleared hypotheses: b, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c_1 : WithTop α
b c : α
hbc : (↑b : WithTop α) < (↑c : WithTop α)
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ (↑a : WithTop α) * x) (↑c : WithTop α))
have simp : ∀ (h₀ : 0 < a) (hbc : b < c), a * b < a * c
Tactic: simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
Cleared hypotheses: h₀, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ StrictMono (β := WithTop α) fun (x : WithTop α) ↦ x * a
have lift : ∀ (a : α) (h₀ : 0 < (↑a : WithTop α)), StrictMono (β := WithTop α) fun (x : WithTop α) ↦ x * (↑a : WithTop α)
Tactic: lift a to α using hinf
Cleared hypotheses: a, h₀, hinf
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
b c : WithTop α
hbc : b < c
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) b)
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) c)
have lift : ∀ (b : α) (hbc : (↑b : WithTop α) < c),
  LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) c)
Tactic: lift b to α using hbc.ne_top
Cleared hypotheses: b, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : α
h₀ : 0 < (↑a : WithTop α)
c_1 : WithTop α
b c : α
hbc : (↑b : WithTop α) < (↑c : WithTop α)
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑b : WithTop α))
    ((fun (x : WithTop α) ↦ x * (↑a : WithTop α)) (↑c : WithTop α))
have simp : ∀ (h₀ : 0 < a) (hbc : b < c), b * a < c * a
Tactic: simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
Cleared hypotheses: h₀, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
⊢ 1 * (↑a : WithTop α) = (↑a : WithTop α)
have rw : (↑1 : WithTop α) * (↑a : WithTop α) = (↑a : WithTop α)
Tactic: rw [← coe_one, ← coe_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
rw : (↑1 : WithTop α) * (↑a : WithTop α) = (↑a : WithTop α)
⊢ 1 * (↑a : WithTop α) = (↑a : WithTop α)
have rw₁ : (↑(1 * a) : WithTop α) = (↑a : WithTop α)
Tactic: rw [← coe_one, ← coe_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
rw : (↑1 : WithTop α) * (↑a : WithTop α) = (↑a : WithTop α)
rw₁ : (↑(1 * a) : WithTop α) = (↑a : WithTop α)
⊢ 1 * (↑a : WithTop α) = (↑a : WithTop α)
have rw₂ : (↑a : WithTop α) = (↑a : WithTop α)
Tactic: rw [← coe_one, ← coe_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
⊢ (↑a : WithTop α) * 1 = (↑a : WithTop α)
have rw : (↑a : WithTop α) * (↑1 : WithTop α) = (↑a : WithTop α)
Tactic: rw [← coe_one, ← coe_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
rw : (↑a : WithTop α) * (↑1 : WithTop α) = (↑a : WithTop α)
⊢ (↑a : WithTop α) * 1 = (↑a : WithTop α)
have rw₁ : (↑(a * 1) : WithTop α) = (↑a : WithTop α)
Tactic: rw [← coe_one, ← coe_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
a : α
rw : (↑a : WithTop α) * (↑1 : WithTop α) = (↑a : WithTop α)
rw₁ : (↑(a * 1) : WithTop α) = (↑a : WithTop α)
⊢ (↑a : WithTop α) * 1 = (↑a : WithTop α)
have rw₂ : (↑a : WithTop α) = (↑a : WithTop α)
Tactic: rw [← coe_one, ← coe_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
have 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)
Tactic: rcases Decidable.eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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)
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
have 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)
Tactic: rcases Decidable.eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
have 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)
Tactic: rcases Decidable.eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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)
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
have 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)
Tactic: rcases Decidable.eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ map (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := WithTop S) (map (⇑f : (a : R) → S) x) (map (⇑f : (a : R) → S) y)
have 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)
Tactic: cases x with | top => simp [hy, this] | coe x => ?_
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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
⊢ 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) ⊤)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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)
have 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) ⊤)
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]
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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) ⊤)
⊢ 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)
have 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))
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]
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
⊢ a * b * c = a * (b * c)
have inl : 0 * b * c = 0 * (b * c)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
inl : 0 * b * c = 0 * (b * c)
⊢ a * b * c = a * (b * c)
have inr : ∀ (ha : a ≠ 0), a * b * c = a * (b * c)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
⊢ a * b * c = a * (b * c)
have inr : a * 0 * c = a * (0 * c)
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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)
⊢ a * b * c = a * (b * c)
have inr₁ : ∀ (hb : b ≠ 0), a * b * c = a * (b * c)
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * c = a * (b * c)
have inr : a * b * 0 = a * (b * 0)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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)
⊢ a * b * c = a * (b * c)
have inr₁ : ∀ (hc : c ≠ 0), a * b * c = a * (b * c)
Tactic: rcases eq_or_ne c 0 with (rfl | hc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ a * b * c = a * (b * c)
have inr : ∀ (a : α) (ha : (↑a : WithTop α) ≠ 0), (↑a : WithTop α) * b * c = (↑a : WithTop α) * (b * c)
Tactic: cases a with | top => simp [hb, hc] | coe a => ?_
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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)
have inr : ∀ (b : α) (hb : (↑b : WithTop α) ≠ 0),
  (↑a : WithTop α) * (↑b : WithTop α) * c = (↑a : WithTop α) * ((↑b : WithTop α) * c)
Tactic: cases b with | top => simp [mul_top ha, top_mul hc] | coe b => ?_
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = (↑a : WithTop α) * ((↑b : WithTop α) * ⊤)
have inr : (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤
Tactic: rw [mul_top hb, mul_top ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤
have inr : ∀ (ha : ¬a = 0) (b : α) (hb : ¬b = 0) (hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0),
  (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = ⊤
Tactic: rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
Cleared hypotheses: ha, b, hb, hc