awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
ι : Type u_1
A : Type u_2
M : Type u_3
inst : AddMonoid A
inst_1 : CommMonoid M
x x_1 : A
⊢ { 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 }
have 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' := sorry, map_add_eq_mul' := sorry } :
          (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' := sorry, map_add_eq_mul' := sorry :
              AddChar (AddChar A M) M }
            { toFun := fun (ψ : AddChar A M) ↦ (ψ : (a : A) → M) x_1, map_zero_eq_one' := sorry, map_add_eq_mul' := sorry :
              AddChar (AddChar A M) M } :
          (a : AddChar A M) → M)
        x_2 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) (if ψ = 0 then (↑(card A) : R) else 0)
have pos : ∀ (h : ψ = 0), Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) (↑(card A) : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) (if ψ = 0 then (↑(card A) : R) else 0)
have neg : ∀ (h : ¬ψ = 0), Eq.{u_2 + 1} (α := R) (∑ a : A, (ψ : (a : A) → R) a) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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) 0
have 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
Tactic: obtain ⟨x, hx⟩ := ne_one_iff.1 h
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
have neg : HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) (∑ a : A, (ψ : (a : A) → R) a : R) = ∑ a : A, (ψ : (a : A) → R) a
Tactic: refine eq_zero_of_mul_eq_self_left hx ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ HMul.hMul (α := R) (β := R) ((ψ : (a : A) → R) x : R) (∑ a : A, (ψ : (a : A) → R) a : R) =
    ∑ a : A, (ψ : (a : A) → R) a
have 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)
Tactic: rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ Eq.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ ≠ 0
have rw : Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0
Tactic: rw [sum_eq_ite, Ne.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ Eq.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ ≠ 0
have rw : Eq.{u_2 + 1} (α := R) (if ψ = 0 then (↑(card A) : R) else 0) 0 ↔ ψ ≠ 0
Tactic: classical
  rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ Eq.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ ≠ 0
have rw₁ : ¬ψ = 0 ↔ ψ ≠ 0
Tactic: classical
  rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ Eq.{u_2 + 1} (α := R) (∑ x : A, (ψ : (a : A) → R) x) 0 ↔ ψ ≠ 0
have rw₂ : Ne.{u_2 + 1} (α := R) (↑(card A) : R) 0
Tactic: classical
  rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : CommMonoid M
ψ : AddChar A M
⊢ ψ.compAddMonoidHom negAddMonoidHom * ψ = 1
have h : ∀ (x : A),
  Eq.{u_2 + 1} (α := M) ((ψ.compAddMonoidHom negAddMonoidHom * ψ : (a : A) → M) x : M) ((1 : (a : A) → M) x : M)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_2
inst : AddGroup A
inst_1 : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ Eq.{u_2 + 1} (α := M) ((ψ : (a : A) → M) (-a) : M) (((ψ : (a : A) → M) a)⁻¹ : M)
have h : HMul.hMul (α := M) (β := M) ((ψ : (a : A) → M) (-a) : M) ((ψ : (a : A) → M) a : M) = 1
Tactic: apply eq_inv_of_mul_eq_one_left
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
have rw : Eq.{u_2 + 1} (α := M) ((ψ : (a : A) → M) (-a) : M) (((ψ : (a : A) → M) a)⁻¹ : M)
Tactic: rw [inv_apply, map_neg_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : A) → M) a : M) (((ψ : (a : A) → M) a)⁻¹ : M)
have rw₁ : Eq.{u_2 + 1} (α := M) (((ψ : (a : A) → M) a)⁻¹ : M) (((ψ : (a : A) → M) a)⁻¹ : M)
Tactic: rw [inv_apply, map_neg_eq_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ / χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
have 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)
Tactic: rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ (ψ / χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
have 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)
Tactic: rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ (ψ / χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
have 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)
Tactic: rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ - χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
have 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)
Tactic: rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ (ψ - χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
have 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)
Tactic: rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ (ψ - χ : (a : A) → M) a = HDiv.hDiv (α := M) (β := M) ((ψ : (a : A) → M) a : M) ((χ : (a : A) → M) a : M)
have 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)
Tactic: rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
A : Type u_1
M : Type u_2
inst : AddCommGroup A
inst_1 : DivisionCommMonoid M
n : ℤ
ψ : AddChar A M
a : A
⊢ (n • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) n
have ofNat : ∀ (a_1 : ℕ), (Int.ofNat a_1 • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) (Int.ofNat a_1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ (n • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) n
have negSucc : ∀ (a_1 : ℕ), (Int.negSucc a_1 • ψ : (a : A) → M) a = HPow.hPow (α := M) ((ψ : (a : A) → M) a : M) (Int.negSucc a_1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
⊢ ψ⁻¹ = ψ.mulShift (-1)
have h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
x : R
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
have h : 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
have h₁ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ : (a : R) → M) (-1 * x) : M)
Tactic: rw [inv_apply, mulShift_apply, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
have h₂ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ : (a : R) → M) (-(1 * x)) : M)
Tactic: rw [inv_apply, mulShift_apply, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ⁻¹ : (a : R) → M) x : M) ((ψ.mulShift (-1) : (a : R) → M) x : M)
have h₃ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (-x) : M) ((ψ : (a : R) → M) (-x) : M)
Tactic: rw [inv_apply, mulShift_apply, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ.mulShift (↑n : R) : (a : R) → M) x = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
have rw : (ψ : (a : R) → M) ((↑n : R) * x) = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
Tactic: rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ (ψ.mulShift (↑n : R) : (a : R) → M) x = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
have rw₁ : (ψ : (a : R) → M) (n • x) = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
Tactic: rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ (ψ.mulShift (↑n : R) : (a : R) → M) x = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
have rw₂ : HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n = HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n
Tactic: rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
n : ℕ
⊢ ψ ^ n = ψ.mulShift (↑n : R)
have h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ ^ n : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ Eq.{u_2 + 1} (α := M) ((ψ ^ n : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)
have h : HPow.hPow (α := M) ((ψ : (a : R) → M) x : M) n = (ψ.mulShift (↑n : R) : (a : R) → M) x
Tactic: rw [pow_apply, ← mulShift_spec']
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ Eq.{u_2 + 1} (α := M) ((ψ ^ n : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)
have h₁ : Eq.{u_2 + 1} (α := M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M) ((ψ.mulShift (↑n : R) : (a : R) → M) x : M)
Tactic: rw [pow_apply, ← mulShift_spec']
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s : R
⊢ ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
have 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)
Tactic: rw [mulShift_apply, right_distrib, map_add_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
r s : R
⊢ (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 0 = 1
have h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
x : R
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)
have h : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (0 * x) : M) ((1 : (a : R) → M) x : M)
Tactic: rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)
have h₁ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) 0 : M) ((1 : (a : R) → M) x : M)
Tactic: rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)
have h₂ : Eq.{u_2 + 1} (α := M) (1 : M) ((1 : (a : R) → M) x : M)
Tactic: rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 0 : (a : R) → M) x : M) ((1 : (a : R) → M) x : M)
have h₃ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 1 = ψ
have h : ∀ (x : R), Eq.{u_2 + 1} (α := M) ((ψ.mulShift 1 : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : CommMonoid M
ψ : AddChar R M
x : R
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 1 : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)
have h : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) (1 * x) : M) ((ψ : (a : R) → M) x : M)
Tactic: rw [mulShift_apply, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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)
⊢ Eq.{u_2 + 1} (α := M) ((ψ.mulShift 1 : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)
have h₁ : Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) x : M) ((ψ : (a : R) → M) x : M)
Tactic: rw [mulShift_apply, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
have refine_1 : ∀ (h : ψ.mulShift u = 1), ψ = 1
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ ψ.mulShift u = 1 ↔ ψ = 1
have refine_2 : ψ = 1 → ψ.mulShift u = 1
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ ψ = 1
have refine_1 : ∀ (y : R), Eq.{u_2 + 1} (α := M) ((ψ : (a : R) → M) y : M) ((1 : (a : R) → M) y : M)
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ y = u * ((↑hu.unit⁻¹ : R) * y)
have rw : y = u * (↑hu.unit⁻¹ : R) * y
Tactic: rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ y = u * ((↑hu.unit⁻¹ : R) * y)
have rw₁ : y = 1 * y
Tactic: rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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
⊢ y = u * ((↑hu.unit⁻¹ : R) * y)
have rw₂ : y = y
Tactic: rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.AddChar (goal)
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) y : M) ((1 : (a : R) → M) y : M)
have 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)
Tactic: rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]