awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
⊢ Eq (α := (a : A) → M) (⇑1 : (a : A) → M) 1

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
⊢ Eq (α := (a : A) → M) (⇑0 : (a : A) → M) 1

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
a : A
⊢ Eq.{u_3 + 1} (α := M) ((1 : (a : A) → M) a : M) (1 : 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
a : A
⊢ Eq.{u_3 + 1} (α := M) ((0 : (a : A) → M) a : M) (1 : 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
⊢ Eq (α := AddChar A M) 1 0

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
rw : Eq (α := (a : A) → M) (⇑ψ : (a : A) → M) (⇑0 : (a : A) → M) ↔ ψ = 0
rw₁ rw₂ : ψ = 0 ↔ ψ = 0
⊢ Eq (α := (a : A) → M) (⇑ψ : (a : A) → M) 1 ↔ ψ = 0

Tactic:
rw [← coe_zero, DFunLike.coe_fn_eq]

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

Tactic:
rfl

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

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
⊢ Eq (α := AddMonoidHom.{u_1, u_3} A (Additive M)) ((toAddMonoidHomEquiv : (a : AddChar A M) → A →+ Additive M) 0) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
N : Type u_5
inst_2 : Monoid N
f : M →* N
φ : AddChar A M
⊢ Eq (α := (a : A) → N) (⇑(f.compAddChar φ) : (a : A) → N)
    (comp.{u_1 + 1, u_3 + 1, u_5 + 1} (β := M) (⇑f : (a : M) → N) (⇑φ : (a : A) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
N : Type u_4
inst : AddMonoid A
inst_1 : Monoid M
inst_2 : Monoid N
f : M →* N
φ : AddChar A M
⊢ Eq (α := (a : A) → N) (⇑(f.compAddChar φ) : (a : A) → N)
    (comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑f : (a : M) → N) (⇑φ : (a : A) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
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)
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)
⊢ f = g

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
hψ.injective_comp_right h

Premises used: Function.Surjective.injective_comp_right
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
exact hψ.injective_comp_right h

Premises used: Function.Surjective.injective_comp_right
-- Module: Mathlib.Algebra.Group.AddChar
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 ψ) χ)
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 ⊢

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
hf.comp_left h

Premises used: Function.Injective.comp_left
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
exact hf.comp_left h

Premises used: Function.Injective.comp_left
-- Module: Mathlib.Algebra.Group.AddChar
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
f : A →+ B
⊢ Eq (α := (a : A) → M) (⇑(φ.compAddMonoidHom f) : (a : A) → M)
    (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := B) (⇑φ : (a : B) → M) (⇑f : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
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
f : A →+ B
a : A
⊢ Eq.{u_3 + 1} (α := M) ((ψ.compAddMonoidHom f : (a : A) → M) a : M) ((ψ : (a : B) → M) ((f : (a : A) → B) a : B) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
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) χ)
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 ⊢

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
hf.injective_comp_right h

Premises used: Function.Surjective.injective_comp_right
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
exact hf.injective_comp_right h

Premises used: Function.Surjective.injective_comp_right
-- Module: Mathlib.Algebra.Group.AddChar
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)
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)
⊢ f = g

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
hψ.comp_left h

Premises used: Function.Injective.comp_left
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := (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:
exact hψ.comp_left h

Premises used: Function.Injective.comp_left
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ ψ = 1 ↔ ∀ (x : A), Eq.{u_3 + 1} (α := M) ((ψ : (a : A) → M) x : M) (1 : M)

Tactic:
DFunLike.ext_iff

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ ψ = 0 ↔ ∀ (x : A), Eq.{u_3 + 1} (α := M) ((ψ : (a : A) → M) x : M) (1 : M)

Tactic:
DFunLike.ext_iff

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ ψ ≠ 1 ↔ ∃ (x : A), Ne.{u_3 + 1} (α := M) ((ψ : (a : A) → M) x : M) (1 : M)

Tactic:
DFunLike.ne_iff

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_3
inst : AddMonoid A
inst_1 : Monoid M
ψ : AddChar A M
⊢ ψ ≠ 0 ↔ ∃ (x : A), Ne.{u_3 + 1} (α := M) ((ψ : (a : A) → M) x : M) (1 : M)

Tactic:
DFunLike.ne_iff

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ χ : AddChar A M
⊢ (⇑(ψ * χ) : (a : A) → M) = HMul.hMul (α := (a : A) → M) (⇑ψ : (a : A) → M) (⇑χ : (a : A) → M)

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ χ : AddChar A M
⊢ (⇑(ψ + χ) : (a : A) → M) = HMul.hMul (α := (a : A) → M) (⇑ψ : (a : A) → M) (⇑χ : (a : A) → M)

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ : AddChar A M
n : ℕ
⊢ (⇑(ψ ^ n) : (a : A) → M) = HPow.hPow (α := (a : A) → M) (⇑ψ : (a : A) → M) n

Tactic:
rfl

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

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
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))
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 ∈ Finset.cons a s h, ψ i) : (a : A) → M)
        (∏ i ∈ Finset.cons a s h, (⇑(ψ i) : (a : A) → M))
⊢ Eq (α := (a : A) → M) (⇑(∏ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M))

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ : ι → AddChar A M
⊢ Eq (α := (a : A) → M) (⇑(∏ i ∈ ∅, ψ i) : (a : A) → M) (∏ i ∈ ∅, (⇑(ψ i) : (a : A) → M))

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ : ι → AddChar A M
a : ι
s : Finset ι
h : a ∉ s
h_1 : 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:
simp [*]
-- Module: Mathlib.Algebra.Group.AddChar
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))
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 ∈ Finset.cons a s h, ψ i) : (a : A) → M)
        (∏ i ∈ Finset.cons a s h, (⇑(ψ i) : (a : A) → M))
⊢ Eq (α := (a : A) → M) (⇑(∑ i ∈ s, ψ i) : (a : A) → M) (∏ i ∈ s, (⇑(ψ i) : (a : A) → M))

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ : ι → AddChar A M
⊢ Eq (α := (a : A) → M) (⇑(∑ i ∈ ∅, ψ i) : (a : A) → M) (∏ i ∈ ∅, (⇑(ψ i) : (a : A) → M))

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ : ι → AddChar A M
a : ι
s : Finset ι
h : a ∉ s
h_1 : 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:
simp [*]
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ φ : AddChar A M
a : A
⊢ (ψ * φ : (a : A) → M) a = HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((φ : (a : A) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ φ : AddChar A M
a : A
⊢ (ψ + φ : (a : A) → M) a = HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((φ : (a : A) → M) a : M)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) (∏ c ∈ s, (ψ c : (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)

Tactic:
rw [coe_prod, Finset.prod_apply]

Premises used: Finset.prod_apply, AddChar.coe_prod
-- Module: Mathlib.Algebra.Group.AddChar
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) (∏ c ∈ s, (ψ c : (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)

Tactic:
rw [coe_sum, Finset.prod_apply]

Premises used: Finset.prod_apply, AddChar.coe_sum
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ χ : AddChar A M
⊢ ψ * χ = ψ + χ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ : AddChar A M
n : ℕ
⊢ ψ ^ n = n • ψ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
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 (α := AddChar A M) (∏ i ∈ s, ψ i) (∑ i ∈ s, ψ i)

Tactic:
rfl

Premises used: Multiset.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ φ : AddChar A M
⊢ (toMonoidHomEquiv : (a : AddChar A M) → Multiplicative A →* M) (ψ + φ) =
    HMul.hMul (α := MonoidHom.{u_2, u_3} (Multiplicative A) M) (β := MonoidHom.{u_2, u_3} (Multiplicative A) M)
      ((toMonoidHomEquiv : (a : AddChar A M) → Multiplicative A →* M) ψ : MonoidHom.{u_2, u_3} (Multiplicative A) M)
      ((toMonoidHomEquiv : (a : AddChar A M) → Multiplicative A →* M) φ : MonoidHom.{u_2, u_3} (Multiplicative A) M)

Tactic:
rfl

Premises used: AddChar.toMonoidHom, Multiplicative, rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
ψ φ : MonoidHom.{u_2, u_3} (Multiplicative A) M
⊢ (Equiv.symm toMonoidHomEquiv : (a : Multiplicative A →* M) → AddChar A M) (ψ * φ) =
    HAdd.hAdd (α := AddChar A M) (β := AddChar A M)
      ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative A →* M) → AddChar A M) ψ : AddChar A M)
      ((Equiv.symm toMonoidHomEquiv : (a : Multiplicative A →* M) → AddChar A M) φ : AddChar A M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
φ ψ : AddChar A M
⊢ Equiv.toFun toMonoidHomEquiv (φ * ψ) = Equiv.toFun toMonoidHomEquiv φ * Equiv.toFun toMonoidHomEquiv ψ

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
φ ψ : Additive (AddChar A M)
⊢ Equiv.toFun toAddMonoidHomEquiv (φ + ψ) = Equiv.toFun toAddMonoidHomEquiv φ + Equiv.toFun toAddMonoidHomEquiv ψ

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

Tactic:
simp
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
a : A
⊢ ∀ (a_1 b : AddChar A M),
    (a_1 + b : (a : A) → M) a = HMul.hMul (α := M) (β := M) ((a_1 : (a : A) → M) a : M) ((b : (a : A) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
h :
  ∀ (x : AddChar A M),
    Eq.{u_3 + 1} (α := M)
      (({ toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
            (a : AddChar A M) → M)
          x :
        M)
      ((0 : (a : AddChar A M) → M) x : 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

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
x : AddChar A M
⊢ Eq.{u_3 + 1} (α := M)
    (({ toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
          (a : AddChar A M) → M)
        x :
      M)
    ((0 : (a : AddChar A M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
x x_1 : A
h :
  ∀ (x_2 : AddChar A M),
    Eq.{u_3 + 1} (α := M)
      (({ toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) (x + x_1), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
            (a : AddChar A M) → M)
          x_2 :
        M)
      ((HAdd.hAdd (α := AddChar (AddChar A M) M)
              { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ :
                AddChar (AddChar A M) M }
              { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x_1, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ :
                AddChar (AddChar A M) M } :
            (a : AddChar A M) → M)
          x_2 :
        M)
⊢ { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) (x + x_1), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } =
    HAdd.hAdd (α := AddChar (AddChar A M) M)
      { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ :
        AddChar (AddChar A M) M }
      { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x_1, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ :
        AddChar (AddChar A M) M }

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
x x_1 : A
x_2 : AddChar A M
⊢ Eq.{u_3 + 1} (α := M)
    (({ toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) (x + x_1), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } :
          (a : AddChar A M) → M)
        x_2 :
      M)
    ((HAdd.hAdd (α := AddChar (AddChar A M) M)
            { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ :
              AddChar (AddChar A M) M }
            { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x_1, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ :
              AddChar (AddChar A M) M } :
          (a : AddChar A M) → M)
        x_2 :
      M)

Tactic:
simp [map_add_eq_mul]

Premises used: AddChar.map_add_eq_mul
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
a : A
ψ : AddChar A M
⊢ Eq.{u_3 + 1} (α := M)
    ((((doubleDualEmb : (a : A) → AddChar (AddChar A M) M) a : AddChar (AddChar A M) M) : (a : AddChar A M) → M) ψ : M)
    ((ψ : (a : A) → M) a : M)

Tactic:
rfl

Premises used: rfl