awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
inl : ∀ (hs : s.erase 0 = ∅), #s ≤ #(s * s)
⊢ #s ≤ #(s * s)
have inr : ∀ (hs : (s.erase 0).Nonempty), #s ≤ #(s * s)
Tactic: obtain hs | hs := (s.erase 0).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : s.erase 0 = ∅
⊢ #s ≤ #(s * s)
have hs₁ : s = ∅ ∨ s = {0}
Tactic: rw [erase_eq_empty_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : s = ∅ ∨ s = {0}
⊢ #s ≤ #(s * s)
have inl : card.{u_1} (α := α) ∅ ≤ #(HMul.hMul (α := Finset α) ∅ ∅)
Tactic: obtain rfl | rfl := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : s = ∅ ∨ s = {0}
inl : card.{u_1} (α := α) ∅ ≤ #(HMul.hMul (α := Finset α) ∅ ∅)
⊢ #s ≤ #(s * s)
have inl₁ : card (α := α) {0} ≤ #(HMul.hMul (α := Finset α) {0} {0})
Tactic: obtain rfl | rfl := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : (s.erase 0).Nonempty
⊢ #s ≤ #(s * s)
have inr : ∀ (a : α) (ha : a ∈ s.erase 0), #s ≤ #(s * s)
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
a : α
ha : a ∈ s.erase 0
⊢ #s ≤ #(s * s)
have ha₁ : ¬a = 0 ∧ a ∈ s
Tactic: simp only [mem_erase, ne_eq] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) 0⁻¹ 0
have h : ∀ (a : α), Membership.mem (γ := Finset α) 0⁻¹ a ↔ Membership.mem (γ := Finset α) 0 a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
⊢ Eq.{u_1 + 1} (α := Set α) 0⁻¹ 0
have h : ∀ (x : α), Membership.mem (γ := Set α) 0⁻¹ x ↔ Membership.mem (γ := Set α) 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀
⊢ Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inl : Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) 0 : N₀) : G₀) ((1 : (a : M₀) → G₀) 0 : G₀)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have 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₀)
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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
⊢ Eq.{u_3 + 1} (α := G₀) ((1 : (a : N₀) → G₀) ((f : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inr : Ne.{u_2 + 1} (α := N₀) ((f : (a : M₀) → N₀) x : N₀) (0 : N₀)
Tactic: rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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
have inl : 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: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ (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
have 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₀)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀ →*₀ H₀) (comp (snd G₀ H₀) (inl G₀ H₀)) 1
have 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₀)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) x : H₀) ((1 : (a : G₀) → H₀) x : H₀)
have h : Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) 0 : H₀) ((1 : (a : G₀) → H₀) 0 : H₀)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) x : H₀) ((1 : (a : G₀) → H₀) x : H₀)
have 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₀)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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
⊢ 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₀)
have rw : Eq.{u_2 + 1} (α := H₀) ((comp (snd G₀ H₀) (inl G₀ H₀) : (a : G₀) → H₀) x : H₀) (1 : H₀)
Tactic: rw [← MonoidWithZeroHom.comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ 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₀)
have rw₁ : Eq.{u_2 + 1} (α := H₀) ((1 : (a : G₀) → H₀) x : H₀) (1 : H₀)
Tactic: rw [← MonoidWithZeroHom.comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ 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₀)
have rw₂ : Eq.{u_2 + 1} (α := H₀) 1 1
Tactic: rw [← MonoidWithZeroHom.comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀ →*₀ G₀) (comp (fst G₀ H₀) (inr G₀ H₀)) 1
have 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₀)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) x : G₀) ((1 : (a : H₀) → G₀) x : G₀)
have h : Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) 0 : G₀) ((1 : (a : H₀) → G₀) 0 : G₀)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) x : G₀) ((1 : (a : H₀) → G₀) x : G₀)
have 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₀)
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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
⊢ 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₀)
have rw : Eq.{u_1 + 1} (α := G₀) ((comp (fst G₀ H₀) (inr G₀ H₀) : (a : H₀) → G₀) x : G₀) (1 : G₀)
Tactic: rw [← MonoidWithZeroHom.comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ 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₀)
have rw₁ : Eq.{u_1 + 1} (α := G₀) ((1 : (a : H₀) → G₀) x : G₀) (1 : G₀)
Tactic: rw [← MonoidWithZeroHom.comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀)
⊢ 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₀)
have rw₂ : Eq.{u_1 + 1} (α := G₀) 1 1
Tactic: rw [← MonoidWithZeroHom.comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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
have inl : 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: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀) ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0) : H₀) (0 : 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
have inr : ∀ (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: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀
⊢ Commute (S := WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
    ((inl G₀ H₀ : (a : G₀) → WithZero (G₀ˣ × H₀ˣ)) m : 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₀ˣ))
have inl : 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₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀ˣ))
    ((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₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
have 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₀ˣ))
    ((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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀
⊢ 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₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
have inl : 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: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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)
⊢ 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₀ˣ))
have 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₀ˣ))
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀ˣ
⊢ 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₀ˣ))
    ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) n : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
have 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₀ˣ))
  ((inr G₀ H₀ : (a : H₀) → WithZero (G₀ˣ × H₀ˣ)) 0 : WithZero (Prod.{u_1, u_2} G₀ˣ H₀ˣ))
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.ProdHom (goal)
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₀ˣ))
⊢ 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₀ˣ))
have 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₀ˣ))
Tactic: obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
hb : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) a
hb' : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) b
⊢ Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
have obtain : ∀ (y : A) (hy : (f : (a : A) → B) y = (↑a : B)),
  Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
Tactic: obtain ⟨y, hy⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
hb' : Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) b
y : A
hy : (f : (a : A) → B) y = (↑a : B)
⊢ Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
have obtain : ∀ (y' : A) (hy' : (f : (a : A) → B) y' = (↑b : B)),
  Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
Tactic: obtain ⟨y', hy'⟩ := hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a : B)
y' : A
hy' : (f : (a : A) → B) y' = (↑b : B)
⊢ Membership.mem (γ := Set Bˣ) (Units.val ⁻¹' range.{u_2, u_1 + 1} (ι := A) (⇑f : (a : A) → B)) (a * b)
have h : (f : (a : A) → B) (y * y') = (↑(a * b) : B)
Tactic: use y * y'
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a : B)
y' : A
hy' : (f : (a : A) → B) y' = (↑b : B)
⊢ (f : (a : A) → B) (y * y') = (↑(a * b) : B)
have h : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
Tactic: rw [map_mul, hy, hy', Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a : B)
y' : A
hy' : (f : (a : A) → B) y' = (↑b : B)
h : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
⊢ (f : (a : A) → B) (y * y') = (↑(a * b) : B)
have h₁ : HMul.hMul (β := B) (↑a : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
Tactic: rw [map_mul, hy, hy', Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
F : Type u_3
inst : FunLike F A B
f : F
inst_1 : MonoidWithZero A
inst_2 : MonoidWithZero B
inst_3 : MonoidWithZeroHomClass F A B
a b : Bˣ
y : A
hy : (f : (a : A) → B) y = (↑a : B)
y' : A
hy' : (f : (a : A) → B) y' = (↑b : B)
h : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
h₁ : HMul.hMul (β := B) (↑a : B) ((f : (a : A) → B) y' : B) = (↑(a * b) : B)
⊢ (f : (a : A) → B) (y * y') = (↑(a * b) : B)
have h₂ : (↑a : B) * (↑b : B) = (↑(a * b) : B)
Tactic: rw [map_mul, hy, hy', Units.val_mul]