awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ IsUnit a
have this : a ^ m * a ∣ a ^ m * 1
Tactic: have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ IsUnit a
have mp : a ^ m ≠ 0
Tactic: rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
⊢ m ∣ n ↔ m = 0 → n = 0
have refine_1 : m ∣ n → ∀ (hm : m = 0) (a : α) (ha : n = m * a), n = 0
Tactic: refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
refine_1 : m ∣ n → ∀ (hm : m = 0) (a : α) (ha : n = m * a), n = 0
⊢ m ∣ n ↔ m = 0 → n = 0
have refine_2 : ∀ (h : m = 0 → n = 0), m ∣ n
Tactic: refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n
have refine_2 : n = m * (m⁻¹ * n)
Tactic: refine ⟨m⁻¹ * n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ n = m * (m⁻¹ * n)
have refine_2 : ∀ (h : m = 0 → Eq.{u_1 + 1} (α := α) 0 0), 0 = m * (m⁻¹ * 0)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
refine_2 : ∀ (h : m = 0 → Eq.{u_1 + 1} (α := α) 0 0), 0 = m * (m⁻¹ * 0)
⊢ n = m * (m⁻¹ * n)
have refine_2₁ : ∀ (hn : n ≠ 0), n = m * (m⁻¹ * n)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)
have refine_2 : n = n
Tactic: rw [mul_inv_cancel_left₀ (mt h hn)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
neZero : NeZero.{u_3} (R := β) ((f : (a : α) → β) a : β)
h : a = 0
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (0 : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : FunLike F α β
inst_3 : ZeroHomClass F α β
a : α
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : NeZero a
⊢ Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (0 : β)
have rw : Ne.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 0 : β)
Tactic: rw [← ZeroHomClass.map_zero f]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
f g : α →*₀ β
h : Eq (α := (a : α) → β) ((fun (f : α →*₀ β) ↦ f.toFun) f) ((fun (f : α →*₀ β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_zero' : toFun 0 = 0)
  (map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1)
  (map_mul' :
    ∀ (x y : α),
      { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
          { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →*₀ β) ↦ f.toFun)
        { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' })
      ((fun (f : α →*₀ β) ↦ f.toFun) g)),
  { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
g : α →*₀ β
toFun : α → β
map_zero' : toFun 0 = 0
map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun 1 = 1
map_mul' :
  ∀ (x y : α),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun (x * y) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun x *
        { toFun := toFun, map_zero' := map_zero' : ZeroHom α β }.toFun y
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →*₀ β) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : α →*₀ β) ↦ f.toFun) g)
⊢ { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } = g
have obtain : ∀ (toFun_1 : α → β) (map_zero'_1 : toFun_1 0 = 0)
  (map_one'_1 : { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun 1 = 1)
  (map_mul'_1 :
    ∀ (x y : α),
      { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun (x * y) =
        { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun x *
          { toFun := toFun_1, map_zero' := map_zero'_1 : ZeroHom α β }.toFun y)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →*₀ β) ↦ f.toFun)
        { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' })
      ((fun (f : α →*₀ β) ↦ f.toFun)
        { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
  { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : α →*₀ β } =
    { toFun := toFun_1, map_zero' := map_zero'_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
F : Type u_7
inst_2 : FunLike F α β
inst_3 : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst_4 : Decidable p
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (if p then 0 else 1) : β) (if p then 0 else 1 : β)
have pos : ∀ (h : p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
F : Type u_7
inst_2 : FunLike F α β
inst_3 : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst_4 : Decidable p
pos : ∀ (h : p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (if p then 0 else 1) : β) (if p then 0 else 1 : β)
have neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
F : Type u_7
inst_2 : FunLike F α β
inst_3 : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst_4 : Decidable p
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (if p then 1 else 0) : β) (if p then 1 else 0 : β)
have pos : ∀ (h : p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
F : Type u_7
inst_2 : FunLike F α β
inst_3 : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst_4 : Decidable p
pos : ∀ (h : p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (if p then 1 else 0) : β) (if p then 1 else 0 : β)
have neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) 0) 0
have rw : Eq.{u_4 + 1} (α := γ) ((hnp : (a : β) → γ) ((hmn : (a : α) → β) 0 : β) : γ) (0 : γ)
Tactic: rw [comp_apply, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
rw : Eq.{u_4 + 1} (α := γ) ((hnp : (a : β) → γ) ((hmn : (a : α) → β) 0 : β) : γ) (0 : γ)
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) 0) 0
have rw₁ : Eq.{u_4 + 1} (α := γ) ((hnp : (a : β) → γ) 0 : γ) (0 : γ)
Tactic: rw [comp_apply, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
hnp : β →*₀ γ
hmn : α →*₀ β
rw : Eq.{u_4 + 1} (α := γ) ((hnp : (a : β) → γ) ((hmn : (a : α) → β) 0 : β) : γ) (0 : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((hnp : (a : β) → γ) 0 : γ) (0 : γ)
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) 0) 0
have rw₂ : Eq.{u_4 + 1} (α := γ) 0 0
Tactic: rw [comp_apply, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h,
    comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h,
    comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h,
    comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β_1
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β_1
β : Type u_7
inst_5 : CommMonoidWithZero β
f g : α →*₀ β
⊢ (↑(HMul.hMul (α := α →* β) (↑f : α →* β) (↑g : α →* β)) : OneHom α β).toFun 0 = 0
have dsimp : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((g : (a : α) → β) 0 : β) = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β_1
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β_1
β : Type u_7
inst_5 : CommMonoidWithZero β
f g : α →*₀ β
⊢ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((g : (a : α) → β) 0 : β) = 0
have rw : HMul.hMul (α := β) (β := β) (0 : β) ((g : (a : α) → β) 0 : β) = 0
Tactic: rw [map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β_1
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β_1
β : Type u_7
inst_5 : CommMonoidWithZero β
f g : α →*₀ β
rw : HMul.hMul (α := β) (β := β) (0 : β) ((g : (a : α) → β) 0 : β) = 0
⊢ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((g : (a : α) → β) 0 : β) = 0
have rw₁ : Eq.{u_7 + 1} (α := β) 0 0
Tactic: rw [map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 1 0
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 1 0
neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 1 1
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have pos₂ : ¬x * y = 0 → x = 0 → y = 0 → 1 = HMul.hMul (α := N₀) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 1 0
neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 1 1
pos₂ : ¬x * y = 0 → x = 0 → y = 0 → 1 = HMul.hMul (α := N₀) 0 0
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have neg₂ : ¬x * y = 0 → x = 0 → ¬y = 0 → 1 = HMul.hMul (α := N₀) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 1 0
neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 1 1
pos₂ : ¬x * y = 0 → x = 0 → y = 0 → 1 = HMul.hMul (α := N₀) 0 0
neg₂ : ¬x * y = 0 → x = 0 → ¬y = 0 → 1 = HMul.hMul (α := N₀) 0 1
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have pos₃ : ¬x * y = 0 → ¬x = 0 → y = 0 → 1 = HMul.hMul (α := N₀) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀_1 : Type u_6
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
inst_4 : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst_5 : MulZeroOneClass M₀
inst_6 : MulZeroOneClass N₀
inst_7 : DecidablePred fun (x : M₀) ↦ x = 0
inst_8 : Nontrivial M₀
inst_9 : NoZeroDivisors M₀
x y : M₀
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 0 1
pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = HMul.hMul (α := N₀) 1 0
neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = HMul.hMul (α := N₀) 1 1
pos₂ : ¬x * y = 0 → x = 0 → y = 0 → 1 = HMul.hMul (α := N₀) 0 0
neg₂ : ¬x * y = 0 → x = 0 → ¬y = 0 → 1 = HMul.hMul (α := N₀) 0 1
pos₃ : ¬x * y = 0 → ¬x = 0 → y = 0 → 1 = HMul.hMul (α := N₀) 1 0
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := N₀) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have neg₃ : ¬x * y = 0 → ¬x = 0 → ¬y = 0 → 1 = HMul.hMul (α := N₀) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
M₀ : Type u_7
N₀ : Type u_8
inst : MulZeroOneClass M₀
inst_1 : MulZeroOneClass N₀
inst_2 : DecidablePred fun (x : M₀) ↦ x = 0
inst_3 : Nontrivial M₀
inst_4 : NoZeroDivisors M₀
inst_5 : Nontrivial N₀
x : M₀
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (0 : N₀) ↔ x = 0
have inl : Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (0 : N₀) ↔ Eq.{u_7 + 1} (α := M₀) 0 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
M₀ : Type u_7
N₀ : Type u_8
inst : MulZeroOneClass M₀
inst_1 : MulZeroOneClass N₀
inst_2 : DecidablePred fun (x : M₀) ↦ x = 0
inst_3 : Nontrivial M₀
inst_4 : NoZeroDivisors M₀
inst_5 : Nontrivial N₀
x : M₀
inl : Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (0 : N₀) ↔ Eq.{u_7 + 1} (α := M₀) 0 0
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (0 : N₀) ↔ x = 0
have inr : ∀ (hx : x ≠ 0), Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (0 : N₀) ↔ x = 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
M₀ : Type u_7
N₀ : Type u_8
inst : MulZeroOneClass M₀
inst_1 : MulZeroOneClass N₀
inst_2 : DecidablePred fun (x : M₀) ↦ x = 0
inst_3 : Nontrivial M₀
inst_4 : NoZeroDivisors M₀
inst_5 : Nontrivial N₀
x : M₀
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (1 : N₀) ↔ x ≠ 0
have inl : Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (1 : N₀) ↔ Ne.{u_7 + 1} (α := M₀) 0 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Hom (goal)
Goal:
M₀ : Type u_7
N₀ : Type u_8
inst : MulZeroOneClass M₀
inst_1 : MulZeroOneClass N₀
inst_2 : DecidablePred fun (x : M₀) ↦ x = 0
inst_3 : Nontrivial M₀
inst_4 : NoZeroDivisors M₀
inst_5 : Nontrivial N₀
x : M₀
inl : Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (1 : N₀) ↔ Ne.{u_7 + 1} (α := M₀) 0 0
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (1 : N₀) ↔ x ≠ 0
have inr : ∀ (hx : x ≠ 0), Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (1 : N₀) ↔ x ≠ 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
⊢ Eq (α := (x : ι) → M₀) (s.indicator fun (i : ι) ↦ f i * g i) fun (i : ι) ↦ s.indicator f i * s.indicator g i
have h : ∀ (x : ι), s.indicator (fun (i : ι) ↦ f i * g i) x = s.indicator f x * s.indicator g x
Tactic: funext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
⊢ s.indicator (fun (i : ι) ↦ f i * g i) x = s.indicator f x * s.indicator g x
have h : (if x ∈ s then f x * g x else 0) = (if x ∈ s then f x else 0) * if x ∈ s then g x else 0
Tactic: simp only [indicator]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Indicator (goal)
Goal:
ι : Type u_1
M₀ : Type u_4
inst : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x : ι
⊢ (if x ∈ s then f x * g x else 0) = (if x ∈ s then f x else 0) * if x ∈ s then g x else 0
have pos : x ∈ s → f x * g x = f x * g x
Tactic: split_ifs