awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
a b : M
fst : ι
snd : α fst
mk : Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
mk₁ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).fst (β := fun (i : ι) ↦ α i))
      (a • (b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd).snd (β := fun (i : ι) ↦ α i))
mk₂ :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst ((a * b) • snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
      (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i))
⊢ (a * b) • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = a • b • Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have mk₃ : Sigma.mk (β := fun (i : ι) ↦ α i) fst (a • b • snd) =
  Sigma.mk (β := fun (i : ι) ↦ α i) ((Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).fst (β := fun (i : ι) ↦ α i))
    (a • (Sigma.mk (β := fun (i : ι) ↦ α i) fst (b • snd)).snd (β := fun (i : ι) ↦ α i))
Tactic: rw [smul_mk, smul_mk, smul_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
x : (i : ι) × α i
⊢ HSMul.hSMul (α := M) 1 x = x
have mk : ∀ (fst : ι) (snd : α fst),
  HSMul.hSMul (α := M) 1 (mk (β := fun (i : ι) ↦ α i) fst snd) = mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
fst : ι
snd : α fst
⊢ HSMul.hSMul (α := M) 1 (mk (β := fun (i : ι) ↦ α i) fst snd) = mk (β := fun (i : ι) ↦ α i) fst snd
have mk : mk (β := fun (i : ι) ↦ α i) fst (HSMul.hSMul.{u_2, u_4, u_4} (α := M) 1 snd) = mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: rw [smul_mk, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sigma (goal)
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst : (i : ι) → MulAction.{u_2, u_4} M (α i)
fst : ι
snd : α fst
mk :
  Sigma.mk (β := fun (i : ι) ↦ α i) fst (HSMul.hSMul.{u_2, u_4, u_4} (α := M) 1 snd) =
    Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
⊢ HSMul.hSMul (α := M) 1 (Sigma.mk (β := fun (i : ι) ↦ α i) fst snd) = Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
have mk₁ : Sigma.mk (β := fun (i : ι) ↦ α i) fst snd = Sigma.mk (β := fun (i : ι) ↦ α i) fst snd
Tactic: rw [smul_mk, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
x : α ⊕ β
⊢ (a • x).swap = a • x.swap
have inl : ∀ (val : α), (HSMul.hSMul (β := α ⊕ β) a (inl val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (inl val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
a : M
x : α ⊕ β
inl : ∀ (val : α), (HSMul.hSMul (β := α ⊕ β) a (Sum.inl val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (Sum.inl val))
⊢ (a • x).swap = a • x.swap
have inr : ∀ (val : β), (HSMul.hSMul (β := α ⊕ β) a (inr val)).swap = HSMul.hSMul (β := β ⊕ α) a (swap (inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x_1 : α ⊕ β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
⊢ (a • b) • x = a • b • x
have inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (a • b) (inl val) = a • HSMul.hSMul (β := α ⊕ β) b (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x_1 : α ⊕ β
inst_4 : SMul M N
inst_5 : IsScalarTower M N α
inst_6 : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (a • b) (Sum.inl val) = a • HSMul.hSMul (β := α ⊕ β) b (Sum.inl val)
⊢ (a • b) • x = a • b • x
have inr : ∀ (val : β), HSMul.hSMul (β := α ⊕ β) (a • b) (inr val) = a • HSMul.hSMul (β := α ⊕ β) b (inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x_1 : α ⊕ β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
a : M
b : N
x : α ⊕ β
⊢ a • b • x = b • a • x
have inl : ∀ (val : α), a • HSMul.hSMul (β := α ⊕ β) b (inl val) = b • HSMul.hSMul (β := α ⊕ β) a (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b_1 : α
c : β
x_1 : α ⊕ β
inst_4 : SMulCommClass M N α
inst_5 : SMulCommClass M N β
a : M
b : N
x : α ⊕ β
inl : ∀ (val : α), a • HSMul.hSMul (β := α ⊕ β) b (Sum.inl val) = b • HSMul.hSMul (β := α ⊕ β) a (Sum.inl val)
⊢ a • b • x = b • a • x
have inr : ∀ (val : β), a • HSMul.hSMul (β := α ⊕ β) b (inr val) = b • HSMul.hSMul (β := α ⊕ β) a (inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b : α
c : β
x_1 : α ⊕ β
inst_4 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_5 : SMul.{u_1, u_4} Mᵐᵒᵖ β
inst_6 : IsCentralScalar M α
inst_7 : IsCentralScalar M β
a : M
x : α ⊕ β
⊢ MulOpposite.op a • x = a • x
have inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (inl val) = HSMul.hSMul (β := α ⊕ β) a (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul M α
inst_1 : SMul M β
inst_2 : SMul N α
inst_3 : SMul N β
a_1 : M
b : α
c : β
x_1 : α ⊕ β
inst_4 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_5 : SMul.{u_1, u_4} Mᵐᵒᵖ β
inst_6 : IsCentralScalar M α
inst_7 : IsCentralScalar M β
a : M
x : α ⊕ β
inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (Sum.inl val) = HSMul.hSMul (β := α ⊕ β) a (Sum.inl val)
⊢ MulOpposite.op a • x = a • x
have inr : ∀ (val : β), HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (inr val) = HSMul.hSMul (β := α ⊕ β) a (inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst : MulAction M α
inst_1 : MulAction M β
a b : M
x : α ⊕ β
⊢ (a * b) • x = a • b • x
have inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (a * b) (inl val) = a • HSMul.hSMul (β := α ⊕ β) b (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst : MulAction M α
inst_1 : MulAction M β
a b : M
x : α ⊕ β
inl : ∀ (val : α), HSMul.hSMul (β := α ⊕ β) (a * b) (Sum.inl val) = a • HSMul.hSMul (β := α ⊕ β) b (Sum.inl val)
⊢ (a * b) • x = a • b • x
have inr : ∀ (val : β), HSMul.hSMul (β := α ⊕ β) (a * b) (inr val) = a • HSMul.hSMul (β := α ⊕ β) b (inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst : MulAction M α
inst_1 : MulAction M β
x : α ⊕ β
⊢ HSMul.hSMul (α := M) 1 x = x
have inl : ∀ (val : α), HSMul.hSMul (α := M) (β := α ⊕ β) 1 (inl val) = inl val
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Sum (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst : MulAction M α
inst_1 : MulAction M β
x : α ⊕ β
inl : ∀ (val : α), HSMul.hSMul (α := M) (β := α ⊕ β) 1 (Sum.inl val) = Sum.inl val
⊢ HSMul.hSMul (α := M) 1 x = x
have inr : ∀ (val : β), HSMul.hSMul (α := M) (β := α ⊕ β) 1 (inr val) = inr val
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
⊢ g • (↑m : M) * g⁻¹ • (↑m⁻¹ : M) = 1
have rw : (g * g⁻¹) • ((↑m : M) * (↑m⁻¹ : M)) = 1
Tactic: rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
rw : (g * g⁻¹) • ((↑m : M) * (↑m⁻¹ : M)) = 1
⊢ g • (↑m : M) * g⁻¹ • (↑m⁻¹ : M) = 1
have rw₁ : HSMul.hSMul (β := M) (g * g⁻¹) 1 = 1
Tactic: rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
rw : (g * g⁻¹) • ((↑m : M) * (↑m⁻¹ : M)) = 1
rw₁ : HSMul.hSMul (β := M) (g * g⁻¹) 1 = 1
⊢ g • (↑m : M) * g⁻¹ • (↑m⁻¹ : M) = 1
have rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := G) (β := M) 1 1 = 1
Tactic: rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
rw : (g * g⁻¹) • ((↑m : M) * (↑m⁻¹ : M)) = 1
rw₁ : HSMul.hSMul (β := M) (g * g⁻¹) 1 = 1
rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := G) (β := M) 1 1 = 1
⊢ g • (↑m : M) * g⁻¹ • (↑m⁻¹ : M) = 1
have rw₃ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • (↑m⁻¹ : M) * g • (↑m : M) = 1
have rw : (g⁻¹ * g) • ((↑m⁻¹ : M) * (↑m : M)) = 1
Tactic: rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
rw : (g⁻¹ * g) • ((↑m⁻¹ : M) * (↑m : M)) = 1
⊢ g⁻¹ • (↑m⁻¹ : M) * g • (↑m : M) = 1
have rw₁ : HSMul.hSMul (β := M) (g⁻¹ * g) 1 = 1
Tactic: rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
rw : (g⁻¹ * g) • ((↑m⁻¹ : M) * (↑m : M)) = 1
rw₁ : HSMul.hSMul (β := M) (g⁻¹ * g) 1 = 1
⊢ g⁻¹ • (↑m⁻¹ : M) * g • (↑m : M) = 1
have rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := G) (β := M) 1 1 = 1
Tactic: rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
g : G
m : Mˣ
rw : (g⁻¹ * g) • ((↑m⁻¹ : M) * (↑m : M)) = 1
rw₁ : HSMul.hSMul (β := M) (g⁻¹ * g) 1 = 1
rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := G) (β := M) 1 1 = 1
⊢ g⁻¹ • (↑m⁻¹ : M) * g • (↑m : M) = 1
have rw₃ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
G : Type u_1
H : Type u_2
M_1 : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst : CommMonoid M
⊢ Eq.{u_6 + 1} (α := SMul Mˣ Mˣ) (@SemigroupAction.toSMul _ _ Monoid.toSemigroup _) instSMulOfMul
have smul : ∀ (x x_1 : Mˣ), (↑(SMul.smul x x_1) : M) = (↑(SMul.smul x x_1) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Action.Units (goal)
Goal:
M : Type u_6
inst : CommMonoid M
u₁ u₂ : Mˣ
⊢ u₁ • u₂ = u₁ * u₂
have huv : (↑(u₁ • u₂) : M) = (↑(u₁ * u₂) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst : AddMonoid A
inst_1 : AddMonoid B
inst_2 : Monoid M
inst_3 : Monoid N
ψ_1 φ ψ : AddChar A M
h : φ.toFun = ψ.toFun
⊢ φ = ψ
have mk : ∀ (toFun : A → M) (map_zero_eq_one' : toFun 0 = 1) (map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b)
  (h :
    { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M }.toFun =
      ψ.toFun),
  { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M } = ψ
Tactic: cases φ
Cleared hypotheses: φ, h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst : AddMonoid A
inst_1 : AddMonoid B
inst_2 : Monoid M
inst_3 : Monoid N
ψ_1 ψ : AddChar A M
toFun : A → M
map_zero_eq_one' : toFun 0 = 1
map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b
h :
  { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M }.toFun =
    ψ.toFun
⊢ { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M } = ψ
have mk : ∀ (toFun_1 : A → M) (map_zero_eq_one'_1 : toFun_1 0 = 1)
  (map_add_eq_mul'_1 : ∀ (a b : A), toFun_1 (a + b) = toFun_1 a * toFun_1 b)
  (h :
    { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M }.toFun =
      { toFun := toFun_1, map_zero_eq_one' := map_zero_eq_one'_1, map_add_eq_mul' := map_add_eq_mul'_1 :
          AddChar A M }.toFun),
  { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M } =
    { toFun := toFun_1, map_zero_eq_one' := map_zero_eq_one'_1, map_add_eq_mul' := map_add_eq_mul'_1 }
Tactic: cases ψ
Cleared hypotheses: ψ, h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ Eq (α := (a : A) → M) (⇑ψ : (a : A) → M) 1 ↔ ψ = 0
have rw : Eq (α := (a : A) → M) (⇑ψ : (a : A) → M) (⇑0 : (a : A) → M) ↔ ψ = 0
Tactic: rw [← coe_zero, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
rw : Eq (α := (a : A) → M) (⇑ψ : (a : A) → M) (⇑0 : (a : A) → M) ↔ ψ = 0
⊢ Eq (α := (a : A) → M) (⇑ψ : (a : A) → M) 1 ↔ ψ = 0
have rw₁ : ψ = 0 ↔ ψ = 0
Tactic: rw [← coe_zero, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_3
N : Type u_4
inst : AddMonoid A
inst_1 : Monoid M
inst_2 : Monoid N
ψ : AddChar A M
hψ : Surjective.{u_1 + 1, u_3 + 1} (α := A) (β := M) (⇑ψ : (a : A) → M)
f g : M →* N
h : Eq (α := AddChar A N) ((fun (f : M →* N) ↦ f.compAddChar ψ) f) ((fun (f : M →* N) ↦ f.compAddChar ψ) g)
⊢ f = g
have rw : ∀
  (h :
    Eq (α := (a : A) → N) (⇑((fun (f : M →* N) ↦ f.compAddChar ψ) f) : (a : A) → N)
      (⇑((fun (f : M →* N) ↦ f.compAddChar ψ) g) : (a : A) → N)),
  Eq (α := (a : M) → N) (⇑f : (a : M) → N) (⇑g : (a : M) → N)
Tactic: rw [DFunLike.ext'_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
B : Type u_2
M : Type u_3
N : Type u_4
inst : AddMonoid B
inst_1 : Monoid M
inst_2 : Monoid N
f : M →* N
hf : Injective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
ψ χ : AddChar B M
h : Eq (α := AddChar B N) ((fun (ψ : AddChar B M) ↦ f.compAddChar ψ) ψ) ((fun (ψ : AddChar B M) ↦ f.compAddChar ψ) χ)
⊢ ψ = χ
have rw : ∀
  (h :
    Eq (α := (a : B) → N) (⇑((fun (ψ : AddChar B M) ↦ f.compAddChar ψ) ψ) : (a : B) → N)
      (⇑((fun (ψ : AddChar B M) ↦ f.compAddChar ψ) χ) : (a : B) → N)),
  Eq (α := (a : B) → M) (⇑ψ : (a : B) → M) (⇑χ : (a : B) → M)
Tactic: rw [DFunLike.ext'_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : AddMonoid B
inst_2 : Monoid M
f : A →+ B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
ψ χ : AddChar B M
h :
  Eq (α := AddChar A M) ((fun (ψ : AddChar B M) ↦ ψ.compAddMonoidHom f) ψ)
    ((fun (ψ : AddChar B M) ↦ ψ.compAddMonoidHom f) χ)
⊢ ψ = χ
have rw : ∀
  (h :
    Eq (α := (a : A) → M) (⇑((fun (ψ : AddChar B M) ↦ ψ.compAddMonoidHom f) ψ) : (a : A) → M)
      (⇑((fun (ψ : AddChar B M) ↦ ψ.compAddMonoidHom f) χ) : (a : A) → M)),
  Eq (α := (a : B) → M) (⇑ψ : (a : B) → M) (⇑χ : (a : B) → M)
Tactic: rw [DFunLike.ext'_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : AddMonoid B
inst_2 : Monoid M
ψ : AddChar B M
hψ : Injective.{u_2 + 1, u_3 + 1} (α := B) (β := M) (⇑ψ : (a : B) → M)
f g : A →+ B
h : Eq (α := AddChar A M) ((fun (f : A →+ B) ↦ ψ.compAddMonoidHom f) f) ((fun (f : A →+ B) ↦ ψ.compAddMonoidHom f) g)
⊢ f = g
have rw : ∀
  (h :
    Eq (α := (a : A) → M) (⇑((fun (f : A →+ B) ↦ ψ.compAddMonoidHom f) f) : (a : A) → M)
      (⇑((fun (f : A →+ B) ↦ ψ.compAddMonoidHom f) g) : (a : A) → M)),
  Eq (α := (a : A) → B) (⇑f : (a : A) → B) (⇑g : (a : A) → B)
Tactic: rw [DFunLike.ext'_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ Eq (α := (a : A) → M) (⇑(∏ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M))
have empty : Eq (α := (a : A) → M) (⇑(∏ i ∈ ∅, ψ i) : (a : A) → M) (∏ i ∈ ∅, (⇑(ψ i) : (a : A) → M))
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
empty : Eq (α := (a : A) → M) (⇑(∏ i ∈ ∅, ψ i) : (a : A) → M) (∏ i ∈ ∅, (⇑(ψ i) : (a : A) → M))
⊢ Eq (α := (a : A) → M) (⇑(∏ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M))
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  Eq (α := (a : A) → M) (⇑(∏ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M)) →
    Eq (α := (a : A) → M) (⇑(∏ i ∈ cons a s h, ψ i) : (a : A) → M) (∏ i ∈ cons a s h, (⇑(ψ i) : (a : A) → M))
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ Eq (α := (a : A) → M) (⇑(∑ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M))
have empty : Eq (α := (a : A) → M) (⇑(∑ i ∈ ∅, ψ i) : (a : A) → M) (∏ i ∈ ∅, (⇑(ψ i) : (a : A) → M))
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
empty : Eq (α := (a : A) → M) (⇑(∑ i ∈ ∅, ψ i) : (a : A) → M) (∏ i ∈ ∅, (⇑(ψ i) : (a : A) → M))
⊢ Eq (α := (a : A) → M) (⇑(∑ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M))
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  Eq (α := (a : A) → M) (⇑(∑ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M)) →
    Eq (α := (a : A) → M) (⇑(∑ i ∈ cons a s h, ψ i) : (a : A) → M) (∏ i ∈ cons a s h, (⇑(ψ i) : (a : A) → M))
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ Eq.{u_3 + 1} (α := M) ((∏ i ∈ s, ψ i : (a : A) → M) a : M) (∏ i ∈ s, (ψ i : (a : A) → M) a : M)
have rw : Eq.{u_3 + 1} (α := M) ((∏ i ∈ s, (⇑(ψ i) : (a : A) → M)) a) (∏ i ∈ s, (ψ i : (a : A) → M) a)
Tactic: rw [coe_prod, Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
rw : Eq.{u_3 + 1} (α := M) ((∏ i ∈ s, (⇑(ψ i) : (a : A) → M)) a) (∏ i ∈ s, (ψ i : (a : A) → M) a)
⊢ Eq.{u_3 + 1} (α := M) ((∏ i ∈ s, ψ i : (a : A) → M) a : M) (∏ i ∈ s, (ψ i : (a : A) → M) a : M)
have rw₁ : Eq.{u_3 + 1} (α := M) (∏ c ∈ s, (ψ c : (a : A) → M) a) (∏ i ∈ s, (ψ i : (a : A) → M) a)
Tactic: rw [coe_prod, Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ Eq.{u_3 + 1} (α := M) ((∑ i ∈ s, ψ i : (a : A) → M) a : M) (∏ i ∈ s, (ψ i : (a : A) → M) a : M)
have rw : Eq.{u_3 + 1} (α := M) ((∏ i ∈ s, (⇑(ψ i) : (a : A) → M)) a) (∏ i ∈ s, (ψ i : (a : A) → M) a)
Tactic: rw [coe_sum, Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
rw : Eq.{u_3 + 1} (α := M) ((∏ i ∈ s, (⇑(ψ i) : (a : A) → M)) a) (∏ i ∈ s, (ψ i : (a : A) → M) a)
⊢ Eq.{u_3 + 1} (α := M) ((∑ i ∈ s, ψ i : (a : A) → M) a : M) (∏ i ∈ s, (ψ i : (a : A) → M) a : M)
have rw₁ : Eq.{u_3 + 1} (α := M) (∏ c ∈ s, (ψ c : (a : A) → M) a) (∏ i ∈ s, (ψ i : (a : A) → M) a)
Tactic: rw [coe_sum, Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
⊢ Eq (α := AddChar (AddChar A M) M)
    { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } 0
have h : ∀ (x : AddChar A M),
  Eq.{u_3 + 1} (α := M)
    (({ toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) 0, map_zero_eq_one' := sorry, map_add_eq_mul' := sorry } :
          (a : AddChar A M) → M)
        x :
      M)
    ((0 : (a : AddChar A M) → M) x : M)
Tactic: ext