awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Nontrivial α
⊢ Nontrivial.{u} (Multiplicative α)

Tactic:
ofAdd.injective.nontrivial

Premises used: Function.Injective.nontrivial, Equiv.injective, Multiplicative.ofAdd
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Add α
x y : α
⊢ (ofAdd : (a : α) → Multiplicative α) (x + y) =
    HMul.hMul (α := Multiplicative α) (β := Multiplicative α)
      ((ofAdd : (a : α) → Multiplicative α) x : Multiplicative α)
      ((ofAdd : (a : α) → Multiplicative α) y : Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Add α
x y : Multiplicative α
⊢ (toAdd : (a : Multiplicative α) → α) (x * y) =
    HAdd.hAdd (α := α) (β := α) ((toAdd : (a : Multiplicative α) → α) x : α)
      ((toAdd : (a : Multiplicative α) → α) y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Mul α
x y : α
⊢ (ofMul : (a : α) → Additive α) (x * y) =
    HAdd.hAdd (α := Additive α) (β := Additive α) ((ofMul : (a : α) → Additive α) x : Additive α)
      ((ofMul : (a : α) → Additive α) y : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Mul α
x y : Additive α
⊢ (toMul : (a : Additive α) → α) (x + y) =
    HMul.hMul (α := α) (β := α) ((toMul : (a : Additive α) → α) x : α) ((toMul : (a : Additive α) → α) y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : IsLeftCancelMul α
⊢ IsLeftCancelAdd.{u} (Additive α)

Tactic:
⟨@mul_left_cancel α _ _⟩

Premises used: mul_left_cancel, IsLeftCancelAdd.mk
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : IsLeftCancelAdd α
⊢ IsLeftCancelMul.{u} (Multiplicative α)

Tactic:
⟨@add_left_cancel α _ _⟩

Premises used: add_left_cancel, IsLeftCancelMul.mk
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : IsRightCancelMul α
⊢ IsRightCancelAdd.{u} (Additive α)

Tactic:
⟨fun _ _ _ ↦ mul_right_cancel (G := α)⟩

Premises used: mul_right_cancel, IsRightCancelAdd.mk
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : IsRightCancelAdd α
⊢ IsRightCancelMul.{u} (Multiplicative α)

Tactic:
⟨fun _ _ _ ↦ add_right_cancel (G := α)⟩

Premises used: add_right_cancel, IsRightCancelMul.mk
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Mul α
inst_1 : IsCancelMul α
⊢ IsCancelAdd.{u} (Additive α)

Tactic:
⟨⟩

Premises used: IsCancelAdd.mk
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : IsCancelAdd α
⊢ IsCancelMul.{u} (Multiplicative α)

Tactic:
⟨⟩

Premises used: IsCancelMul.mk
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := Additive α) ((ofMul : (a : α) → Additive α) 1 : Additive α) (0 : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
A : Type u_1
inst : One A
x : A
⊢ Eq (α := Additive A) ((ofMul : (a : A) → Additive A) x : Additive A) (0 : Additive A) ↔ x = 1

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := α) ((toMul : (a : Additive α) → α) 0 : α) (1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u_1
inst : One α
x : Additive α
⊢ Eq (α := α) ((toMul : (a : Additive α) → α) x : α) (1 : α) ↔ x = 0

Tactic:
Iff.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Zero α
⊢ Eq.{u + 1} (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) 0 : Multiplicative α) (1 : Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
A : Type u_1
inst : Zero A
x : A
⊢ Eq (α := Multiplicative A) ((ofAdd : (a : A) → Multiplicative A) x : Multiplicative A) (1 : Multiplicative A) ↔ x = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Zero α
⊢ Eq.{u + 1} (α := α) ((toAdd : (a : Multiplicative α) → α) 1 : α) (0 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u_1
inst : Zero α
x : Multiplicative α
⊢ Eq (α := α) ((toAdd : (a : Multiplicative α) → α) x : α) (0 : α) ↔ x = 1

Tactic:
Iff.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
n : ℕ
a : α
⊢ (ofMul : (a : α) → Additive α) (a ^ n) =
    HSMul.hSMul (β := Additive α) n ((ofMul : (a : α) → Additive α) a : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
n : ℕ
a : Additive α
⊢ (toMul : (a : Additive α) → α) (n • a) = HPow.hPow (α := α) ((toMul : (a : Additive α) → α) a : α) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
n : ℕ
a : α
⊢ (ofAdd : (a : α) → Multiplicative α) (n • a) =
    HPow.hPow (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : Multiplicative α
n : ℕ
⊢ (toAdd : (a : Multiplicative α) → α) (a ^ n) = HSMul.hSMul (β := α) n ((toAdd : (a : Multiplicative α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
a : α
⊢ IsAddLeftRegular (R := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
a : Additive α
⊢ IsLeftRegular (R := α) ((toMul : (a : Additive α) → α) a : α) ↔ IsAddLeftRegular a

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
a : α
⊢ IsAddRightRegular (R := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
a : Additive α
⊢ IsRightRegular (R := α) ((toMul : (a : Additive α) → α) a : α) ↔ IsAddRightRegular a

Tactic:
.rfl

Premises used: Additive, Iff.rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
a : α
⊢ IsAddRegular (R := Additive α) ((ofMul : (a : α) → Additive α) a : Additive α) ↔ IsRegular a

Tactic:
simp [isAddRegular_iff, isRegular_iff]

Premises used: isRegular_iff, isAddRegular_iff
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Monoid α
a : Additive α
⊢ IsRegular (R := α) ((toMul : (a : Additive α) → α) a : α) ↔ IsAddRegular a

Tactic:
simp [isAddRegular_iff, isRegular_iff]

Premises used: isRegular_iff, isAddRegular_iff
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : α
⊢ IsLeftRegular (R := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) ↔ IsAddLeftRegular a

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : Multiplicative α
⊢ IsAddLeftRegular (R := α) ((toAdd : (a : Multiplicative α) → α) a : α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : α
⊢ IsRightRegular (R := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) ↔
    IsAddRightRegular a

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : Multiplicative α
⊢ IsAddRightRegular (R := α) ((toAdd : (a : Multiplicative α) → α) a : α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Iff.rfl, Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : α
⊢ IsRegular (R := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) ↔ IsAddRegular a

Tactic:
simp [isAddRegular_iff, isRegular_iff]

Premises used: isRegular_iff, isAddRegular_iff
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : AddMonoid α
a : Multiplicative α
⊢ IsAddRegular (R := α) ((toAdd : (a : Multiplicative α) → α) a : α) ↔ IsRegular a

Tactic:
simp [isAddRegular_iff, isRegular_iff]

Premises used: isRegular_iff, isAddRegular_iff
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Inv α
x : α
⊢ Eq (α := Additive α) ((ofMul : (a : α) → Additive α) x⁻¹ : Additive α)
    (-(ofMul : (a : α) → Additive α) x : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Inv α
x : Additive α
⊢ Eq (α := α) ((toMul : (a : Additive α) → α) (-x) : α) (((toMul : (a : Additive α) → α) x)⁻¹ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Neg α
x : α
⊢ Eq (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) (-x) : Multiplicative α)
    (((ofAdd : (a : α) → Multiplicative α) x)⁻¹ : Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Neg α
x : Multiplicative α
⊢ Eq (α := α) ((toAdd : (a : Multiplicative α) → α) x⁻¹ : α) (-(toAdd : (a : Multiplicative α) → α) x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Sub α
x y : α
⊢ (ofAdd : (a : α) → Multiplicative α) (x - y) =
    HDiv.hDiv (α := Multiplicative α) (β := Multiplicative α)
      ((ofAdd : (a : α) → Multiplicative α) x : Multiplicative α)
      ((ofAdd : (a : α) → Multiplicative α) y : Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Sub α
x y : Multiplicative α
⊢ (toAdd : (a : Multiplicative α) → α) (x / y) =
    HSub.hSub (α := α) (β := α) ((toAdd : (a : Multiplicative α) → α) x : α)
      ((toAdd : (a : Multiplicative α) → α) y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Div α
x y : α
⊢ (ofMul : (a : α) → Additive α) (x / y) =
    HSub.hSub (α := Additive α) (β := Additive α) ((ofMul : (a : α) → Additive α) x : Additive α)
      ((ofMul : (a : α) → Additive α) y : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : Div α
x y : Additive α
⊢ (toMul : (a : Additive α) → α) (x - y) =
    HDiv.hDiv (α := α) (β := α) ((toMul : (a : Additive α) → α) x : α) ((toMul : (a : Additive α) → α) y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : DivInvMonoid α
z : ℤ
a : α
⊢ (ofMul : (a : α) → Additive α) (a ^ z) =
    HSMul.hSMul (β := Additive α) z ((ofMul : (a : α) → Additive α) a : Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : DivInvMonoid α
z : ℤ
a : Additive α
⊢ (toMul : (a : Additive α) → α) (z • a) = HPow.hPow (α := α) ((toMul : (a : Additive α) → α) a : α) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : SubNegMonoid α
z : ℤ
a : α
⊢ (ofAdd : (a : α) → Multiplicative α) (z • a) =
    HPow.hPow (α := Multiplicative α) ((ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
α : Type u
inst : SubNegMonoid α
a : Multiplicative α
z : ℤ
⊢ (toAdd : (a : Multiplicative α) → α) (a ^ z) = HSMul.hSMul (β := α) z ((toAdd : (a : Multiplicative α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
inl :
  ∀ (a : M j),
    Eq.{u_2 + 1} (α := Multiplicative (M j))
      (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) j
        ((ofAdd : (a : M j) → Multiplicative (M j)) a : Multiplicative (M j)) j)
      ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) j a j))
inr :
  ∀ (h : j ≠ i),
    Eq.{u_2 + 1} (α := Multiplicative (M j))
      (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) i
        ((ofAdd : (a : M i) → Multiplicative (M i)) a : Multiplicative (M i)) j)
      ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) i a j))
⊢ Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) i
      ((ofAdd : (a : M i) → Multiplicative (M i)) a : Multiplicative (M i)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) i a j))

Tactic:
rcases eq_or_ne j i with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → AddMonoid (M i)
j : ι
a : M j
⊢ Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) j
      ((ofAdd : (a : M j) → Multiplicative (M j)) a : Multiplicative (M j)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) j a j))

Tactic:
simp only [mulSingle_eq_same, single_eq_same]

Premises used: Pi.mulSingle_eq_same, Pi.single_eq_same
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ Eq.{u_2 + 1} (α := Multiplicative (M j))
    (mulSingle (M := fun (i : ι) ↦ Multiplicative (M i)) i
      ((ofAdd : (a : M i) → Multiplicative (M i)) a : Multiplicative (M i)) j)
    ((ofAdd : (a : M j) → Multiplicative (M j)) (single (M := M) i a j))

Tactic:
simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single,
      zero_apply, ofAdd_zero]

Premises used: ofAdd_zero, Pi.one_apply, Pi.zero_apply, Pi.single, ne_eq, not_false_eq_true, Pi.mulSingle, Function.update_of_ne
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
inl :
  ∀ (a : M j),
    Eq.{u_2 + 1} (α := Additive (M j))
      (single (M := fun (i : ι) ↦ Additive (M i)) j ((ofMul : (a : M j) → Additive (M j)) a : Additive (M j)) j)
      ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) j a j))
inr :
  ∀ (h : j ≠ i),
    Eq.{u_2 + 1} (α := Additive (M j))
      (single (M := fun (i : ι) ↦ Additive (M i)) i ((ofMul : (a : M i) → Additive (M i)) a : Additive (M i)) j)
      ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) i a j))
⊢ Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) i ((ofMul : (a : M i) → Additive (M i)) a : Additive (M i)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) i a j))

Tactic:
rcases eq_or_ne j i with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
j : ι
a : M j
⊢ Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) j ((ofMul : (a : M j) → Additive (M j)) a : Additive (M j)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) j a j))

Tactic:
simp only [mulSingle_eq_same, single_eq_same]

Premises used: Pi.mulSingle_eq_same, Pi.single_eq_same
-- Module: Mathlib.Algebra.Group.TypeTags.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ Eq.{u_2 + 1} (α := Additive (M j))
    (single (M := fun (i : ι) ↦ Additive (M i)) i ((ofMul : (a : M i) → Additive (M i)) a : Additive (M i)) j)
    ((ofMul : (a : M j) → Additive (M j)) (mulSingle (M := M) i a j))

Tactic:
simp only [single, ne_eq, h, not_false_eq_true, Function.update_of_ne, zero_apply, mulSingle,
      one_apply, ofMul_one]

Premises used: Pi.one_apply, Pi.zero_apply, Pi.single, ne_eq, ofMul_one, not_false_eq_true, Pi.mulSingle, Function.update_of_ne
-- Module: Mathlib.Algebra.Group.TypeTags.Finite
Goal:
α : Type u
inst : Finite α
⊢ α ≃ α

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Finite
Goal:
α : Type u
h : Infinite α
⊢ Infinite.{u + 1} (Additive α)

Tactic:
h

Premises used: Additive
-- Module: Mathlib.Algebra.Group.TypeTags.Finite
Goal:
α : Type u
h : Infinite α
⊢ Infinite.{u + 1} (Multiplicative α)

Tactic:
h

Premises used: Multiplicative
-- Module: Mathlib.Algebra.Group.TypeTags.Finite
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (Multiplicative α) = card α

Tactic:
Finset.card_map _

Premises used: Finset.univ, Finset.card_map, Finset.map, Fintype.card
-- Module: Mathlib.Algebra.Group.TypeTags.Finite
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (Additive α) = card α

Tactic:
Finset.card_map _

Premises used: Finset.univ, Finset.card_map, Finset.map, Fintype.card
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : AddZeroClass α
inst_1 : AddZeroClass β
f : α →+ β
⊢ Eq (α := (a : Multiplicative α) → Multiplicative β)
    (⇑((toMultiplicative : (a : α →+ β) → Multiplicative α →* Multiplicative β) f :
          MonoidHom.{u_3, u_4} (Multiplicative α) (Multiplicative β)) :
      (a : Multiplicative α) → Multiplicative β)
    (Function.comp (β := β) (⇑ofAdd : (a : β) → Multiplicative β)
      (Function.comp (β := α) (⇑f : (a : α) → β) (⇑toAdd : (a : Multiplicative α) → α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
inst : AddZeroClass α
⊢ Eq (α := Multiplicative α →* Multiplicative α)
    ((toMultiplicative : (a : α →+ α) → Multiplicative α →* Multiplicative α) (id α) :
      Multiplicative α →* Multiplicative α)
    (MonoidHom.id (Multiplicative α) : Multiplicative α →* Multiplicative α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : MulOneClass α
inst_1 : MulOneClass β
f : α →* β
⊢ Eq (α := (a : Additive α) → Additive β)
    (⇑((toAdditive : (a : α →* β) → Additive α →+ Additive β) f : AddMonoidHom.{u_3, u_4} (Additive α) (Additive β)) :
      (a : Additive α) → Additive β)
    (Function.comp (β := β) (⇑ofMul : (a : β) → Additive β)
      (Function.comp (β := α) (⇑f : (a : α) → β) (⇑toMul : (a : Additive α) → α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
inst : MulOneClass α
⊢ Eq (α := Additive α →+ Additive α)
    ((toAdditive : (a : α →* α) → Additive α →+ Additive α) (id α) : Additive α →+ Additive α)
    (AddMonoidHom.id (Additive α) : Additive α →+ Additive α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : MulOneClass α
inst_1 : AddZeroClass β
f : AddMonoidHom.{u_3, u_4} (Additive α) β
⊢ Eq (α := (a : α) → Multiplicative β)
    (⇑((toMultiplicativeRight : (a : Additive α →+ β) → α →* Multiplicative β) f :
          MonoidHom.{u_3, u_4} α (Multiplicative β)) :
      (a : α) → Multiplicative β)
    (Function.comp (β := β) (⇑ofAdd : (a : β) → Multiplicative β)
      (Function.comp (β := Additive α) (⇑f : (a : Additive α) → β) (⇑ofMul : (a : α) → Additive α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : MulOneClass α
inst_1 : AddZeroClass β
f : MonoidHom.{u_3, u_4} α (Multiplicative β)
⊢ Eq (α := (a : Additive α) → β)
    (⇑((toAdditiveLeft : (a : α →* Multiplicative β) → Additive α →+ β) f : AddMonoidHom.{u_3, u_4} (Additive α) β) :
      (a : Additive α) → β)
    (Function.comp (β := Multiplicative β) (⇑toAdd : (a : Multiplicative β) → β)
      (Function.comp (β := α) (⇑f : (a : α) → Multiplicative β) (⇑toMul : (a : Additive α) → α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : AddZeroClass α
inst_1 : MulOneClass β
f : AddMonoidHom.{u_3, u_4} α (Additive β)
⊢ Eq (α := (a : Multiplicative α) → β)
    (⇑((toMultiplicativeLeft : (a : α →+ Additive β) → Multiplicative α →* β) f :
          MonoidHom.{u_3, u_4} (Multiplicative α) β) :
      (a : Multiplicative α) → β)
    (Function.comp (β := Additive β) (⇑toMul : (a : Additive β) → β)
      (Function.comp (β := α) (⇑f : (a : α) → Additive β) (⇑toAdd : (a : Multiplicative α) → α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : AddZeroClass α
inst_1 : MulOneClass β
f : MonoidHom.{u_3, u_4} (Multiplicative α) β
⊢ Eq (α := (a : α) → Additive β)
    (⇑((toAdditiveRight : (a : Multiplicative α →* β) → α →+ Additive β) f : AddMonoidHom.{u_3, u_4} α (Additive β)) :
      (a : α) → Additive β)
    (Function.comp (β := β) (⇑ofMul : (a : β) → Additive β)
      (Function.comp (β := Multiplicative α) (⇑f : (a : Multiplicative α) → β) (⇑ofAdd : (a : α) → Multiplicative α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : AddZeroClass α
inst_1 : MulOneClass β
f g : MonoidHom.{u_3, u_4} (Multiplicative α) β
h :
  Eq (α := AddMonoidHom.{u_3, u_4} α (Additive β))
    ((MonoidHom.toAdditiveRight : (a : Multiplicative α →* β) → α →+ Additive β) f :
      AddMonoidHom.{u_3, u_4} α (Additive β))
    ((MonoidHom.toAdditiveRight : (a : Multiplicative α →* β) → α →+ Additive β) g :
      AddMonoidHom.{u_3, u_4} α (Additive β))
⊢ f = g

Tactic:
MonoidHom.toAdditiveRight.injective h

Premises used: Equiv.injective, MonoidHom.toAdditiveRight
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
α : Type u_3
β : Type u_4
inst : MulOneClass α
inst_1 : AddZeroClass β
f g : AddMonoidHom.{u_3, u_4} (Additive α) β
h :
  Eq (α := MonoidHom.{u_3, u_4} α (Multiplicative β))
    ((AddMonoidHom.toMultiplicativeRight : (a : Additive α →+ β) → α →* Multiplicative β) f :
      MonoidHom.{u_3, u_4} α (Multiplicative β))
    ((AddMonoidHom.toMultiplicativeRight : (a : Additive α →+ β) → α →* Multiplicative β) g :
      MonoidHom.{u_3, u_4} α (Multiplicative β))
⊢ f = g

Tactic:
AddMonoidHom.toMultiplicativeRight.injective h

Premises used: AddMonoidHom.toMultiplicativeRight, Equiv.injective
-- Module: Mathlib.Algebra.Group.TypeTags.Hom
Goal:
M : Type u_1
N : Type u_2
inst : AddMonoid M
inst_1 : AddCommMonoid N
f g : M →+ N
⊢ (toMultiplicative : (a : M →+ N) → Multiplicative M →* Multiplicative N) (f + g) =
    HMul.hMul (α := MonoidHom.{u_1, u_2} (Multiplicative M) (Multiplicative N)) (β :=
      MonoidHom.{u_1, u_2} (Multiplicative M) (Multiplicative N))
      ((toMultiplicative : (a : M →+ N) → Multiplicative M →* Multiplicative N) f :
        MonoidHom.{u_1, u_2} (Multiplicative M) (Multiplicative N))
      ((toMultiplicative : (a : M →+ N) → Multiplicative M →* Multiplicative N) g :
        MonoidHom.{u_1, u_2} (Multiplicative M) (Multiplicative N))

Tactic:
rfl

Premises used: rfl