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'
a : Rˣ
⊢ (↑((((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')
have simp_rw : (χ₁ * χ₂ : (a : R) → R') (↑a : R) =
  HMul.hMul (α := R') (β := R') ((χ₁ : (a : R) → R') (↑a : R) : R') ((χ₂ : (a : R) → R') (↑a : R) : R')
Tactic: simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]
-- 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ˣ
simp_rw :
  (χ₁ * χ₂ : (a : R) → R') (↑a : R) =
    HMul.hMul (α := R') (β := R') ((χ₁ : (a : R) → R') (↑a : R) : R') ((χ₂ : (a : R) → R') (↑a : R) : R')
⊢ (↑((((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')
have simp_rw₁ : HMul.hMul (α := (a : R) → R') (β := (a : R) → R') (⇑χ₁ : (a : R) → R') (⇑χ₂ : (a : R) → R') (↑a : R) =
  HMul.hMul (α := R') (β := R') ((χ₁ : (a : R) → R') (↑a : R) : R') ((χ₂ : (a : R) → R') (↑a : R) : R')
Tactic: simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]
-- 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'
⊢ Equiv.toFun equivToUnitHom (χ * ψ) = Equiv.toFun equivToUnitHom χ * Equiv.toFun equivToUnitHom ψ
have h : ∀ (x : Rˣ),
  Eq.{u_2 + 1} (α := R') (↑((Equiv.toFun equivToUnitHom (χ * ψ) : (a : Rˣ) → R'ˣ) x) : R')
    (↑((Equiv.toFun equivToUnitHom χ * Equiv.toFun equivToUnitHom ψ : (a : Rˣ) → R'ˣ) x) : 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 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
f : R' →+* R''
⊢ Eq (α := MulChar R R'') (ringHomComp 1 f) 1
have h : ∀ (a : Rˣ),
  Eq.{u_3 + 1} (α := R'') ((ringHomComp 1 f : (a : R) → R'') (↑a : R) : R'') ((1 : (a : R) → R'') (↑a : R) : R'')
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R' : Type u_2
inst : CommRing R'
R'' : Type u_3
inst_1 : CommRing R''
R : Type u_4
inst_2 : CommMonoidWithZero R
χ : MulChar R R'
f : R' →+* R''
⊢ (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f
have h : ∀ (a : Rˣ),
  Eq.{u_3 + 1} (α := R'') (((χ.ringHomComp f)⁻¹ : (a : R) → R'') (↑a : R) : R'')
    ((χ⁻¹.ringHomComp f : (a : R) → R'') (↑a : R) : R'')
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
χ φ : MulChar R R'
f : R' →+* R''
⊢ (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f
have h : ∀ (a : Rˣ),
  Eq.{u_3 + 1} (α := R'') (((χ * φ).ringHomComp f : (a : R) → R'') (↑a : R) : R'')
    ((χ.ringHomComp f * φ.ringHomComp f : (a : R) → R'') (↑a : R) : R'')
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
χ : MulChar R R'
f : R' →+* R''
n : ℕ
⊢ χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
have zero : HPow.hPow (β := ℕ) (χ.ringHomComp f) 0 = (HPow.hPow (β := ℕ) χ 0).ringHomComp f
Tactic: induction n with
  | zero => simp only [pow_zero, ringHomComp_one]
  | succ n ih => simp only [pow_succ, ih, ringHomComp_mul]
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 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
χ : MulChar R R'
f : R' →+* R''
n : ℕ
zero : HPow.hPow (β := ℕ) (χ.ringHomComp f) 0 = (HPow.hPow (β := ℕ) χ 0).ringHomComp f
⊢ χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
have succ : ∀ (n : ℕ) (ih : χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f), χ.ringHomComp f ^ (n + 1) = (χ ^ (n + 1)).ringHomComp f
Tactic: induction n with
  | zero => simp only [pow_zero, ringHomComp_one]
  | succ n ih => simp only [pow_succ, ih, ringHomComp_mul]
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 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
f : R' →+* R''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R') (β := R'') (⇑f : (a : R') → R'')
χ : MulChar R R'
| χ.ringHomComp f = 1
have rw : χ.ringHomComp f = ringHomComp 1 f
Tactic: rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
f : R' →+* R''
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R') (β := R'') (⇑f : (a : R') → R'')
χ : MulChar R R'
⊢ χ.ringHomComp f = 1 ↔ χ = 1
have conv_lhs : χ.ringHomComp f = ringHomComp 1 f ↔ χ = 1
Tactic: conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
⊢ Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
have inl : ∀ (ha : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (0 : R')),
  Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
Tactic: rcases hχ a with (ha | ha | ha)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
inl :
  ∀ (ha : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (0 : R')),
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
        Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
⊢ Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
have inr : ∀ (ha : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (1 : R')),
  Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
Tactic: rcases hχ a with (ha | ha | ha)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
R'' : Type u_3
inst_2 : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
inl :
  ∀ (ha : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (0 : R')),
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
        Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
inr :
  ∀ (ha : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (1 : R')),
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
        Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
⊢ Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
have inr₁ : ∀ (ha : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (-1 : R')),
  Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (0 : R'') ∨
    Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (1 : R'') ∨
      Eq.{u_3 + 1} (α := R'') ((χ.ringHomComp f : (a : R) → R'') a : R'') (-1 : R'')
Tactic: rcases hχ a with (ha | ha | ha)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ χ⁻¹ = χ
have h : ∀ (x : Rˣ), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') (↑x : R) : R') ((χ : (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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (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 [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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h : ∀ (h₀ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')),
  Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
Tactic: rcases hχ x with (h₀ | h₁ | h₂)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h :
  ∀ (h₀ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')),
    Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₁ : ∀ (h₁ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')),
  Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
Tactic: rcases hχ x with (h₀ | h₁ | h₂)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h :
  ∀ (h₀ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')),
    Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
h₁ :
  ∀ (h₁ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')),
    Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₂ : ∀ (h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')),
  Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
Tactic: rcases hχ x with (h₀ | h₁ | h₂)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₀ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h : Eq.{u_2 + 1} (α := R') 0⁻¹ʳ 0
Tactic: rw [h₀, Ring.inverse_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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₀ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')
h : Eq.{u_2 + 1} (α := R') 0⁻¹ʳ 0
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₁ : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [h₀, Ring.inverse_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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₁ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h : Eq.{u_2 + 1} (α := R') 1⁻¹ʳ 1
Tactic: rw [h₁, Ring.inverse_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₁ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')
h : Eq.{u_2 + 1} (α := R') 1⁻¹ʳ 1
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₂ : Eq.{u_2 + 1} (α := R') 1 1
Tactic: rw [h₁, Ring.inverse_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
⊢ Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
have norm_cast : Eq.{u_2 + 1} (α := R') (↑(Int.negSucc 0) : R') (-1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have this : Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
Tactic: have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
this : Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h : Eq.{u_2 + 1} (α := R') (-1)⁻¹ʳ (-1)
Tactic: rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
this : Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
h : Eq.{u_2 + 1} (α := R') (-1)⁻¹ʳ (-1)
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₁ : Eq.{u_2 + 1} (α := R') (↑(-1) : R')⁻¹ʳ (↑(-1) : R')
Tactic: rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
this : Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
h : Eq.{u_2 + 1} (α := R') (-1)⁻¹ʳ (-1)
h₁ : Eq.{u_2 + 1} (α := R') (↑(-1) : R')⁻¹ʳ (↑(-1) : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₃ : Eq.{u_2 + 1} (α := R') (↑(-1)⁻¹ : R') (↑(-1) : R')
Tactic: rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
this : Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
h : Eq.{u_2 + 1} (α := R') (-1)⁻¹ʳ (-1)
h₁ : Eq.{u_2 + 1} (α := R') (↑(-1) : R')⁻¹ʳ (↑(-1) : R')
h₃ : Eq.{u_2 + 1} (α := R') (↑(-1)⁻¹ : R') (↑(-1) : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₄ : Eq.{u_2 + 1} (α := R') (↑(-1⁻¹) : R') (↑(-1) : R')
Tactic: rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
this : Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')
h : Eq.{u_2 + 1} (α := R') (-1)⁻¹ʳ (-1)
h₁ : Eq.{u_2 + 1} (α := R') (↑(-1) : R')⁻¹ʳ (↑(-1) : R')
h₃ : Eq.{u_2 + 1} (α := R') (↑(-1)⁻¹ : R') (↑(-1) : R')
h₄ : Eq.{u_2 + 1} (α := R') (↑(-1⁻¹) : R') (↑(-1) : R')
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R')
have h₅ : Eq.{u_2 + 1} (α := R') (↑(-1) : R') (↑(-1) : R')
Tactic: rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ HPow.hPow (β := ℕ) χ 2 = 1
have rw : HPow.hPow (β := ℕ) χ 2 = χ⁻¹ * χ
Tactic: rw [← inv_mul_cancel χ, pow_two, hχ.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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
rw : HPow.hPow (β := ℕ) χ 2 = χ⁻¹ * χ
⊢ HPow.hPow (β := ℕ) χ 2 = 1
have rw₁ : χ * χ = χ⁻¹ * χ
Tactic: rw [← inv_mul_cancel χ, pow_two, hχ.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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
rw : HPow.hPow (β := ℕ) χ 2 = χ⁻¹ * χ
rw₁ : χ * χ = χ⁻¹ * χ
⊢ HPow.hPow (β := ℕ) χ 2 = 1
have rw₂ : χ * χ = χ * χ
Tactic: rw [← inv_mul_cancel χ, pow_two, hχ.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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
⊢ χ ^ p = χ
have h : ∀ (x : Rˣ), Eq.{u_2 + 1} (α := R') ((χ ^ p : (a : R) → R') (↑x : R) : R') ((χ : (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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ ^ p : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
have h : HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
Tactic: rw [pow_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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
have h : ∀ (hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')),
  HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
Tactic: rcases hχ x with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
h :
  ∀ (hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')),
    HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
have h₁ : ∀ (hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')),
  HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
Tactic: rcases hχ x with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
h :
  ∀ (hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')),
    HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
h₁ :
  ∀ (hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')),
    HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
have h₂ : ∀ (hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')),
  HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
Tactic: rcases hχ x with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
have h : HPow.hPow (α := R') 0 p = 0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
have h : HPow.hPow (α := R') 1 p = 1
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
have h : HPow.hPow (α := R') (-1) p = -1
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')
⊢ HPow.hPow (α := R') 0 p = 0
have h : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [zero_pow (@Fact.out p.Prime).ne_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 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')
⊢ HPow.hPow (α := R') 1 p = 1
have h : Eq.{u_2 + 1} (α := R') 1 1
Tactic: rw [one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even n
⊢ χ ^ n = 1
have obtain : ∀ (n : ℕ) (hn : Even (2 * n)), χ ^ (2 * n) = 1
Tactic: obtain ⟨n, rfl⟩ := even_iff_two_dvd.mp hn
Cleared hypotheses: n, hn