awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Sum
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)
inr : ∀ (val : β), HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (Sum.inr val) = HSMul.hSMul (β := α ⊕ β) a (Sum.inr val)
⊢ MulOpposite.op a • x = a • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sum
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 : α ⊕ β
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
val : α
⊢ HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (inl val) = HSMul.hSMul (β := α ⊕ β) a (inl val)

Tactic:
congr_arg inl (op_smul_eq_smul _ _)

Premises used: Sum.map, Sum.inl, congr_arg, IsCentralScalar.op_smul_eq_smul, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
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 : α ⊕ β
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
val : β
⊢ HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (inr val) = HSMul.hSMul (β := α ⊕ β) a (inr val)

Tactic:
congr_arg inr (op_smul_eq_smul _ _)

Premises used: Sum.map, congr_arg, Sum.inr, IsCentralScalar.op_smul_eq_smul, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
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 : α ⊕ β
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
val : α
⊢ HSMul.hSMul (β := α ⊕ β) (MulOpposite.op a) (inl val) = HSMul.hSMul (β := α ⊕ β) a (inl val)

Tactic:
exacts [congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]

Premises used: Sum.inl, congr_arg, Sum.inr, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Sum
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 : α ⊕ β
inst_4 : FaithfulSMul M α
m₁ m₂ : M
h : ∀ (a : α ⊕ β), m₁ • a = m₂ • a
a : α
⊢ m₁ • a = m₂ • a

Tactic:
injection h (inl a)

Premises used: Sum.inl
-- Module: Mathlib.Algebra.Group.Action.Sum
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 : M
b_1 : α
c : β
x : α ⊕ β
inst_4 : FaithfulSMul M β
m₁ m₂ : M
h : ∀ (a : α ⊕ β), m₁ • a = m₂ • a
b : β
⊢ m₁ • b = m₂ • b

Tactic:
injection h (inr b)

Premises used: Sum.inr
-- Module: Mathlib.Algebra.Group.Action.Sum
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)
inr : ∀ (val : β), HSMul.hSMul (β := α ⊕ β) (a * b) (Sum.inr val) = a • HSMul.hSMul (β := α ⊕ β) b (Sum.inr val)
⊢ (a * b) • x = a • b • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sum
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
val : α
⊢ HSMul.hSMul (β := α ⊕ β) (a * b) (inl val) = a • HSMul.hSMul (β := α ⊕ β) b (inl val)

Tactic:
congr_arg inl (mul_smul _ _ _)

Premises used: Sum.map, Sum.inl, congr_arg, SemigroupAction.mul_smul, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
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
val : β
⊢ HSMul.hSMul (β := α ⊕ β) (a * b) (inr val) = a • HSMul.hSMul (β := α ⊕ β) b (inr val)

Tactic:
congr_arg inr (mul_smul _ _ _)

Premises used: Sum.map, congr_arg, Sum.inr, SemigroupAction.mul_smul, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
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
val : α
⊢ HSMul.hSMul (β := α ⊕ β) (a * b) (inl val) = a • HSMul.hSMul (β := α ⊕ β) b (inl val)

Tactic:
exacts [congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)]

Premises used: Sum.inl, congr_arg, Sum.inr, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Sum
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
inr : ∀ (val : β), HSMul.hSMul (α := M) (β := α ⊕ β) 1 (Sum.inr val) = Sum.inr val
⊢ HSMul.hSMul (α := M) 1 x = x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Sum
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 β
val : α
⊢ HSMul.hSMul (α := M) (β := α ⊕ β) 1 (inl val) = inl val

Tactic:
congr_arg inl (one_smul _ _)

Premises used: Sum.map, Sum.inl, one_smul, congr_arg, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
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 β
val : β
⊢ HSMul.hSMul (α := M) (β := α ⊕ β) 1 (inr val) = inr val

Tactic:
congr_arg inr (one_smul _ _)

Premises used: Sum.map, one_smul, congr_arg, Sum.inr, Sum.elim
-- Module: Mathlib.Algebra.Group.Action.Sum
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 β
val : α
⊢ HSMul.hSMul (α := M) (β := α ⊕ β) 1 (inl val) = inl val

Tactic:
exacts [congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)]

Premises used: Sum.inl, one_smul, congr_arg, Sum.inr
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid M
e : α ≃ β
inst_1 : MulAction M β
⊢ ∀ (x y : M) (b : α), (x * y) • b = x • y • b

Tactic:
simp [smul_def, mul_smul]

Premises used: Equiv.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid M
e : α ≃ β
inst_1 : MulAction M β
⊢ ∀ (b : α), HSMul.hSMul.{u_1, u_4, u_4} (α := M) 1 b = b

Tactic:
simp [smul_def]

Premises used: Equiv.smul_def
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
N : Type u_2
α : Type u_4
β : Type u_5
inst : SMul M β
inst_1 : SMul N β
e : α ≃ β
inst_2 : SMulCommClass M N β
this_1 : SMul M α := Equiv.smul M e
this : SMul N α := Equiv.smul N e
⊢ ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a

Tactic:
simp [smul_def, smul_comm]

Premises used: Equiv.smul_def, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
N : Type u_2
α : Type u_4
β : Type u_5
inst : SMul M N
inst_1 : SMul M β
inst_2 : SMul N β
e : α ≃ β
inst_3 : IsScalarTower M N β
this_1 : SMul M α := Equiv.smul M e
this : SMul N α := Equiv.smul N e
⊢ ∀ (x : M) (y : N) (z : α), (x • y) • z = x • y • z

Tactic:
simp [smul_def, smul_assoc]

Premises used: smul_assoc, Equiv.smul_def
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
α : Type u_4
β : Type u_5
inst : SMul M β
inst_1 : SMul.{u_1, u_5} Mᵐᵒᵖ β
e : α ≃ β
inst_2 : IsCentralScalar M β
this_1 : SMul M α := Equiv.smul M e
this : SMul.{u_1, u_4} Mᵐᵒᵖ α := Equiv.smul Mᵐᵒᵖ e
⊢ ∀ (m : M) (a : α), MulOpposite.op m • a = m • a

Tactic:
simp [smul_def, op_smul_eq_smul]

Premises used: Equiv.smul_def, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid M
inst_1 : Monoid O
e : N ≃ O
inst_2 : MulDistribMulAction M O
this : Monoid N := e.monoid
⊢ ∀ (r : M), HSMul.hSMul (β := N) r 1 = 1

Tactic:
simp [one_def, smul_def, smul_one]

Premises used: Equiv.smul_def, MulDistribMulAction.smul_one, Equiv.one_def
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid M
inst_1 : Monoid O
e : N ≃ O
inst_2 : MulDistribMulAction M O
this : Monoid N := e.monoid
⊢ ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y

Tactic:
simp [mul_def, smul_def, smul_mul']

Premises used: Equiv.smul_def, Equiv.mul_def, smul_mul'
-- Module: Mathlib.Algebra.Group.Action.TransferInstance
Goal:
M : Type u_1
α : Type u_4
β : Type u_5
inst : SMul M β
e : α ≃ β
inst_1 : FaithfulSMul M β
this : SMul M α := Equiv.smul M e
m₁ m₂ : M
⊢ (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simpa [← e.forall_congr_right, smul_def] using eq_of_smul_eq_smul (α := β)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, Equiv.smul_def, Equiv.forall_congr_right
-- Module: Mathlib.Algebra.Group.Action.TypeTags
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : Additive α
b : β
⊢ HSMul.hSMul (α := α) ((toMul : (a : Additive α) → α) a : α) b = a +ᵥ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.TypeTags
Goal:
α : Type u_2
β : Type u_3
inst : SMul α β
a : α
b : β
⊢ HVAdd.hVAdd (α := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α) b = a • b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.TypeTags
Goal:
α : Type u_2
β : Type u_3
inst : VAdd α β
a : Multiplicative α
b : β
⊢ HVAdd.hVAdd (α := α) ((toAdd : (a : Multiplicative α) → α) a : α) b = a • b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.TypeTags
Goal:
α : Type u_2
β : Type u_3
inst : VAdd α β
a : α
b : β
⊢ HSMul.hSMul (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) b = a +ᵥ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.TypeTags
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SMul α γ
inst_1 : SMul β γ
inst_2 : SMulCommClass α β γ
⊢ VAddCommClass.{u_2, u_3, u_4} (Additive α) (Additive β) γ

Tactic:
⟨@smul_comm α β _ _ _ _⟩

Premises used: VAddCommClass.mk, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Group.Action.TypeTags
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : VAdd α γ
inst_1 : VAdd β γ
inst_2 : VAddCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} (Multiplicative α) (Multiplicative β) γ

Tactic:
⟨@vadd_comm α β _ _ _ _⟩

Premises used: VAddCommClass.vadd_comm, SMulCommClass.mk
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_3
α : Type u_5
inst : Monoid M
inst_1 : SMul M α
m : Mˣ
a : α
⊢ m • a = (↑m : M) • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_6
α : Type u_7
inst : Monoid M
inst_1 : SMul M α
m n : M
h₁ : m * n = 1
h₂ : n * m = 1
a : α
⊢ { val := m, inv := n, val_inv := h₁, inv_val := h₂ : Mˣ } • a = m • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_3
α : Type u_5
inst : Monoid M
inst_1 : SMul M α
m : M
hm : IsUnit m
a : α
⊢ hm.unit • a = m • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
α : Type u_5
inst : Monoid α
a : α
h : IsUnit a
⊢ h.unit⁻¹ • a = 1

Tactic:
h.val_inv_mul

Premises used: IsUnit.val_inv_mul
-- Module: Mathlib.Algebra.Group.Action.Units
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
rw₃ rw₄ : Eq.{u_3 + 1} (α := M) 1 1
⊢ g • (↑m : M) * g⁻¹ • (↑m⁻¹ : M) = 1

Tactic:
rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]

Premises used: Units.mul_inv, smul_mul_smul_comm, one_smul, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Action.Units
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
rw₃ rw₄ : Eq.{u_3 + 1} (α := M) 1 1
⊢ g⁻¹ • (↑m⁻¹ : M) * g • (↑m : M) = 1

Tactic:
rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, Units.inv_mul, smul_mul_smul_comm, one_smul
-- Module: Mathlib.Algebra.Group.Action.Units
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
smul : ∀ (x x_1 : Mˣ), (↑(SMul.smul x x_1) : M) = (↑(SMul.smul x x_1) : M)
⊢ Eq.{u_6 + 1} (α := SMul Mˣ Mˣ) (@SemigroupAction.toSMul _ _ Monoid.toSemigroup _) instSMulOfMul

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Units
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
x x_1 : Mˣ
⊢ (↑(SMul.smul x x_1) : M) = (↑(SMul.smul x x_1) : M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_6
inst : CommMonoid M
u₁ u₂ : Mˣ
huv : (↑(u₁ • u₂) : M) = (↑(u₁ * u₂) : M)
⊢ u₁ • u₂ = u₁ * u₂

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_6
inst : CommMonoid M
u₁ u₂ : Mˣ
⊢ (↑(u₁ • u₂) : M) = (↑(u₁ * u₂) : M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
G : Type u_1
M : Type u_3
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)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
G : Type u_1
M : Type u_3
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)⁻¹ = g⁻¹ • m⁻¹

Tactic:
ext rfl

Premises used: Units.ext, rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
G : Type u_1
H : Type u_2
M_1 : Type u_3
N_1 : Type u_4
α : Type u_5
M : Type u_6
N : Type u_7
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulDistribMulAction M N
m : M
u : Nˣ
⊢ m • (↑u : N) * m • (↑u⁻¹ : N) = 1

Tactic:
simp [← smul_mul', smul_one]

Premises used: MulDistribMulAction.smul_one, smul_mul'
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
G : Type u_1
H : Type u_2
M_1 : Type u_3
N_1 : Type u_4
α : Type u_5
M : Type u_6
N : Type u_7
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulDistribMulAction M N
m : M
u : Nˣ
⊢ m • (↑u⁻¹ : N) * m • (↑u : N) = 1

Tactic:
simp [← smul_mul', smul_one]

Premises used: MulDistribMulAction.smul_one, smul_mul'
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_6
N : Type u_7
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulDistribMulAction M N
m : M
u : Nˣ
⊢ (↑(m • u) : N) = m • (↑u : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
M : Type u_6
N : Type u_7
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulDistribMulAction M N
m : M
u : Nˣ
⊢ (↑(m • u)⁻¹ : N) = m • (↑u⁻¹ : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Units
Goal:
G : Type u_1
M : Type u_3
inst : Group G
inst_1 : Monoid M
inst_2 : MulAction G M
inst_3 : SMulCommClass G M M
inst_4 : IsScalarTower G M M
m : M
g : G
h : IsUnit m
⊢ IsUnit (g • m)

Tactic:
let ⟨u, hu⟩ := h
  hu ▸ ⟨g • u, Units.val_smul _ _⟩

Premises used: _private.0.IsUnit.smul.match_1, IsUnit, Eq.rec, Units.val_smul, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Algebra.Group.AddChar
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
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 φ
-- Module: Mathlib.Algebra.Group.AddChar
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
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 }
⊢ { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M } = ψ

Tactic:
cases ψ
-- Module: Mathlib.Algebra.Group.AddChar
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
ψ : 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
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:
congr
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
f g : AddChar A M
h : ∀ (x : A), Eq.{u_3 + 1} (α := M) ((f : (a : A) → M) x : M) ((g : (a : A) → M) x : M)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
f : A → M
map_zero_eq_one' : f 0 = 1
map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b
⊢ (⇑{ toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' : AddChar A M } :
      (a : A) → M) =
    f

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ Eq.{u_3 + 1} (α := M) ((ψ : (a : A) → M) 0 : M) (1 : M)

Tactic:
ψ.map_zero_eq_one'

Premises used: AddChar.map_zero_eq_one'
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
x y : A
⊢ (ψ : (a : A) → M) (x + y) = HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) x : M) ((ψ : (a : A) → M) y : M)

Tactic:
ψ.map_add_eq_mul' x y

Premises used: AddChar.map_add_eq_mul'
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
a : Multiplicative A
⊢ Eq.{u_3 + 1} (α := M) ((ψ.toMonoidHom : (a : Multiplicative A) → M) a : M)
    ((ψ : (a : A) → M) ((toAdd : (a : Multiplicative A) → A) a : A) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
n : ℕ
x : A
⊢ (ψ : (a : A) → M) (n • x) = HPow.hPow (α := M) ((ψ : (a : A) → M) x : M) n

Tactic:
ψ.toMonoidHom.map_pow x n

Premises used: AddChar.toMonoidHom, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ Eq (α := (a : Multiplicative A) → M)
    (⇑((toMonoidHomEquiv : (a : AddChar A M) → Multiplicative A →* M) ψ : MonoidHom.{u_1, u_3} (Multiplicative A) M) :
      (a : Multiplicative A) → M)
    (comp (β := A) (⇑ψ : (a : A) → M) (⇑toAdd : (a : Multiplicative A) → A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : MonoidHom.{u_1, u_3} (Multiplicative A) M
⊢ Eq (α := (a : A) → M)
    (⇑((Equiv.symm toMonoidHomEquiv : (a : Multiplicative A →* M) → AddChar A M) ψ : AddChar A M) : (a : A) → M)
    (comp (β := Multiplicative A) (⇑ψ : (a : Multiplicative A) → M) (⇑ofAdd : (a : A) → Multiplicative A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
a : Multiplicative A
⊢ Eq.{u_3 + 1} (α := M)
    ((((toMonoidHomEquiv : (a : AddChar A M) → Multiplicative A →* M) ψ : MonoidHom.{u_1, u_3} (Multiplicative A) M) :
          (a : Multiplicative A) → M)
        a :
      M)
    ((ψ : (a : A) → M) ((toAdd : (a : Multiplicative A) → A) a : A) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : MonoidHom.{u_1, u_3} (Multiplicative A) M
a : A
⊢ Eq.{u_3 + 1} (α := M)
    ((((Equiv.symm toMonoidHomEquiv : (a : Multiplicative A →* M) → AddChar A M) ψ : AddChar A M) : (a : A) → M) a : M)
    ((ψ : (a : Multiplicative A) → M) ((ofAdd : (a : A) → Multiplicative A) a : Multiplicative A) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ Eq (α := (a : A) → Additive M) (⇑ψ.toAddMonoidHom : (a : A) → Additive M)
    (comp (β := M) (⇑Additive.ofMul : (a : M) → Additive M) (⇑ψ : (a : A) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
a : A
⊢ Eq.{u_3 + 1} (α := Additive M) ((ψ.toAddMonoidHom : (a : A) → Additive M) a : Additive M)
    ((Additive.ofMul : (a : M) → Additive M) ((ψ : (a : A) → M) a : M) : Additive M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ Eq (α := (a : A) → Additive M)
    (⇑((toAddMonoidHomEquiv : (a : AddChar A M) → A →+ Additive M) ψ : AddMonoidHom.{u_1, u_3} A (Additive M)) :
      (a : A) → Additive M)
    (comp (β := M) (⇑Additive.ofMul : (a : M) → Additive M) (⇑ψ : (a : A) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddMonoidHom.{u_1, u_3} A (Additive M)
⊢ Eq (α := (a : A) → M)
    (⇑((Equiv.symm toAddMonoidHomEquiv : (a : A →+ Additive M) → AddChar A M) ψ : AddChar A M) : (a : A) → M)
    (comp (β := Additive M) (⇑Additive.toMul : (a : Additive M) → M) (⇑ψ : (a : A) → Additive M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
a : A
⊢ Eq.{u_3 + 1} (α := Additive M)
    ((((toAddMonoidHomEquiv : (a : AddChar A M) → A →+ Additive M) ψ : AddMonoidHom.{u_1, u_3} A (Additive M)) :
          (a : A) → Additive M)
        a :
      Additive M)
    ((Additive.ofMul : (a : M) → Additive M) ((ψ : (a : A) → M) a : M) : Additive M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddMonoidHom.{u_1, u_3} A (Additive M)
a : A
⊢ Eq.{u_3 + 1} (α := M)
    ((((Equiv.symm toAddMonoidHomEquiv : (a : A →+ Additive M) → AddChar A M) ψ : AddChar A M) : (a : A) → M) a : M)
    ((Additive.toMul : (a : Additive M) → M) ((ψ : (a : A) → Additive M) a : Additive M) : M)

Tactic:
rfl

Premises used: rfl