awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
⊢ (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 β)))
      ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
          { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
            map_mul' := ⋯ : α ≃* β })
        x) =
    x
have h : ∀ (x_1 : WithZero α),
  Eq.{u_2 + 1} (α := WithZero β)
    ((((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 β)))
              ((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 : α ≃* β })
                x) :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
          (a : WithZero α) → WithZero β)
        x_1 :
      WithZero β)
    ((x : (a : WithZero α) → WithZero β) x_1 : WithZero β)
Tactic: ext x
-- 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_1 : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : WithZero α
⊢ Eq.{u_2 + 1} (α := WithZero β)
    ((((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 β)))
              ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                  { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                    map_mul' := ⋯ : α ≃* β })
                x_1) :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
          (a : WithZero α) → WithZero β)
        x :
      WithZero β)
    ((x_1 : (a : WithZero α) → WithZero β) x : WithZero β)
have h : Eq.{u_2 + 1} (α := WithZero β)
  ((((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 β)))
          ((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 : α ≃* β })
            x_1) :
        MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
      (a : WithZero α) → WithZero β)
    0)
  ((x_1 : (a : WithZero α) → WithZero β) 0)
Tactic: cases 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 : Group α
inst_1 : Group β
x_1 : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : WithZero α
h :
  Eq.{u_2 + 1} (α := WithZero β)
    ((((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 β)))
            ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ : α ≃* β })
              x_1) :
          MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
        (a : WithZero α) → WithZero β)
      0)
    ((x_1 : (a : WithZero α) → WithZero β) 0)
⊢ Eq.{u_2 + 1} (α := WithZero β)
    ((((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 β)))
              ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                  { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                    map_mul' := ⋯ : α ≃* β })
                x_1) :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
          (a : WithZero α) → WithZero β)
        x :
      WithZero β)
    ((x_1 : (a : WithZero α) → WithZero β) x : WithZero β)
have h₁ : ∀ (a : α),
  Eq.{u_2 + 1} (α := WithZero β)
    ((((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 β)))
              ((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 : α ≃* β })
                x_1) :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
          (a : WithZero α) → WithZero β)
        (↑a : WithZero α) :
      WithZero β)
    ((x_1 : (a : WithZero α) → WithZero β) (↑a : WithZero α) : WithZero β)
Tactic: cases 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 : AddMonoidWithOne α
n : ℕ
⊢ (if n + 1 = 0 then 0 else (↑(↑(n + 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if n = 0 then 0 else (↑(↑n : α) : WithZero α)) 1
have zero : (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else (↑(↑(HAdd.hAdd (α := ℕ) 0 1) : α) : WithZero α)) =
  HAdd.hAdd (α := WithZero α) (if Eq (α := ℕ) 0 0 then 0 else (↑(↑0 : α) : WithZero α)) 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : AddMonoidWithOne α
n : ℕ
zero :
  (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else (↑(↑(HAdd.hAdd (α := ℕ) 0 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if Eq (α := ℕ) 0 0 then 0 else (↑(↑0 : α) : WithZero α)) 1
⊢ (if n + 1 = 0 then 0 else (↑(↑(n + 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if n = 0 then 0 else (↑(↑n : α) : WithZero α)) 1
have succ : ∀ (n : ℕ),
  (if n + 1 + 1 = 0 then 0 else (↑(↑(n + 1 + 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if n + 1 = 0 then 0 else (↑(↑(n + 1) : α) : WithZero α)) 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M : Type u_4
inst : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
⊢ exp x.log = x
have lift : ∀ (x : Multiplicative M), exp (↑x : WithZero (Multiplicative M)).log = (↑x : WithZero (Multiplicative M))
Tactic: lift x to Multiplicative M using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M : Type u_4
inst : AddMonoid M
x : M
⊢ exp x = 1 ↔ x = 0
have rw : exp x = exp 0 ↔ x = 0
Tactic: rw [← exp_zero, exp_inj]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M : Type u_4
inst : AddMonoid M
x : M
rw : exp x = exp 0 ↔ x = 0
⊢ exp x = 1 ↔ x = 0
have rw₁ : x = 0 ↔ x = 0
Tactic: rw [← exp_zero, exp_inj]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M : Type u_4
inst : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).log = x.log + y.log
have lift : ∀ (x : Multiplicative M), ((↑x : WithZero (Multiplicative M)) * y).log = (↑x : WithZero (Multiplicative M)).log + y.log
Tactic: lift x to Multiplicative M using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M : Type u_4
inst : AddMonoid M
y : WithZero (Multiplicative M)
hy : y ≠ 0
x : Multiplicative M
⊢ ((↑x : WithZero (Multiplicative M)) * y).log = (↑x : WithZero (Multiplicative M)).log + y.log
have lift : ∀ (y : Multiplicative M),
  ((↑x : WithZero (Multiplicative M)) * (↑y : WithZero (Multiplicative M))).log =
    (↑x : WithZero (Multiplicative M)).log + (↑y : WithZero (Multiplicative M)).log
Tactic: lift y to Multiplicative M using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x : (WithZero (Multiplicative G))ˣ
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) x = (↑x : WithZero (Multiplicative G)).log
have none : ∀ (hab hba : HMul.hMul (α := WithZero (Multiplicative G)) none none = 1),
  (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := none, inv := none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := none, inv := none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log
Tactic: obtain ⟨_ | a, _ | b, hab, hba⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x : (WithZero (Multiplicative G))ˣ
none :
  ∀ (hab hba : HMul.hMul (α := WithZero (Multiplicative G)) Option.none Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) x = (↑x : WithZero (Multiplicative G)).log
have none₁ : ∀ (b : Multiplicative G) (hab : Option.none * some b = 1) (hba : some b * Option.none = 1),
  (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := Option.none, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := Option.none, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log
Tactic: obtain ⟨_ | a, _ | b, hab, hba⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x : (WithZero (Multiplicative G))ˣ
none :
  ∀ (hab hba : HMul.hMul (α := WithZero (Multiplicative G)) Option.none Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
none₁ :
  ∀ (b : Multiplicative G) (hab : Option.none * some b = 1) (hba : some b * Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) x = (↑x : WithZero (Multiplicative G)).log
have some : ∀ (a : Multiplicative G) (hab : some a * Option.none = 1) (hba : Option.none * some a = 1),
  (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := some a, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := some a, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log
Tactic: obtain ⟨_ | a, _ | b, hab, hba⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x : (WithZero (Multiplicative G))ˣ
none :
  ∀ (hab hba : HMul.hMul (α := WithZero (Multiplicative G)) Option.none Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
none₁ :
  ∀ (b : Multiplicative G) (hab : Option.none * Option.some b = 1) (hba : Option.some b * Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := Option.some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := Option.some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
some :
  ∀ (a : Multiplicative G) (hab : Option.some a * Option.none = 1) (hba : Option.none * Option.some a = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.some a, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.some a, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) x = (↑x : WithZero (Multiplicative G)).log
have some₁ : ∀ (a b : Multiplicative G) (hab : Option.some a * Option.some b = 1) (hba : Option.some b * Option.some a = 1),
  (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := Option.some a, inv := Option.some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := Option.some a, inv := Option.some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log
Tactic: obtain ⟨_ | a, _ | b, hab, hba⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).log = x.log - y.log
have lift : ∀ (x : Multiplicative G), ((↑x : WithZero (Multiplicative G)) / y).log = (↑x : WithZero (Multiplicative G)).log - y.log
Tactic: lift x to Multiplicative G using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
⊢ ((↑x : WithZero (Multiplicative G)) / y).log = (↑x : WithZero (Multiplicative G)).log - y.log
have lift : ∀ (y : Multiplicative G),
  ((↑x : WithZero (Multiplicative G)) / (↑y : WithZero (Multiplicative G))).log =
    (↑x : WithZero (Multiplicative G)).log - (↑y : WithZero (Multiplicative G)).log
Tactic: lift y to Multiplicative G using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x : WithZero (Multiplicative G)
n : ℤ
⊢ (x ^ n).log = n • x.log
have ofNat : ∀ (a : ℕ), (x ^ Int.ofNat a).log = Int.ofNat a • x.log
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G : Type u_5
inst : AddGroup G
x : WithZero (Multiplicative G)
n : ℤ
ofNat : ∀ (a : ℕ), (x ^ Int.ofNat a).log = Int.ofNat a • x.log
⊢ (x ^ n).log = n • x.log
have negSucc : ∀ (a : ℕ), (x ^ Int.negSucc a).log = Int.negSucc a • x.log
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀) ↔ x = 0
have refine : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀) → x = 0
Tactic: refine ⟨?_, by simp +contextual⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀) → x = 0
have contrapose! : x ≠ 0 → Ne.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
hx : x ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀)
⊢ False
have lift : ∀ (x : G₀ˣ) (hx : (↑x : G₀) ≠ 0) (H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)), False
Tactic: lift x to G₀ˣ using isUnit_iff_ne_zero.mpr hx
Cleared hypotheses: x, hx, H
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
⊢ False
have apply : Eq.{u_2 + 1} (α := M₀) 1 0
Tactic: apply one_ne_zero (α := M₀)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
⊢ Eq.{u_2 + 1} (α := M₀) 1 0
have rw : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 1 : M₀) (0 : M₀)
Tactic: rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
rw : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 1 : M₀) (0 : M₀)
⊢ Eq.{u_2 + 1} (α := M₀) 1 0
have rw₁ : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) ((↑x : G₀) * (↑x⁻¹ : G₀)) : M₀) (0 : M₀)
Tactic: rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
rw : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 1 : M₀) (0 : M₀)
rw₁ : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) ((↑x : G₀) * (↑x⁻¹ : G₀)) : M₀) (0 : M₀)
⊢ Eq.{u_2 + 1} (α := M₀) 1 0
have rw₂ : HMul.hMul (α := M₀) (β := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
Tactic: rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
rw : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 1 : M₀) (0 : M₀)
rw₁ : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) ((↑x : G₀) * (↑x⁻¹ : G₀)) : M₀) (0 : M₀)
rw₂ : HMul.hMul (α := M₀) (β := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
⊢ Eq.{u_2 + 1} (α := M₀) 1 0
have rw₃ : HMul.hMul (α := M₀) (β := M₀) (0 : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
Tactic: rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
rw : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 1 : M₀) (0 : M₀)
rw₁ : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) ((↑x : G₀) * (↑x⁻¹ : G₀)) : M₀) (0 : M₀)
rw₂ : HMul.hMul (α := M₀) (β := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
rw₃ : HMul.hMul (α := M₀) (β := M₀) (0 : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
⊢ Eq.{u_2 + 1} (α := M₀) 1 0
have rw₄ : Eq.{u_2 + 1} (α := M₀) 0 0
Tactic: rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inl : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (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.WithZero (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
inl : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) 0 : N₀) : G₀) ((1 : (a : M₀) → G₀) 0 : G₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inr : ∀ (hx : x ≠ 0),
  Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (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.WithZero (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inr : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) ((1 : (a : M₀) → G₀) x : G₀)
Tactic: rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
inr : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) ((1 : (a : M₀) → G₀) x : G₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inr₁ : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) (1 : G₀)
Tactic: rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]