awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : (↑a : G₀) ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') 1 0
have rw : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 1 : M₀') (0 : M₀')
Tactic: rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : (↑a : G₀) ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')
rw : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 1 : M₀') (0 : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') 1 0
have rw₁ : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') ((↑a : G₀) * (↑a⁻¹ : G₀)) : M₀') (0 : M₀')
Tactic: rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : (↑a : G₀) ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')
rw : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 1 : M₀') (0 : M₀')
rw₁ : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') ((↑a : G₀) * (↑a⁻¹ : G₀)) : M₀') (0 : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') 1 0
have rw₂ : HMul.hMul (α := M₀') (β := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') ((f : (a : G₀) → M₀') (↑a⁻¹ : G₀) : M₀') = 0
Tactic: rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : (↑a : G₀) ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')
rw : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 1 : M₀') (0 : M₀')
rw₁ : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') ((↑a : G₀) * (↑a⁻¹ : G₀)) : M₀') (0 : M₀')
rw₂ :
  HMul.hMul (α := M₀') (β := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') ((f : (a : G₀) → M₀') (↑a⁻¹ : G₀) : M₀') = 0
⊢ Eq.{u_4 + 1} (α := M₀') 1 0
have rw₃ : HMul.hMul (α := M₀') (β := M₀') (0 : M₀') ((f : (a : G₀) → M₀') (↑a⁻¹ : G₀) : M₀') = 0
Tactic: rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀'
inst_2 : Nontrivial M₀'
inst_3 : FunLike F G₀ M₀'
inst_4 : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : (↑a : G₀) ≠ 0
H : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') (0 : M₀')
rw : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 1 : M₀') (0 : M₀')
rw₁ : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') ((↑a : G₀) * (↑a⁻¹ : G₀)) : M₀') (0 : M₀')
rw₂ :
  HMul.hMul (α := M₀') (β := M₀') ((f : (a : G₀) → M₀') (↑a : G₀) : M₀') ((f : (a : G₀) → M₀') (↑a⁻¹ : G₀) : M₀') = 0
rw₃ : HMul.hMul (α := M₀') (β := M₀') (0 : M₀') ((f : (a : G₀) → M₀') (↑a⁻¹ : G₀) : M₀') = 0
⊢ Eq.{u_4 + 1} (α := M₀') 1 0
have rw₄ : Eq.{u_4 + 1} (α := M₀') 0 0
Tactic: rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst : GroupWithZero G₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F' G₀ M₀'
a : G₀
inst_3 : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') ((g : (a : G₀) → M₀') a : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a⁻¹ : M₀') ((g : (a : G₀) → M₀') a⁻¹ : M₀')
have inl : ∀ (h : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0 : M₀') ((g : (a : G₀) → M₀') 0 : M₀')),
  Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0⁻¹ : M₀') ((g : (a : G₀) → M₀') 0⁻¹ : M₀')
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst : GroupWithZero G₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F' G₀ M₀'
a : G₀
inst_3 : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') ((g : (a : G₀) → M₀') a : M₀')
inl :
  ∀ (h : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0 : M₀') ((g : (a : G₀) → M₀') 0 : M₀')),
    Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0⁻¹ : M₀') ((g : (a : G₀) → M₀') 0⁻¹ : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a⁻¹ : M₀') ((g : (a : G₀) → M₀') a⁻¹ : M₀')
have inr : ∀ (ha : a ≠ 0), Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a⁻¹ : M₀') ((g : (a : G₀) → M₀') a⁻¹ : M₀')
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst : GroupWithZero G₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F' G₀ M₀'
inst_3 : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h inl : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0 : M₀') ((g : (a : G₀) → M₀') 0 : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0⁻¹ : M₀') ((g : (a : G₀) → M₀') 0⁻¹ : M₀')
have inl₁ : Eq.{u_4 + 1} (α := M₀') (0 : M₀') ((g : (a : G₀) → M₀') 0 : M₀')
Tactic: rw [inv_zero, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst : GroupWithZero G₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F' G₀ M₀'
inst_3 : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h inl : Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0 : M₀') ((g : (a : G₀) → M₀') 0 : M₀')
inl₁ : Eq.{u_4 + 1} (α := M₀') (0 : M₀') ((g : (a : G₀) → M₀') 0 : M₀')
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0⁻¹ : M₀') ((g : (a : G₀) → M₀') 0⁻¹ : M₀')
have inl₂ : Eq.{u_4 + 1} (α := M₀') 0 0
Tactic: rw [inv_zero, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
⊢ Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')
have pos : ∀ (h : a = 0), Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
pos : ∀ (h : a = 0), Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')
⊢ Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')
have neg : ∀ (h : ¬a = 0), Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')
have neg : HMul.hMul (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') ((f : (a : G₀) → G₀') a : G₀') = 1
Tactic: apply eq_inv_of_mul_eq_one_left
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ HMul.hMul (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') ((f : (a : G₀) → G₀') a : G₀') = 1
have neg : Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') (a⁻¹ * a) : G₀') (1 : G₀')
Tactic: rw [← map_mul, inv_mul_cancel₀ h, map_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
neg : Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') (a⁻¹ * a) : G₀') (1 : G₀')
⊢ HMul.hMul (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') ((f : (a : G₀) → G₀') a : G₀') = 1
have neg₁ : Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') 1 : G₀') (1 : G₀')
Tactic: rw [← map_mul, inv_mul_cancel₀ h, map_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Lemmas (goal)
Goal:
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
neg : Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') (a⁻¹ * a) : G₀') (1 : G₀')
neg₁ : Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') 1 : G₀') (1 : G₀')
⊢ HMul.hMul (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') ((f : (a : G₀) → G₀') a : G₀') = 1
have neg₂ : Eq.{u_5 + 1} (α := G₀') 1 1
Tactic: rw [← map_mul, inv_mul_cancel₀ h, map_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
hf : Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : β
⊢ ∃ (a : WithZero α),
    (((lift' : (a : α →* β) → WithZero α →*₀ β) f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β) : (a : WithZero α) → β)
        a =
      b
have obtain : ∀ (a : α),
  ∃ (a_1 : WithZero α),
    Eq.{u_2 + 1} (α := β)
      ((((lift' : (a : α →* β) → WithZero α →*₀ β) f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β) :
            (a : WithZero α) → β)
          a_1 :
        β)
      ((f : (a : α) → β) a : β)
Tactic: obtain ⟨a, rfl⟩ := hf b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
β : Type u_2
inst : MulOneClass β
⊢ Eq (α := WithZero β →* WithZero β) (↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) (MonoidHom.id (WithZero β))
have h : ∀ (x : WithZero β),
  Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
β : Type u_2
inst : MulOneClass β
x : WithZero β
⊢ Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
have h : Eq (α := WithZero β)
  (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) 0 : WithZero β)
  ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) 0 : WithZero β)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
β : Type u_2
inst : MulOneClass β
x : WithZero β
h :
  Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) 0 : WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) 0 : WithZero β)
⊢ Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
have h₁ : ∀ (a : β),
  Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) (↑a : WithZero β) :
      WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) (↑a : WithZero β) : WithZero β)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : MulOneClass γ
f : α →* β
g : β →* γ
x : WithZero α
⊢ Eq.{u_3 + 1} (α := WithZero γ)
    ((map' g : (a : WithZero β) → WithZero γ) ((map' f : (a : WithZero α) → WithZero β) x) : WithZero γ)
    ((map' (g.comp f) : (a : WithZero α) → WithZero γ) x : WithZero γ)
have zero : Eq.{u_3 + 1} (α := WithZero γ)
  ((map' g : (a : WithZero β) → WithZero γ) ((map' f : (a : WithZero α) → WithZero β) 0) : WithZero γ)
  ((map' (g.comp f) : (a : WithZero α) → WithZero γ) 0 : WithZero γ)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : MulOneClass γ
f : α →* β
g : β →* γ
x : WithZero α
zero :
  Eq.{u_3 + 1} (α := WithZero γ)
    ((map' g : (a : WithZero β) → WithZero γ) ((map' f : (a : WithZero α) → WithZero β) 0) : WithZero γ)
    ((map' (g.comp f) : (a : WithZero α) → WithZero γ) 0 : WithZero γ)
⊢ Eq.{u_3 + 1} (α := WithZero γ)
    ((map' g : (a : WithZero β) → WithZero γ) ((map' f : (a : WithZero α) → WithZero β) x) : WithZero γ)
    ((map' (g.comp f) : (a : WithZero α) → WithZero γ) x : WithZero γ)
have coe : ∀ (a : α),
  Eq.{u_3 + 1} (α := WithZero γ)
    ((map' g : (a : WithZero β) → WithZero γ) ((map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α)) : WithZero γ)
    ((map' (g.comp f) : (a : WithZero α) → WithZero γ) (↑a : WithZero α) : WithZero γ)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := WithZero α) (β := WithZero β) (⇑(map' f) : (a : WithZero α) → WithZero β) ↔
    Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
have simp : ((∃ (a : WithZero α),
      Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
    ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)) ↔
  ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
Tactic: simp only [Surjective, «forall»]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
⊢ ((∃ (a : WithZero α),
        Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
      ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)) ↔
    ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
have refine_1 : ∀
  (h :
    (∃ (a : WithZero α),
        Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
      ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β))
  (b : β), ∃ (a : α), (f : (a : α) → β) a = b
Tactic: refine ⟨fun h b ↦ ?_, fun h ↦ ⟨⟨0, by simp⟩, fun b ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
refine_1 :
  ∀
    (h :
      (∃ (a : WithZero α),
          Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
        ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β))
    (b : β), ∃ (a : α), (f : (a : α) → β) a = b
⊢ ((∃ (a : WithZero α),
        Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
      ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)) ↔
    ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
have refine_2 : ∀ (h : ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b) (b : β),
  ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
Tactic: refine ⟨fun h b ↦ ?_, fun h ↦ ⟨⟨0, by simp⟩, fun b ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h :
  (∃ (a : WithZero α),
      Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
    ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)
b : β
⊢ ∃ (a : α), (f : (a : α) → β) a = b
have refine_1 : ∀ (a : WithZero α) (hab : (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)),
  ∃ (a : α), (f : (a : α) → β) a = b
Tactic: obtain ⟨a, hab⟩ := h.2 b
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h :
  (∃ (a : WithZero α),
      Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
    ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)
b : β
a : WithZero α
hab : (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
⊢ ∃ (a : α), (f : (a : α) → β) a = b
have refine_1 : ∀ (hab : (map' f : (a : WithZero α) → WithZero β) 0 = (↑b : WithZero β)), ∃ (a : α), (f : (a : α) → β) a = b
Tactic: induction a using WithZero.recZeroCoe
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h :
  (∃ (a : WithZero α),
      Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
    ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)
b : β
a : WithZero α
hab : (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
refine_1 : ∀ (hab : (map' f : (a : WithZero α) → WithZero β) 0 = (↑b : WithZero β)), ∃ (a : α), (f : (a : α) → β) a = b
⊢ ∃ (a : α), (f : (a : α) → β) a = b
have refine_1₁ : ∀ (a : α) (hab : (map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α) = (↑b : WithZero β)),
  ∃ (a : α), (f : (a : α) → β) a = b
Tactic: induction a using WithZero.recZeroCoe
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h :
  (∃ (a : WithZero α),
      Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) a : WithZero β) (0 : WithZero β)) ∧
    ∀ (a : β), ∃ (a_1 : WithZero α), (map' f : (a : WithZero α) → WithZero β) a_1 = (↑a : WithZero β)
b : β
a : α
hab : (map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α) = (↑b : WithZero β)
⊢ ∃ (a : α), (f : (a : α) → β) a = b
have hab₁ : (f : (a : α) → β) a = b
Tactic: simp at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
b : β
⊢ ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
have refine_2 : ∀ (a : α) (ha : (f : (a : α) → β) a = b),
  ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
Tactic: obtain ⟨a, ha⟩ := h b
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
b : β
a : α
ha : (f : (a : α) → β) a = b
⊢ ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
have h₁ : (map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α) = (↑b : WithZero β)
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Monoid α
n : ℕ
⊢ HPow.hPow (α := WithZero α) 0 (n + 1) = HPow.hPow (α := WithZero α) 0 n * 0
have simp : HPow.hPow (α := WithZero α) 0 (n + 1) = 0
Tactic: simp only [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DivInvMonoid α
n : ℕ
⊢ HPow.hPow (α := WithZero α) (β := ℤ) none (↑n.succ : ℤ) = HPow.hPow (α := WithZero α) (β := ℤ) none (↑n : ℤ) * none
have change : HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n : ℤ) * 0
Tactic: change 0 ^ _ = 0 ^ _ * 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DivInvMonoid α
n : ℕ
⊢ HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n : ℤ) * 0
have simp : HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = 0
Tactic: simp only [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1
have lift : ∀ (a : α), (↑a : WithZero α) * (↑a : WithZero α)⁻¹ = 1
Tactic: lift a to α using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
a : α
⊢ (↑a : WithZero α) * (↑a : WithZero α)⁻¹ = 1
have norm_cast : a * a⁻¹ = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
G : Type u_4
inst_1 : GroupWithZero G
inst_2 : DecidablePred fun (a : G) ↦ a = 0
x : G
⊢ recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val
      (if h : x = 0 then 0 else (↑(Units.mk0 x h) : WithZero Gˣ)) =
    x
have isTrue : x = 0 → recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val 0 = x
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
G : Type u_4
inst_1 : GroupWithZero G
inst_2 : DecidablePred fun (a : G) ↦ a = 0
x : G
isTrue : x = 0 → recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val 0 = x
⊢ recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val
      (if h : x = 0 then 0 else (↑(Units.mk0 x h) : WithZero Gˣ)) =
    x
have isFalse : ∀ (h : ¬x = 0), recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val (↑(Units.mk0 x h) : WithZero Gˣ) = x
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x : α ≃* β
⊢ (fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
        { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ : α ≃* β })
      ((fun (e : α ≃* β) ↦
          ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
              invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯, right_inv := ⋯,
              map_mul' := ⋯ } :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
        x) =
    x
have h : ∀ (x_1 : α),
  Eq.{u_2 + 1} (α := β)
    (((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
              { toFun := fun (x : α) ↦ unzero sorry, invFun := fun (x : β) ↦ unzero sorry, left_inv := sorry, right_inv := sorry,
                map_mul' := sorry : α ≃* β })
            ((fun (e : α ≃* β) ↦
                ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                    invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := sorry,
                    right_inv := sorry, map_mul' := sorry } :
                  MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
              x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)
Tactic: ext