awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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
rw₄ rw₅ : Eq.{u_4 + 1} (α := M₀') 0 0
⊢ Eq.{u_4 + 1} (α := M₀') 1 0

Tactic:
rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]

Premises used: MulZeroClass.zero_mul, Units.mul_inv, map_mul, map_one
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a : M₀') (0 : M₀') ↔ a = 0

Tactic:
not_iff_not.1 (map_ne_zero f)

Premises used: not_iff_not, Iff.mp, map_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
inr : ∀ (ha : a ≠ 0), 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₀')

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
inl₂ inl₃ : Eq.{u_4 + 1} (α := M₀') 0 0
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') 0⁻¹ : M₀') ((g : (a : G₀) → M₀') 0⁻¹ : M₀')

Tactic:
rw [inv_zero, map_zero, map_zero]

Premises used: inv_zero, map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
ha : a ≠ 0
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a⁻¹ : M₀') ((g : (a : G₀) → M₀') a⁻¹ : M₀')

Tactic:
(IsUnit.mk0 a ha).eq_on_inv f g h

Premises used: IsUnit.eq_on_inv, IsUnit.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
ha : a ≠ 0
⊢ Eq.{u_4 + 1} (α := M₀') ((f : (a : G₀) → M₀') a⁻¹ : M₀') ((g : (a : G₀) → M₀') a⁻¹ : M₀')

Tactic:
exact (IsUnit.mk0 a ha).eq_on_inv f g h

Premises used: IsUnit.eq_on_inv, IsUnit.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
neg : ∀ (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₀')

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')

Tactic:
simp [h, map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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 : HMul.hMul (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') ((f : (a : G₀) → G₀') a : G₀') = 1
⊢ Eq.{u_5 + 1} (α := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') (((f : (a : G₀) → G₀') a)⁻¹ : G₀')

Tactic:
apply eq_inv_of_mul_eq_one_left

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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₀')
neg₂ neg₃ : Eq.{u_5 + 1} (α := G₀') 1 1
⊢ HMul.hMul (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a⁻¹ : G₀') ((f : (a : G₀) → G₀') a : G₀') = 1

Tactic:
rw [← map_mul, inv_mul_cancel₀ h, map_one]

Premises used: map_mul, map_one, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
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 b : G₀
⊢ (f : (a : G₀) → G₀') (a / b) =
    HDiv.hDiv (α := G₀') (β := G₀') ((f : (a : G₀) → G₀') a : G₀') ((f : (a : G₀) → G₀') b : G₀')

Tactic:
map_div' f (map_inv₀ f) a b

Premises used: map_div', map_inv₀
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
M : Type u_8
inst : CommMonoidWithZero M
⊢ Eq.{u_8 + 1} (α := (a : M) → M) (⇑inverse : (a : M) → M) Ring.inverse

Tactic:
rfl

Premises used: Ring.inverse, dite, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
M : Type u_8
inst : CommMonoidWithZero M
a : M
⊢ (inverse : (a : M) → M) a = a⁻¹ʳ

Tactic:
rfl

Premises used: Ring.inverse, dite, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas
Goal:
F : Type u_8
G₀ : Type u_9
G₀' : Type u_10
inst : GroupWithZero G₀
inst_1 : GroupWithZero G₀'
inst_2 : FunLike F G₀ G₀'
inst_3 : MonoidWithZeroHomClass F G₀ G₀'
f : F
x : G₀
n : ℤ
⊢ (f : (a : G₀) → G₀') (x ^ n) = HPow.hPow (α := G₀') ((f : (a : G₀) → G₀') x : G₀') n

Tactic:
map_zpow' f (map_inv₀ f) x n

Premises used: map_inv₀, map_zpow'
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := WithZero α) (↑1 : WithZero α) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
N : Type u_5
inst : One M
f : M → N
z : N
⊢ recZeroCoe (motive := fun (x : WithZero M) ↦ N) z f 1 = f 1

Tactic:
rfl

Premises used: WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
a b : α
⊢ (↑(a * b) : WithZero α) = (↑a : WithZero α) * (↑b : WithZero α)

Tactic:
rfl

Premises used: WithZero.coe, rfl, Option.map₂
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Mul α
x y : WithZero α
hxy : x * y ≠ 0
⊢ unzero hxy = unzero ⋯ * unzero ⋯

Tactic:
simp only [← coe_inj, coe_mul, coe_unzero]

Premises used: WithZero.coe_inj, WithZero.coe_unzero, WithZero.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Mul α
⊢ NoZeroDivisors.{u_1} (WithZero α)

Tactic:
⟨Option.map₂_eq_none_iff.1⟩

Premises used: Option.map₂_eq_none_iff, Iff.mp, NoZeroDivisors.mk
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f g : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β
h : (↑f : WithZero α →* β).comp coeMonoidHom = (↑g : WithZero α →* β).comp coeMonoidHom
⊢ f = g

Tactic:
DFunLike.ext _ _ fun
    | 0 => (map_zero f).trans (map_zero g).symm
    | (g : α) => DFunLike.congr_fun h g

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
⊢ Eq.{u_2 + 1} (α := β) (recZeroCoe (motive := fun (x : WithZero α) ↦ β) 0 (⇑f : (a : α) → β) 1 : β) (1 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
⊢ Eq.{u_2 + 1} (α := β)
    ((((lift' : (a : α →* β) → WithZero α →*₀ β) f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β) :
          (a : WithZero α) → β)
        0 :
      β)
    (0 : β)

Tactic:
rfl

Premises used: WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
x : α
⊢ Eq.{u_2 + 1} (α := β)
    ((((lift' : (a : α →* β) → WithZero α →*₀ β) f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β) :
          (a : WithZero α) → β)
        (↑x : WithZero α) :
      β)
    ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β
⊢ f = (lift' : (a : α →* β) → WithZero α →*₀ β) ((↑f : WithZero α →* β).comp coeMonoidHom)

Tactic:
(lift'.apply_symm_apply f).symm

Premises used: Equiv.apply_symm_apply, WithZero.lift', Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
hf : Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : β
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 : β)
⊢ ∃ (a : WithZero α),
    (((lift' : (a : α →* β) → WithZero α →*₀ β) f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β) : (a : WithZero α) → β)
        a =
      b

Tactic:
obtain ⟨a, rfl⟩ := hf b

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
hf : Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ Eq.{u_2 + 1} (α := β)
    ((((lift' : (a : α →* β) → WithZero α →*₀ β) f : MonoidWithZeroHom.{u_1, u_2} (WithZero α) β) :
          (a : WithZero α) → β)
        (↑a : WithZero α) :
      β)
    ((f : (a : α) → β) a : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulZeroOneClass β
f : α →* β
hf : Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
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:
exact ⟨a, by simp⟩
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
⊢ Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) 0) 0

Tactic:
rfl

Premises used: WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
x : α
⊢ Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) (↑x : WithZero α) : WithZero β)
    ((↑((f : (a : α) → β) x) : WithZero β) : WithZero β)

Tactic:
rfl

Premises used: WithZero.coe, WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
β : Type u_2
inst : MulOneClass β
h :
  ∀ (x : WithZero β),
    Eq (α := WithZero β)
      (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
      ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
⊢ Eq (α := WithZero β →* WithZero β) (↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) (MonoidHom.id (WithZero β))

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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 β)
h₁ :
  ∀ (a : β),
    Eq (α := WithZero β)
      (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) (↑a : WithZero β) :
        WithZero β)
      ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) (↑a : WithZero β) : WithZero β)
⊢ Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) x : WithZero β)

Tactic:
induction x
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
β : Type u_2
inst : MulOneClass β
⊢ Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) 0 : WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) 0 : WithZero β)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
β : Type u_2
inst : MulOneClass β
a : β
⊢ Eq (α := WithZero β)
    (((↑(map' (MonoidHom.id β)) : WithZero β →* WithZero β) : (a : WithZero β) → WithZero β) (↑a : WithZero β) :
      WithZero β)
    ((MonoidHom.id (WithZero β) : (a : WithZero β) → WithZero β) (↑a : WithZero β) : WithZero β)

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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 γ)
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 γ)
⊢ 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 γ)

Tactic:
induction x
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : MulOneClass γ
f : α →* β
g : β →* γ
⊢ 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:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : MulOneClass γ
f : α →* β
g : β →* γ
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:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MulOneClass α
inst_1 : MulOneClass β
inst_2 : MulOneClass γ
f : α →* β
g : β →* γ
⊢ map' (g.comp f) = (map' g).comp (map' f)

Tactic:
MonoidWithZeroHom.ext fun x => (map'_map' f g x).symm

Premises used: MonoidWithZeroHom.ext, Eq.symm, WithZero.map'_map'
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
⊢ Injective.{u_1 + 1, u_2 + 1} (α := WithZero α) (β := WithZero β) (⇑(map' f) : (a : WithZero α) → WithZero β) ↔
    Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
simp [Injective, WithZero.forall]

Premises used: WithZero.forall, Function.Injective
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
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
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := WithZero α) (β := WithZero β) (⇑(map' f) : (a : WithZero α) → WithZero β) ↔
    Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
simp only [Surjective, «forall»]

Premises used: WithZero.forall, Function.Surjective
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
⊢ Eq.{u_2 + 1} (α := WithZero β) ((map' f : (a : WithZero α) → WithZero β) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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
refine_2 :
  ∀ (h : ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b) (b : β),
    ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
⊢ ((∃ (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 ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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 : β
refine_1 :
  ∀ (a : WithZero α) (hab : (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)),
    ∃ (a : α), (f : (a : α) → β) a = b
⊢ ∃ (a : α), (f : (a : α) → β) a = b

Tactic:
obtain ⟨a, hab⟩ := h.2 b

Premises used: And.right
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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
refine_1₁ :
  ∀ (a : α) (hab : (map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α) = (↑b : WithZero β)),
    ∃ (a : α), (f : (a : α) → β) a = b
⊢ ∃ (a : α), (f : (a : α) → β) a = b

Tactic:
induction a using WithZero.recZeroCoe
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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 : β
hab : (map' f : (a : WithZero α) → WithZero β) 0 = (↑b : WithZero β)
⊢ ∃ (a : α), (f : (a : α) → β) a = b

Tactic:
simp at hab
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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 β)
⊢ (f : (a : α) → β) a = b

Tactic:
simp at hab
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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 : (f : (a : α) → β) a = b
⊢ ∃ (a : α), (f : (a : α) → β) a = b

Tactic:
grind
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ (a : α), (f : (a : α) → β) a = b
b : β
refine_2 :
  ∀ (a : α) (ha : (f : (a : α) → β) a = b),
    ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)
⊢ ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)

Tactic:
obtain ⟨a, ha⟩ := h b
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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
h₁ : (map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α) = (↑b : WithZero β)
⊢ ∃ (a : WithZero α), (map' f : (a : WithZero α) → WithZero β) a = (↑b : WithZero β)

Tactic:
use a
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
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
⊢ (map' f : (a : WithZero α) → WithZero β) (↑a : WithZero α) = (↑b : WithZero β)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : One α
inst_1 : Pow α ℕ
a : α
n : ℕ
⊢ (↑(a ^ n) : WithZero α) = (↑a : WithZero α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Monoid α
n : ℕ
simp : HPow.hPow (α := WithZero α) 0 (n + 1) = 0
⊢ HPow.hPow (α := WithZero α) 0 (n + 1) = HPow.hPow (α := WithZero α) 0 n * 0

Tactic:
simp only [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Monoid α
n : ℕ
⊢ HPow.hPow (α := WithZero α) 0 (n + 1) = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ (↑a⁻¹ : WithZero α) = (↑a : WithZero α)⁻¹

Tactic:
rfl

Premises used: WithZero.coe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Inv α
⊢ Eq.{u_1 + 1} (α := WithZero α) 0⁻¹ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : InvOneClass α
⊢ Eq.{u_1 + 1} (α := WithZero α) (↑1⁻¹ : WithZero α) 1

Tactic:
simp