awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
pos : ∀ (h : ψ = 0), Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) (↑(card A) : R)
neg : ∀ (h : ¬ψ = 0), Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) (if ψ = 0 then (↑(card A) : R) else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ψ = 0
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) (↑(card A) : R)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ¬ψ = 0
neg :
  ∀ (x : A) (hx : Ne.{u_2 + 1} (α := R) ((ψ : (a : A) → R) x : R) (1 : R)),
    Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) 0

Tactic:
obtain ⟨x, hx⟩ := ne_one_iff.1 h

Premises used: AddChar.ne_one_iff, Iff.mp
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : Ne.{u_2 + 1} (α := R) ((ψ : (a : A) → R) x : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) 0

Tactic:
eq_zero_of_mul_eq_self_left hx ?_

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : Ne.{u_2 + 1} (α := R) ((ψ : (a : A) → R) x : R) (1 : R)
neg :
  HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) (∑ a : A, (ψ : (a : A) → R) a : R) =
    ∑ a : A, (ψ : (a : A) → R) a
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) 0

Tactic:
refine eq_zero_of_mul_eq_self_left hx ?_

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : Ne.{u_2 + 1} (α := R) ((ψ : (a : A) → R) x : R) (1 : R)
neg :
  Eq.{u_2 + 1} (α := R) (∑ i : A, HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) ((ψ : (a : A) → R) i : R))
    (∑ a : A, (ψ : (a : A) → R) a)
⊢ HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) (∑ a : A, (ψ : (a : A) → R) a : R) =
    ∑ a : A, (ψ : (a : A) → R) a

Tactic:
rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : Ne.{u_2 + 1} (α := R) ((ψ : (a : A) → R) x : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) (∑ i : A, HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) ((ψ : (a : A) → R) i : R))
    (∑ a : A, (ψ : (a : A) → R) a)

Tactic:
Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm

Premises used: AddChar.map_add_eq_mul, Equiv.addLeft, Fintype.sum_equiv, Eq.symm
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : Ne.{u_2 + 1} (α := R) ((ψ : (a : A) → R) x : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) (∑ i : A, HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) ((ψ : (a : A) → R) i : R))
    (∑ a : A, (ψ : (a : A) → R) a)

Tactic:
exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm

Premises used: Equiv.addLeft, Fintype.sum_equiv
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : CharZero R
rw : Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ ≠ 0

Tactic:
rw [sum_eq_ite, Ne.ite_eq_right_iff]

Premises used: Ne.ite_eq_right_iff, AddChar.sum_eq_ite
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : CharZero R
⊢ Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0

Tactic:
Nat.cast_ne_zero.2 Fintype.card_ne_zero

Premises used: Iff.mpr, Fintype.card_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : CharZero R
⊢ Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0

Tactic:
exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Premises used: Iff.mpr, Fintype.card_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : CharZero R
rw : Eq.{u_2 + 1} (α := R) (if ψ = 0 then (↑(card A) : R) else 0) 0 ↔ ψ ≠ 0
rw₁ : ¬ψ = 0 ↔ ψ ≠ 0
rw₂ : Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0
rw₃ : ¬ψ = 0 ↔ ψ ≠ 0
rw₄ rw₅ rw₆ : Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ ≠ 0

Tactic:
classical
  rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Premises used: Iff.mpr, Ne.ite_eq_right_iff, AddChar.sum_eq_ite, Fintype.card_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Fintype A
inst_2 : CommSemiring R
inst_3 : IsDomain R
ψ : AddChar A R
inst_4 : CharZero R
⊢ Ne.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ = 0

Tactic:
sum_eq_zero_iff_ne_zero.not_left

Premises used: AddChar.sum_eq_zero_iff_ne_zero, Iff.not_left
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : CommMonoid M
ψ : AddChar A M
h :
  ∀ (x : A),
    Eq.{u_2 + 1} (α := M) ((ψ.compAddMonoidHom negAddMonoidHom * ψ : (a : A) → M) x : M) ((1 : (a : A) → M) x : M)
⊢ ψ.compAddMonoidHom negAddMonoidHom * ψ = 1

Tactic:
ext1 x
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : CommMonoid M
ψ : AddChar A M
x : A
⊢ Eq.{u_2 + 1} (α := M) ((ψ.compAddMonoidHom negAddMonoidHom * ψ : (a : A) → M) x : M) ((1 : (a : A) → M) x : M)

Tactic:
simp [negAddMonoidHom, ← map_add_eq_mul]

Premises used: AddChar.map_add_eq_mul, negAddMonoidHom
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : CommMonoid M
ψ : AddChar A M
a : A
⊢ Eq.{u_2 + 1} (α := 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_1
M : Type u_2
inst : AddCommGroup A
inst_1 : CommMonoid M
ψ : AddChar A M
a : A
⊢ Eq.{u_2 + 1} (α := 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_1
M : Type u_2
inst : AddCommGroup 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_1
M : Type u_2
inst : AddCommGroup 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_1
M : Type u_2
inst : AddGroup A
inst_1 : Monoid M
φ : AddChar A M
a : A
⊢ IsUnit.{u_2} (M := M) ((φ : (a : A) → M) a : M)

Tactic:
IsUnit.map φ.toMonoidHom <| Group.isUnit (Multiplicative.ofAdd a)

Premises used: AddChar.toMonoidHom, Group.isUnit, IsUnit.map, Multiplicative.ofAdd, DFunLike.coe
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddGroup A
inst_1 : DivisionMonoid M
ψ : AddChar A M
a : A
h : HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) (-a) : M) ((ψ : (a : A) → M) a : M) = 1
⊢ Eq.{u_2 + 1} (α := M) ((ψ : (a : A) → M) (-a) : M) (((ψ : (a : A) → M) a)⁻¹ : M)

Tactic:
apply eq_inv_of_mul_eq_one_left

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddGroup A
inst_1 : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) (-a) : M) ((ψ : (a : A) → M) a : M) = 1

Tactic:
simp only [← map_add_eq_mul, neg_add_cancel, map_zero_eq_one]

Premises used: AddChar.map_add_eq_mul, AddChar.map_zero_eq_one, neg_add_cancel
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddGroup A
inst_1 : DivisionMonoid M
ψ : AddChar A M
n : ℤ
a : A
⊢ (ψ : (a : A) → M) (n • a) = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) n

Tactic:
ψ.toMonoidHom.map_zpow a n

Premises used: AddChar.toMonoidHom, MonoidHom.map_zpow
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
a : A
rw : Eq.{u_2 + 1} (α := M) ((ψ : (a : A) → M) (-a) : M) (((ψ : (a : A) → M) a)⁻¹ : M)
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (((ψ : (a : A) → M) a)⁻¹ : M) (((ψ : (a : A) → M) a)⁻¹ : M)
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : A) → M) a : M) (((ψ : (a : A) → M) a)⁻¹ : M)

Tactic:
rw [inv_apply, map_neg_eq_inv]

Premises used: AddChar.map_neg_eq_inv, AddChar.inv_apply
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
a : A
⊢ Eq.{u_2 + 1} (α := M) ((-ψ : (a : A) → M) a : M) (((ψ : (a : A) → M) a)⁻¹ : M)

Tactic:
map_neg_eq_inv _ _

Premises used: AddChar.map_neg_eq_inv
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
rw :
  HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) (-a) : M) =
    HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
rw₁ :
  HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) (((χ : (a : A) → M) a)⁻¹ : M) =
    HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
rw₂ rw₃ :
  HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) (((χ : (a : A) → M) a)⁻¹ : M) =
    HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) (((χ : (a : A) → M) a)⁻¹ : M)
⊢ (ψ / χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)

Tactic:
rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]

Premises used: AddChar.map_neg_eq_inv, AddChar.div_apply, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
rw :
  HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) (-a) : M) =
    HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
rw₁ :
  HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) (((χ : (a : A) → M) a)⁻¹ : M) =
    HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
rw₂ rw₃ :
  HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) (((χ : (a : A) → M) a)⁻¹ : M) =
    HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) a : M) (((χ : (a : A) → M) a)⁻¹ : M)
⊢ (ψ - χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)

Tactic:
rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]

Premises used: AddChar.sub_apply, AddChar.map_neg_eq_inv, div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
n : ℤ
ψ : AddChar A M
a : A
ofNat : ∀ (a_1 : ℕ), (Int.ofNat a_1 • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) (Int.ofNat a_1)
negSucc :
  ∀ (a_1 : ℕ), (Int.negSucc a_1 • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) (Int.negSucc a_1)
⊢ (n • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) n

Tactic:
cases n
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
a : A
a_1 : ℕ
⊢ (Int.ofNat a_1 • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) (Int.ofNat a_1)

Tactic:
simp [-neg_apply, neg_apply']

Premises used: AddChar.neg_apply, AddChar.neg_apply'
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
a : A
a_1 : ℕ
⊢ (Int.negSucc a_1 • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) (Int.negSucc a_1)

Tactic:
simp [-neg_apply, neg_apply']

Premises used: AddChar.neg_apply, AddChar.neg_apply'
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
n : ℤ
a : A
⊢ (ψ ^ n : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) n

Tactic:
zsmul_apply ..

Premises used: AddChar.zsmul_apply
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
a b : A
⊢ (ψ : (a : A) → M) (a - b) = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((ψ : (a : A) → M) b : M)

Tactic:
ψ.toMonoidHom.map_div _ _

Premises used: AddChar.toMonoidHom, MonoidHom.map_div
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ : AddChar A M
⊢ Injective.{u_1 + 1, u_2 + 1} (α := A) (β := M) (⇑ψ : (a : A) → M) ↔
    ∀ ⦃x : A⦄, Eq.{u_2 + 1} (α := M) ((ψ : (a : A) → M) x : M) (1 : M) → x = 0

Tactic:
ψ.toMonoidHom.ker_eq_bot_iff.symm.trans eq_bot_iff

Premises used: AddChar.toMonoidHom, Multiplicative, MonoidHom.ker_eq_bot_iff, Iff.trans, eq_bot_iff, Iff.symm
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
A : Type u_1
M₀ : Type u_2
inst : AddGroup A
inst_1 : MonoidWithZero M₀
inst_2 : Nontrivial M₀
ψ : AddChar A M₀
h : Eq.{u_2 + 1} (α := M₀) ((ψ : (a : A) → M₀) 0 : M₀) (0 0 : M₀)
⊢ False

Tactic:
simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ

Premises used: Pi.zero_apply, zero_ne_one, AddChar.map_zero_eq_one
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r x : R
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift r : (a : R) → M) x : M) ((ψ : (a : R) → M) (r * x) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
⊢ ψ⁻¹ = ψ.mulShift (-1)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
x : R
h : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
h₁ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ : (a : R) → M) (-1 * x) : M)
h₂ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ : (a : R) → M) (-(1 * x)) : M)
h₃ h₄ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ : (a : R) → M) (-x) : M)
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)

Tactic:
rw [inv_apply, mulShift_apply, neg_mul, one_mul]

Premises used: AddChar.mulShift_apply, AddChar.inv_apply, neg_mul, one_mul
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
rw : (ψ : (a : R) → M) ((↑n : R) * x) = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
rw₁ : (ψ : (a : R) → M) (n • x) = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
rw₂ rw₃ : HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
⊢ (ψ.mulShift (↑n : R) : (a : R) → M) x = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n

Tactic:
rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]

Premises used: AddChar.map_nsmul_eq_pow, AddChar.mulShift_apply, nsmul_eq_mul
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
n : ℕ
h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ ^ n : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)
⊢ ψ ^ n = ψ.mulShift (↑n : R)

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
h : HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n = (ψ.mulShift (↑n : R) : (a : R) → M) x
h₁ h₂ : Eq.{u_2 + 1} (α := M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((ψ ^ n : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)

Tactic:
rw [pow_apply, ← mulShift_spec']

Premises used: AddChar.pow_apply, AddChar.mulShift_spec'
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s : R
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := M) ((ψ.mulShift r * ψ.mulShift s : (a : R) → M) x : M) ((ψ.mulShift (r + s) : (a : R) → M) x : M)
⊢ ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s x : R
h :
  (ψ.mulShift r * ψ.mulShift s : (a : R) → M) x =
    HMul.hMul (α := M) (β := M) ((ψ : (a : R) → M) (r * x) : M) ((ψ : (a : R) → M) (s * x) : M)
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift r * ψ.mulShift s : (a : R) → M) x : M) ((ψ.mulShift (r + s) : (a : R) → M) x : M)

Tactic:
rw [mulShift_apply, right_distrib, map_add_eq_mul]

Premises used: AddChar.map_add_eq_mul, AddChar.mulShift_apply, right_distrib
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s x : R
⊢ (ψ.mulShift r * ψ.mulShift s : (a : R) → M) x =
    HMul.hMul (α := M) (β := M) ((ψ : (a : R) → M) (r * x) : M) ((ψ : (a : R) → M) (s * x) : M)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s : R
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := M) (((ψ.mulShift r).mulShift s : (a : R) → M) x : M) ((ψ.mulShift (r * s) : (a : R) → M) x : M)
⊢ (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s x : R
⊢ Eq.{u_2 + 1} (α := M) (((ψ.mulShift r).mulShift s : (a : R) → M) x : M) ((ψ.mulShift (r * s) : (a : R) → M) x : M)

Tactic:
simp only [mulShift_apply, mul_assoc]

Premises used: mul_assoc, AddChar.mulShift_apply
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)
⊢ ψ.mulShift 0 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
x : R
h : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (0 * x) : M) ((1 : (a : R) → M) x : M)
h₁ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) 0 : M) ((1 : (a : R) → M) x : M)
h₂ : Eq.{u_2 + 1} (α := M) (1 : M) ((1 : (a : R) → M) x : M)
h₃ h₄ : Eq.{u_2 + 1} (α := M) 1 1
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)

Tactic:
rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]

Premises used: MulZeroClass.zero_mul, AddChar.map_zero_eq_one, AddChar.mulShift_apply, AddChar.one_apply
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ.mulShift 1 : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)
⊢ ψ.mulShift 1 = ψ

Tactic:
ext
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
x : R
h : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (1 * x) : M) ((ψ : (a : R) → M) x : M)
h₁ h₂ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 1 : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)

Tactic:
rw [mulShift_apply, one_mul]

Premises used: AddChar.mulShift_apply, one_mul
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ.mulShift u = 1 ↔ ψ = 1

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
refine_1 : ∀ (h : ψ.mulShift u = 1), ψ = 1
refine_2 : ψ = 1 → ψ.mulShift u = 1
⊢ ψ.mulShift u = 1 ↔ ψ = 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
refine_1 : ∀ (y : R), Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) y : M) ((1 : (a : R) → M) y : M)
⊢ ψ = 1

Tactic:
ext1 y
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
rw : y = u * (↑hu.unit⁻¹ : R) * y
rw₁ : y = 1 * y
rw₂ rw₃ : y = y
⊢ y = u * ((↑hu.unit⁻¹ : R) * y)

Tactic:
rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]

Premises used: IsUnit.mul_val_inv, mul_assoc, one_mul
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
refine_1 :
  Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (u * ((↑hu.unit⁻¹ : R) * y)) : M)
    ((1 : (a : R) → M) (u * ((↑hu.unit⁻¹ : R) * y)) : M)
⊢ Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) y : M) ((1 : (a : R) → M) y : M)

Tactic:
rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
y : R
⊢ Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (u * ((↑hu.unit⁻¹ : R) * y)) : M)
    ((1 : (a : R) → M) (u * ((↑hu.unit⁻¹ : R) * y)) : M)

Tactic:
simpa only [mulShift_apply] using DFunLike.ext_iff.mp h (hu.unit⁻¹ * y)

Premises used: Units.val, HMul.hMul, AddChar.mulShift_apply, DFunLike.ext_iff, Inv.inv, Iff.mp, IsUnit.unit
-- Module: Mathlib.Algebra.Group.AddChar
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : α
b : p → β
c : ¬p → β
pos : ∀ (h : p), a ^ b h = a ^ b h
neg : ∀ (h : ¬p), a ^ c h = a ^ c h
⊢ HPow.hPow.{u_1, u_2, u_1} (β := β) a (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : α
b : p → β
c : ¬p → β
h : p
⊢ a ^ b h = a ^ b h

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : α
b : p → β
c : ¬p → β
h : ¬p
⊢ a ^ c h = a ^ c h

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
c : β
pos : ∀ (h : p), a h ^ c = a h ^ c
neg : ∀ (h : ¬p), b h ^ c = b h ^ c
⊢ HPow.hPow (α := α) (if h : p then a h else b h) c = if h : p then a h ^ c else b h ^ c

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Group.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
c : β
h : p
⊢ a h ^ c = a h ^ c

Tactic:
rfl