awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((ofUnitHom χ.toUnitHom : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
have h : Eq.{u_2 + 1} (α := R') ((↑((χ.toUnitHom : (a : Rˣ) → R'ˣ) x) : R') : R') ((χ : (a : R) → R') (↑x : R) : R')
Tactic: rw [ofUnitHom_coe, coe_toUnitHom]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
h : Eq.{u_2 + 1} (α := R') ((↑((χ.toUnitHom : (a : Rˣ) → R'ˣ) x) : R') : R') ((χ : (a : R) → R') (↑x : R) : R')
⊢ Eq.{u_2 + 1} (α := R') ((ofUnitHom χ.toUnitHom : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₁ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
Tactic: rw [ofUnitHom_coe, coe_toUnitHom]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
⊢ (ofUnitHom f).toUnitHom = f
have h : ∀ (x : Rˣ),
  Eq.{u_2 + 1} (α := R') (↑(((ofUnitHom f).toUnitHom : (a : Rˣ) → R'ˣ) x) : R') (↑((f : (a : Rˣ) → R'ˣ) x) : R')
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
inst_2 : Nontrivial R
χ : MulChar R R'
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') 0 : R') (0 : R')
have rw : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [map_nonunit χ not_isUnit_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommSemiring R
inst_2 : Nontrivial R
χ : MulChar R R'
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑(ringChar R) : R) : R') (0 : R')
have rw : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') 0 : R') (0 : R')
Tactic: rw [ringChar.Nat.cast_ringChar, χ.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommSemiring R
inst_2 : Nontrivial R
χ : MulChar R R'
rw : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') 0 : R') (0 : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑(ringChar R) : R) : R') (0 : R')
have rw₁ : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [ringChar.Nat.cast_ringChar, χ.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ 1 * χ = χ
have h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((1 * χ : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ * 1 = χ
have h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ * 1 : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos : ∀ (ha : IsUnit a), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
pos : ∀ (ha : IsUnit a), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have neg : ∀ (ha : ¬IsUnit a), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos : Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') a)⁻¹ʳ : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
Tactic: rw [inv_apply_eq_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') a)⁻¹ʳ : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have h : IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')
Tactic: have h := IsUnit.map χ ha
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') a)⁻¹ʳ : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos : Eq.{u_2 + 1} (α := R') ((fun (x : R') ↦ HMul.hMul (α := R') ((χ : (a : R) → R') a : R') x) ((χ : (a : R) → R') a)⁻¹ʳ)
  ((fun (x : R') ↦ HMul.hMul (α := R') ((χ : (a : R) → R') a : R') x) ((χ : (a : R) → R') a⁻¹ʳ))
Tactic: apply_fun (χ a * ·) using IsUnit.mul_right_injective h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') (((χ : (a : R) → R') a)⁻¹ʳ : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos : 1 = HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
Tactic: rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')
pos : 1 = HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') (((χ : (a : R) → R') a)⁻¹ʳ : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos₁ : Eq.{u_2 + 1} (α := R') (1 : R') ((χ : (a : R) → R') (a * a⁻¹ʳ) : R')
Tactic: rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')
pos : 1 = HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
pos₁ : Eq.{u_2 + 1} (α := R') (1 : R') ((χ : (a : R) → R') (a * a⁻¹ʳ) : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') (((χ : (a : R) → R') a)⁻¹ʳ : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos₂ : Eq.{u_2 + 1} (α := R') (1 : R') ((χ : (a : R) → R') 1 : R')
Tactic: rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')
pos : 1 = HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
pos₁ : Eq.{u_2 + 1} (α := R') (1 : R') ((χ : (a : R) → R') (a * a⁻¹ʳ) : R')
pos₂ : Eq.{u_2 + 1} (α := R') (1 : R') ((χ : (a : R) → R') 1 : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') (((χ : (a : R) → R') a)⁻¹ʳ : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have pos₃ : Eq.{u_2 + 1} (α := R') 1 1
Tactic: rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have neg : ∀ (ha : ¬IsUnit a), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
Tactic: revert ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ∀ (ha : ¬IsUnit a), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have a₁ : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
h : Nontrivial R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have rw : Eq.{u_2 + 1} (α := R') (0 : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
Tactic: rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
h : Nontrivial R
ha : ¬IsUnit a
rw : Eq.{u_2 + 1} (α := R') (0 : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have rw₁ : Eq.{u_2 + 1} (α := R') (0 : R') ((χ : (a : R) → R') 0 : R')
Tactic: rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
h : Nontrivial R
ha : ¬IsUnit a
rw : Eq.{u_2 + 1} (α := R') (0 : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
rw₁ : Eq.{u_2 + 1} (α := R') (0 : R') ((χ : (a : R) → R') 0 : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')
have rw₂ : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ⁻¹ * χ = 1
have h : ∀ (x : Rˣ), Eq.{u_2 + 1} (α := R') ((χ⁻¹ * χ : (a : R) → R') (↑x : R) : R') ((1 : (a : R) → R') (↑x : R) : R')
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ * χ : (a : R) → R') (↑x : R) : R') ((1 : (a : R) → R') (↑x : R) : R')
have h : HMul.hMul (α := R') (β := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R') =
  (1 : (a : R) → R') (↑x : R)
Tactic: rw [coeToFun_mul, Pi.mul_apply, inv_apply_eq_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ HMul.hMul (α := R') (β := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R') =
    (1 : (a : R) → R') (↑x : R)
have h : Eq.{u_2 + 1} (α := R') (1 : R') ((1 : (a : R) → R') (↑x : R) : R')
Tactic: simp only [Ring.inverse_mul_cancel _ (IsUnit.map χ x.isUnit)]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') (1 : R') ((1 : (a : R) → R') (↑x : R) : R')
have h : Eq.{u_2 + 1} (α := R') 1 1
Tactic: rw [one_apply_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ χ₂ χ₃ : MulChar R R'
⊢ χ₁ * χ₂ * χ₃ = χ₁ * (χ₂ * χ₃)
have h : ∀ (a : Rˣ),
  Eq.{u_2 + 1} (α := R') ((χ₁ * χ₂ * χ₃ : (a : R) → R') (↑a : R) : R') ((χ₁ * (χ₂ * χ₃) : (a : R) → R') (↑a : R) : R')
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
⊢ χ₁ * χ₂ = χ₂ * χ₁
have h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ₁ * χ₂ : (a : R) → R') (↑a : R) : R') ((χ₂ * χ₁ : (a : R) → R') (↑a : R) : R')
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
have zero : (1 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
Tactic: rw [pow_zero, pow_zero, one_apply_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
zero : (1 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
⊢ (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
have zero₁ : Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (↑a : R) : R') (1 : R')
Tactic: rw [pow_zero, pow_zero, one_apply_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
zero : (1 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
zero₁ : Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (↑a : R) : R') (1 : R')
⊢ (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
have zero₂ : Eq.{u_2 + 1} (α := R') 1 1
Tactic: rw [pow_zero, pow_zero, one_apply_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n
⊢ (χ ^ (n + 1) : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
have succ : (χ ^ n * χ : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
Tactic: rw [pow_succ, pow_succ, mul_apply, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n
succ : (χ ^ n * χ : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
⊢ (χ ^ (n + 1) : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
have succ₁ : (χ ^ n * χ : (a : R) → R') (↑a : R) =
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R')
Tactic: rw [pow_succ, pow_succ, mul_apply, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n
succ : (χ ^ n * χ : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
succ₁ :
  (χ ^ n * χ : (a : R) → R') (↑a : R) =
    HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R')
⊢ (χ ^ (n + 1) : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
have succ₂ : HMul.hMul (α := R') (β := R') ((χ ^ n : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R') =
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R')
Tactic: rw [pow_succ, pow_succ, mul_apply, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n
succ : (χ ^ n * χ : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
succ₁ :
  (χ ^ n * χ : (a : R) → R') (↑a : R) =
    HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R')
succ₂ :
  HMul.hMul (α := R') (β := R') ((χ ^ n : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R') =
    HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R')
⊢ (χ ^ (n + 1) : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
have succ₃ : HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R') =
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n) ((χ : (a : R) → R') (↑a : R) : R')
Tactic: rw [pow_succ, pow_succ, mul_apply, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
⊢ (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n
have zero : (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
Tactic: induction n with
  | zero => rw [pow_zero, pow_zero, one_apply_coe]
  | succ n ih => rw [pow_succ, pow_succ, mul_apply, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
zero :
  (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
⊢ (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n
have succ : ∀ (n : ℕ) (ih : (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n),
  (χ ^ (n + 1) : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') (n + 1)
Tactic: induction n with
  | zero => rw [pow_zero, pow_zero, one_apply_coe]
  | succ n ih => rw [pow_succ, pow_succ, mul_apply, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
⊢ (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
have pos : ∀ (ha : IsUnit a), (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
pos : ∀ (ha : IsUnit a), (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
⊢ (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
have neg : ∀ (ha : ¬IsUnit a), (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
⊢ (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
have neg : 0 = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
Tactic: rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
neg : 0 = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
⊢ (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
have neg₁ : 0 = HPow.hPow (α := R') 0 n
Tactic: rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
neg : 0 = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
neg₁ : 0 = HPow.hPow (α := R') 0 n
⊢ (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
have neg₂ : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) (χ₁ * χ₂) : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a =
    HMul.hMul (α := R'ˣ) (β := R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a : R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a : R'ˣ)
have apply_fun : (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) (χ₁ * χ₂) : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a) :
    R') =
  (↑(HMul.hMul (α := R'ˣ) (β := R'ˣ)
        ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a :
          R'ˣ)
        ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a :
          R'ˣ)) :
    R')
Tactic: apply_fun ((↑) : R'ˣ → R') using Units.val_injective
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) (χ₁ * χ₂) : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a) :
      R') =
    (↑(HMul.hMul (α := R'ˣ) (β := R'ˣ)
          ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a :
            R'ˣ)
          ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a :
            R'ˣ)) :
      R')
have push_cast : (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) (χ₁ * χ₂) : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a) :
    R') =
  HMul.hMul (α := R')
    (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a) : R')
    (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a) : R')
Tactic: push_cast