awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : CommMonoidWithZero M₀
inst_1 : CommMonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : CommMonoidWithZero M₀
inst_1 : CommMonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
inst : GroupWithZero M₀
inst_1 : DecidablePred fun (x : M₀) ↦ x = 0
⊢ Eq (α := WithZero M₀ˣ →*₀ M₀) (↑withZeroUnitsEquiv : WithZero M₀ˣ →*₀ M₀)
    ((lift' : (a : M₀ˣ →* M₀) → WithZero M₀ˣ →*₀ M₀) (Units.coeHom M₀))

Tactic:
rfl

Premises used: MonoidWithZeroHomClass.toMonoidWithZeroHom, WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : GroupWithZero M₀
inst_1 : MulZeroOneClass N₀
inst_2 : Nontrivial N₀
inst_3 : NoZeroDivisors N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
inst_6 : DecidablePred fun (x : N₀) ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
inl : Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) 0 : N₀) : G₀) ((1 : (a : M₀) → G₀) 0 : G₀)
inr :
  ∀ (hx : x ≠ 0),
    Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : GroupWithZero M₀
inst_1 : MulZeroOneClass N₀
inst_2 : Nontrivial N₀
inst_3 : NoZeroDivisors N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
inst_6 : DecidablePred fun (x : N₀) ↦ x = 0
f : M₀ →*₀ N₀
⊢ Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) 0 : N₀) : G₀) ((1 : (a : M₀) → G₀) 0 : G₀)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : GroupWithZero M₀
inst_1 : MulZeroOneClass N₀
inst_2 : Nontrivial N₀
inst_3 : NoZeroDivisors N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
inst_6 : DecidablePred fun (x : N₀) ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
inr : Ne.{u_2 + 1} (α := N₀) ((f : (a : M₀) → N₀) x : N₀) (0 : N₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)

Tactic:
rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero]

Premises used: MonoidWithZeroHom.one_apply_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : GroupWithZero M₀
inst_1 : MulZeroOneClass N₀
inst_2 : Nontrivial N₀
inst_3 : NoZeroDivisors N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
inst_6 : DecidablePred fun (x : N₀) ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx inr inr₁ inr₂ inr₃ : x ≠ 0
⊢ Ne.{u_2 + 1} (α := N₀) ((f : (a : M₀) → N₀) x : N₀) (0 : N₀)

Tactic:
rwa [map_ne_zero f]

Premises used: map_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : GroupWithZero M₀
inst_1 : MulZeroOneClass N₀
inst_2 : Nontrivial N₀
inst_3 : NoZeroDivisors N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
inst_6 : DecidablePred fun (x : N₀) ↦ x = 0
f : M₀ →*₀ N₀
⊢ Eq (α := M₀ →*₀ G₀) (comp 1 f) 1

Tactic:
ext <| one_apply_apply_eq _

Premises used: MonoidWithZeroHom.ext, MonoidWithZeroHom.one_apply_apply_eq
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
x : G₀ˣ
⊢ Eq (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑x : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((↑(x, 1) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
simp [inl]

Premises used: MonoidWithZeroHom.inl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
x : H₀ˣ
⊢ Eq (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑x : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((↑(1, x) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
simp [inr]

Premises used: MonoidWithZeroHom.inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
x : Prod.{u_1, u_2} G₀ˣ H₀ˣ
⊢ (fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀) (↑x : WithZero (G₀ˣ × H₀ˣ)) = (↑x.1 : G₀)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
x : Prod.{u_1, u_2} G₀ˣ H₀ˣ
⊢ (snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀) (↑x : WithZero (G₀ˣ × H₀ˣ)) = (↑x.2 : H₀)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
x : G₀
inl :
  Eq.{u_1 + 1} (α := G₀)
    ((fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀) ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0) :
      G₀)
    (0 : G₀)
inr :
  ∀ (w : G₀ˣ),
    (fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)
        ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) :
          WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
      (↑w : G₀)
⊢ (fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)
      ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    x

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀) ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0) : G₀) (0 : G₀)

Tactic:
simp [WithZero.withZeroUnitsEquiv, fst, inl]

Premises used: MonoidWithZeroHom.fst, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
w : G₀ˣ
⊢ (fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)
      ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    (↑w : G₀)

Tactic:
simp [WithZero.withZeroUnitsEquiv, fst, inl]

Premises used: MonoidWithZeroHom.fst, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
⊢ Eq (α := G₀ →*₀ G₀) (comp (β := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (fst G₀ H₀) (inl G₀ H₀)) (id G₀)

Tactic:
MonoidWithZeroHom.ext fun _ ↦ fst_inl _

Premises used: MonoidWithZeroHom.ext, MonoidWithZeroHom.fst_inl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
h :
  ∀ (x : G₀),
    Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) x : H₀) ((1 : (a : G₀) → H₀) x : H₀)
⊢ Eq (α := G₀ →*₀ H₀) (comp (snd G₀ H₀) (inl G₀ H₀)) 1

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
x : G₀
h : Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) 0 : H₀) ((1 : (a : G₀) → H₀) 0 : H₀)
h₁ :
  ∀ (w : G₀ˣ),
    Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) (↑w : G₀) : H₀)
      ((1 : (a : G₀) → H₀) (↑w : G₀) : H₀)
⊢ Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) x : H₀) ((1 : (a : G₀) → H₀) x : H₀)

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
⊢ Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) 0 : H₀) ((1 : (a : G₀) → H₀) 0 : H₀)

Tactic:
simp_all [WithZero.withZeroUnitsEquiv, snd, inl]

Premises used: MonoidWithZeroHom.snd, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
w : G₀ˣ
⊢ Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) (↑w : G₀) : H₀)
    ((1 : (a : G₀) → H₀) (↑w : G₀) : H₀)

Tactic:
simp_all [WithZero.withZeroUnitsEquiv, snd, inl]

Premises used: MonoidWithZeroHom.snd, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
x : G₀
hx : x ≠ 0
rw : Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) x : H₀) (1 : H₀)
rw₁ : Eq.{u_2 + 1} (α := H₀) ((1 : (a : G₀) → H₀) x : H₀) (1 : H₀)
rw₂ rw₃ : Eq.{u_2 + 1} (α := H₀) 1 1
⊢ Eq.{u_2 + 1} (α := H₀)
    ((snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)
        ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) :
      H₀)
    (1 : H₀)

Tactic:
rw [← MonoidWithZeroHom.comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]

Premises used: MonoidWithZeroHom.comp_apply, MonoidWithZeroHom.snd_comp_inl, MonoidWithZeroHom.one_apply_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
h :
  ∀ (x : H₀),
    Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) x : G₀) ((1 : (a : H₀) → G₀) x : G₀)
⊢ Eq (α := H₀ →*₀ G₀) (comp (fst G₀ H₀) (inr G₀ H₀)) 1

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
x : H₀
h : Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) 0 : G₀) ((1 : (a : H₀) → G₀) 0 : G₀)
h₁ :
  ∀ (w : H₀ˣ),
    Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) (↑w : H₀) : G₀)
      ((1 : (a : H₀) → G₀) (↑w : H₀) : G₀)
⊢ Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) x : G₀) ((1 : (a : H₀) → G₀) x : G₀)

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
⊢ Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) 0 : G₀) ((1 : (a : H₀) → G₀) 0 : G₀)

Tactic:
simp_all [WithZero.withZeroUnitsEquiv, fst, inr]

Premises used: MonoidWithZeroHom.fst, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
w : H₀ˣ
⊢ Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) (↑w : H₀) : G₀)
    ((1 : (a : H₀) → G₀) (↑w : H₀) : G₀)

Tactic:
simp_all [WithZero.withZeroUnitsEquiv, fst, inr]

Premises used: MonoidWithZeroHom.fst, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
x : H₀
hx : x ≠ 0
rw : Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) x : G₀) (1 : G₀)
rw₁ : Eq.{u_1 + 1} (α := G₀) ((1 : (a : H₀) → G₀) x : G₀) (1 : G₀)
rw₂ rw₃ : Eq.{u_1 + 1} (α := G₀) 1 1
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)
        ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) :
      G₀)
    (1 : G₀)

Tactic:
rw [← MonoidWithZeroHom.comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]

Premises used: MonoidWithZeroHom.comp_apply, MonoidWithZeroHom.one_apply_of_ne_zero, MonoidWithZeroHom.fst_comp_inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
x : H₀
inl :
  Eq.{u_2 + 1} (α := H₀)
    ((snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀) ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0) :
      H₀)
    (0 : H₀)
inr :
  ∀ (w : H₀ˣ),
    (snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)
        ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : H₀) :
          WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
      (↑w : H₀)
⊢ (snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)
      ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    x

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
⊢ Eq.{u_2 + 1} (α := H₀)
    ((snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀) ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0) : H₀) (0 : H₀)

Tactic:
simp [WithZero.withZeroUnitsEquiv, snd, inr]

Premises used: MonoidWithZeroHom.snd, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
w : H₀ˣ
⊢ (snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)
      ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    (↑w : H₀)

Tactic:
simp [WithZero.withZeroUnitsEquiv, snd, inr]

Premises used: MonoidWithZeroHom.snd, WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
⊢ Eq (α := H₀ →*₀ H₀) (comp (β := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (snd G₀ H₀) (inr G₀ H₀)) (id H₀)

Tactic:
MonoidWithZeroHom.ext fun _ ↦ snd_inr _

Premises used: MonoidWithZeroHom.ext, MonoidWithZeroHom.snd_inr
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
x : G₀
⊢ (fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)
      ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : H₀) ↦ x = 0
x : H₀
⊢ (snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)
      ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
x : G₀
⊢ (fst G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)
      ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
⊢ Function.Surjective (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (β := G₀)
    (⇑(fst G₀ H₀) : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)

Tactic:
exact Function.HasRightInverse.surjective ⟨inl .., fun _ ↦ by simp⟩

Premises used: Function.HasRightInverse.surjective, MonoidWithZeroHom.inl, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
⊢ Function.Surjective (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (β := G₀)
    (⇑(fst G₀ H₀) : (a : WithZero (G₀ˣ × H₀ˣ)) → G₀)

Tactic:
classical
  exact Function.HasRightInverse.surjective ⟨inl .., fun _ ↦ by simp⟩

Premises used: Function.HasRightInverse.surjective, MonoidWithZeroHom.inl, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
x : H₀
⊢ (snd G₀ H₀ : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)
      ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) x : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
⊢ Function.Surjective (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (β := H₀)
    (⇑(snd G₀ H₀) : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)

Tactic:
exact Function.HasRightInverse.surjective ⟨inr .., fun _ ↦ by simp⟩

Premises used: Function.HasRightInverse.surjective, MonoidWithZeroHom.inr, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
⊢ Function.Surjective (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (β := H₀)
    (⇑(snd G₀ H₀) : (a : WithZero (G₀ˣ × H₀ˣ)) → H₀)

Tactic:
classical
  exact Function.HasRightInverse.surjective ⟨inr .., fun _ ↦ by simp⟩

Premises used: Function.HasRightInverse.surjective, MonoidWithZeroHom.inr, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
m : G₀ˣ
n : H₀ˣ
⊢ HMul.hMul (α := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) (β := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑m : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑n : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) =
    (↑(m, n) : WithZero (G₀ˣ × H₀ˣ))

Tactic:
simp [inl, WithZero.withZeroUnitsEquiv, inr, ← WithZero.coe_mul]

Premises used: WithZero.withZeroUnitsEquiv, MonoidWithZeroHom.inl, MonoidWithZeroHom.inr, WithZero.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
m : G₀
n : H₀
inl :
  Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
inr :
  ∀ (w : G₀ˣ),
    Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) m : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit m

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
n : H₀
inl :
  Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0)
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0)
inl₁ :
  ∀ (w : H₀ˣ),
    Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
n : H₀
w : G₀ˣ
inr :
  Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
inr₁ :
  ∀ (w_1 : H₀ˣ),
    Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
      ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w_1 : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : G₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((MonoidWithZeroHom.inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ)) ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0)
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0)

Tactic:
simp [inl, inr, WithZero.withZeroUnitsEquiv, commute_iff_eq, ← WithZero.coe_mul]

Premises used: WithZero.withZeroUnitsEquiv, commute_iff_eq, MonoidWithZeroHom.inl, MonoidWithZeroHom.inr, WithZero.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.ProdHom
Goal:
G₀ : Type u_1
H₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : GroupWithZero H₀
inst_2 : DecidablePred fun (x : G₀) ↦ x = 0
inst_3 : DecidablePred fun (x : H₀) ↦ x = 0
w : H₀ˣ
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) (↑w : H₀) : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))

Tactic:
simp [inl, inr, WithZero.withZeroUnitsEquiv, commute_iff_eq, ← WithZero.coe_mul]

Premises used: WithZero.withZeroUnitsEquiv, commute_iff_eq, MonoidWithZeroHom.inl, MonoidWithZeroHom.inr, WithZero.coe_mul