awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 δ
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
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:
congr
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : Subsingleton α
⊢ Subsingleton (α →*₀ β)

Tactic:
.of_oneHomClass

Premises used: Subsingleton.of_oneHomClass
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : FunLike F α β
inst_3 : MonoidWithZeroHomClass F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑(↑f : α →*₀ β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : ZeroHom α β
h1 : f.toFun 1 = 1
hmul : ∀ (x y : α), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ Eq (α := (a : α) → β) (⇑{ toZeroHom := f, map_one' := h1, map_mul' := hmul : α →*₀ β } : (a : α) → β)
    (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
⊢ Eq (α := (a : α) → β) (⇑(↑f : ZeroHom α β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
⊢ (↑(↑f : α →* β) : OneHom α β).toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f g : α →*₀ β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
h1 : ZeroHom.toFun (↑f : ZeroHom α β) 1 = 1
hmul :
  ∀ (x y : α),
    ZeroHom.toFun (↑f : ZeroHom α β) (x * y) = ZeroHom.toFun (↑f : ZeroHom α β) x * ZeroHom.toFun (↑f : ZeroHom α β) y
⊢ { toZeroHom := (↑f : ZeroHom α β), map_one' := h1, map_mul' := hmul : α →*₀ β } = f

Tactic:
ext fun _ ↦ rfl

Premises used: MonoidWithZeroHom.ext, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = (↑f : α →* β)

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)

Tactic:
f.map_one'

Premises used: MonoidWithZeroHom.map_one'
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
f.map_zero'

Premises used: ZeroHom.map_zero', MonoidWithZeroHom.toZeroHom
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
a b : α
⊢ (f : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
f.map_mul' a b

Premises used: MonoidWithZeroHom.map_mul'
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : β)
neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (if p then 0 else 1) : β) (if p then 0 else 1 : β)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
h : p
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
h : ¬p
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : β)
neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (if p then 1 else 0) : β) (if p then 1 else 0 : β)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
h : p
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
h : ¬p
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : γ)
rw₂ rw₃ : Eq.{u_4 + 1} (α := γ) 0 0
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) 0) 0

Tactic:
rw [comp_apply, map_zero, map_zero]

Premises used: map_zero, Function.comp_apply
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : α) → β) 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : α →*₀ β
⊢ ∀ (x y : α),
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) (x * y) =
      HMul.hMul (α := γ)
        (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) x)
        (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑hnp : (a : β) → γ) (⇑hmn : (a : α) → β) y)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
g : β →*₀ γ
f : α →*₀ β
⊢ Eq (α := α → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
g : β →*₀ γ
f : α →*₀ β
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((g.comp f : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
inst_3 : MulZeroOneClass δ
f : α →*₀ β
g : β →*₀ γ
h : γ →*₀ δ
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: MonoidWithZeroHom.comp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
inst_2 : MulZeroOneClass γ
g₁ g₂ : β →*₀ γ
f : α →*₀ β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h ↦ ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h ↦ h ▸ rfl⟩

Premises used: MonoidWithZeroHom.ext, Iff.mpr, Function.Surjective.forall, Eq.rec, DFunLike.ext_iff, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)

Tactic:
rw [← comp_apply, h,
    comp_apply]

Premises used: MonoidWithZeroHom.comp_apply
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
⊢ Injective (α := α →*₀ β) toMonoidHom

Tactic:
Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
⊢ Injective (α := α →*₀ β) toZeroHom

Tactic:
Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
⊢ f.comp (id α) = f

Tactic:
ext fun _ ↦ rfl

Premises used: MonoidWithZeroHom.ext, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
Goal:
α : Type u_2
β : Type u_3
inst : MulZeroOneClass α
inst_1 : MulZeroOneClass β
f : α →*₀ β
⊢ comp (id β) f = f

Tactic:
ext fun _ ↦ rfl

Premises used: MonoidWithZeroHom.ext, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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 : α →*₀ β
dsimp : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((g : (a : α) → β) 0 : β) = 0
⊢ (↑(HMul.hMul (α := α →* β) (↑f : α →* β) (↑g : α →* β)) : OneHom α β).toFun 0 = 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
rw₁ rw₂ : Eq.{u_7 + 1} (α := β) 0 0
⊢ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((g : (a : α) → β) 0 : β) = 0

Tactic:
rw [map_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
⊢ Eq.{u_8 + 1} (α := N₀) (if Eq.{u_7 + 1} (α := M₀) 0 0 then 0 else 1) 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
⊢ Eq.{u_8 + 1} (α := N₀) (if Eq.{u_7 + 1} (α := M₀) 1 0 then 0 else 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
neg₃ : ¬x * y = 0 → ¬x = 0 → ¬y = 0 → 1 = 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)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : x * y = 0
h_1 : x = 0
h_2 : y = 0
⊢ 0 = HMul.hMul (α := N₀) 0 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : x * y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ 0 = HMul.hMul (α := N₀) 0 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : x * y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ 0 = HMul.hMul (α := N₀) 1 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : x * y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ 0 = HMul.hMul (α := N₀) 1 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : ¬x * y = 0
h_1 : x = 0
h_2 : y = 0
⊢ 1 = HMul.hMul (α := N₀) 0 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : ¬x * y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ 1 = HMul.hMul (α := N₀) 0 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : ¬x * y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ 1 = HMul.hMul (α := N₀) 1 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
h : ¬x * y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ 1 = HMul.hMul (α := N₀) 1 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
x : M₀
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (if x = 0 then 0 else 1 : N₀)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (0 : N₀)

Tactic:
if_pos rfl

Premises used: if_pos, rfl, ite
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
x : M₀
hx : x ≠ 0
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (1 : N₀)

Tactic:
if_neg hx

Premises used: if_neg, ite
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
inr : ∀ (hx : x ≠ 0), Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (0 : N₀) ↔ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (0 : N₀) ↔ Eq.{u_7 + 1} (α := M₀) 0 0

Tactic:
simp_all [one_apply_of_ne_zero]

Premises used: MonoidWithZeroHom.one_apply_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
hx : x ≠ 0
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (0 : N₀) ↔ x = 0

Tactic:
simp_all [one_apply_of_ne_zero]

Premises used: MonoidWithZeroHom.one_apply_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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
inr : ∀ (hx : x ≠ 0), Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (1 : N₀) ↔ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) 0 : N₀) (1 : N₀) ↔ Ne.{u_7 + 1} (α := M₀) 0 0

Tactic:
simp_all [one_apply_of_ne_zero]

Premises used: MonoidWithZeroHom.one_apply_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Hom
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₀
hx : x ≠ 0
⊢ Eq.{u_8 + 1} (α := N₀) ((1 : (a : M₀) → N₀) x : N₀) (1 : N₀) ↔ x ≠ 0

Tactic:
simp_all [one_apply_of_ne_zero]

Premises used: MonoidWithZeroHom.one_apply_of_ne_zero