awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
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')
⊢ (((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'ˣ)

Tactic:
apply_fun ((↑) : R'ˣ → R') using Units.val_injective

Premises used: Units.val, Units.val_injective
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
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')
⊢ (↑((((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:
push_cast
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
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')
⊢ (↑((((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:
simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]

Premises used: Pi.mul_apply, MulChar.coe_equivToUnitHom, MulChar.coeToFun_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ ψ : MulChar R R'
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')
⊢ Equiv.toFun equivToUnitHom (χ * ψ) = Equiv.toFun equivToUnitHom χ * Equiv.toFun equivToUnitHom ψ

Tactic:
ext
-- Module: Mathlib.NumberTheory.MulChar.Basic
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') (↑((Equiv.toFun equivToUnitHom (χ * ψ) : (a : Rˣ) → R'ˣ) x) : R')
    (↑((Equiv.toFun equivToUnitHom χ * Equiv.toFun equivToUnitHom ψ : (a : Rˣ) → R'ˣ) x) : R')

Tactic:
simp only [Equiv.toFun_as_coe, coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply,
        MonoidHom.mul_apply, Units.val_mul]

Premises used: Pi.mul_apply, Equiv.toFun_as_coe, MulChar.coe_equivToUnitHom, MulChar.coeToFun_mul, Units.val_mul, MonoidHom.mul_apply
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ = 1 ↔ ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') (1 : R')

Tactic:
simp only [MulChar.ext_iff, one_apply_coe]

Premises used: MulChar.one_apply_coe, MulChar.ext_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ ≠ 1 ↔ ∃ (a : Rˣ), Ne.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') (1 : R')

Tactic:
simp only [Ne, eq_one_iff, not_forall]

Premises used: MulChar.eq_one_iff, Ne, Classical.not_forall
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
S : Type u_3
inst_2 : SetLike S R
inst_3 : SubmonoidClass S R
T : S
χ : MulChar R R'
⊢ Eq (α := MulChar.{u_1, u_2} (↥T) R') (restrict T χ) 1 ↔
    ∀ (x : (↥T)ˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑(↑x : ↥T) : R) : R') (1 : R')

Tactic:
simp [eq_one_iff]

Premises used: MulChar.eq_one_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 ℤ
hχ : χ.IsQuadratic
χ' : MulChar R' ℤ
hχ' : χ'.IsQuadratic
inst_3 : Nontrivial R''
hR'' : ringChar R'' ≠ 2
a : R
a' : R'
h : Eq.{u_3 + 1} (α := R'') (↑((χ : (a : R) → ℤ) a) : R'') (↑((χ' : (a : R') → ℤ) a') : R'')
⊢ Eq (α := ℤ) ((χ : (a : R) → ℤ) a : ℤ) ((χ' : (a : R') → ℤ) a' : ℤ)

Tactic:
Int.cast_injOn_of_ringChar_ne_two hR'' (hχ a) (hχ' a') h

Premises used: Int.cast_injOn_of_ringChar_ne_two
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
a : R
ha : ¬IsUnit a
⊢ Eq.{u_3 + 1} (α := R'') ((f : (a : R') → R'') ((χ : (a : R) → R') a : R') : R'') (0 : R'')

Tactic:
simp only [map_nonunit χ ha, map_zero]

Premises used: map_zero, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
h :
  ∀ (a : Rˣ),
    Eq.{u_3 + 1} (α := R'') ((ringHomComp 1 f : (a : R) → R'') (↑a : R) : R'') ((1 : (a : R) → R'') (↑a : R) : R'')
⊢ Eq (α := MulChar R R'') (ringHomComp 1 f) 1

Tactic:
ext1
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
a : Rˣ
⊢ Eq.{u_3 + 1} (α := R'') ((ringHomComp 1 f : (a : R) → R'') (↑a : R) : R'') ((1 : (a : R) → R'') (↑a : R) : R'')

Tactic:
simp only [MulChar.ringHomComp_apply, MulChar.one_apply_coe, map_one]

Premises used: MulChar.one_apply_coe, MulChar.ringHomComp_apply, map_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
h :
  ∀ (a : Rˣ),
    Eq.{u_3 + 1} (α := R'') (((χ.ringHomComp f)⁻¹ : (a : R) → R'') (↑a : R) : R'')
      ((χ⁻¹.ringHomComp f : (a : R) → R'') (↑a : R) : R'')
⊢ (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f

Tactic:
ext1
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
a : Rˣ
⊢ Eq.{u_3 + 1} (α := R'') (((χ.ringHomComp f)⁻¹ : (a : R) → R'') (↑a : R) : R'')
    ((χ⁻¹.ringHomComp f : (a : R) → R'') (↑a : R) : R'')

Tactic:
simp only [inv_apply, Ring.inverse_unit, ringHomComp_apply]

Premises used: MulChar.ringHomComp_apply, Ring.inverse_unit, MulChar.inv_apply
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
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'')
⊢ (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f

Tactic:
ext1
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
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:
simp only [ringHomComp_apply, coeToFun_mul, Pi.mul_apply, map_mul]

Premises used: Pi.mul_apply, MulChar.ringHomComp_apply, map_mul, MulChar.coeToFun_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
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''
⊢ HPow.hPow (β := ℕ) (χ.ringHomComp f) 0 = (HPow.hPow (β := ℕ) χ 0).ringHomComp f

Tactic:
simp only [pow_zero, ringHomComp_one]

Premises used: pow_zero, MulChar.ringHomComp_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 : ℕ
ih : χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
⊢ χ.ringHomComp f ^ (n + 1) = (χ ^ (n + 1)).ringHomComp f

Tactic:
simp only [pow_succ, ih, ringHomComp_mul]

Premises used: pow_succ, MulChar.ringHomComp_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
succ :
  ∀ (n : ℕ) (ih : χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f), χ.ringHomComp f ^ (n + 1) = (χ ^ (n + 1)).ringHomComp f
⊢ χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f

Tactic:
induction n with
  | zero => simp only [pow_zero, ringHomComp_one]
  | succ n ih => simp only [pow_succ, ih, ringHomComp_mul]

Premises used: pow_succ, pow_zero, MulChar.ringHomComp_mul, MulChar.ringHomComp_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
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'')
⊢ Function.Injective (β := MulChar R R'') fun (x : MulChar R R') ↦ x.ringHomComp f

Tactic:
simpa
    only [Function.Injective, MulChar.ext_iff, ringHomComp, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
    using fun χ χ' h a ↦ hf (h a)

Premises used: OneHom.coe_mk, MulChar.coe_mk, MonoidHom.coe_mk, Function.Injective, MulChar.ext_iff, MulChar.ringHomComp
-- Module: Mathlib.NumberTheory.MulChar.Basic
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'
⊢ Eq (α := MulChar R R'') (ringHomComp 1 f) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.MulChar.Basic
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'
rw : χ.ringHomComp f = ringHomComp 1 f
| χ.ringHomComp f = 1

Tactic:
rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
-- Module: Mathlib.NumberTheory.MulChar.Basic
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'
conv_lhs : χ.ringHomComp f = ringHomComp 1 f ↔ χ = 1
⊢ χ.ringHomComp f = 1 ↔ χ = 1

Tactic:
conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 = ringHomComp 1 f ↔ χ = 1

Tactic:
(injective_ringHomComp hf).eq_iff

Premises used: MulChar.injective_ringHomComp, Function.Injective.eq_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 = ringHomComp 1 f ↔ χ = 1

Tactic:
exact (injective_ringHomComp hf).eq_iff

Premises used: MulChar.injective_ringHomComp, Function.Injective.eq_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
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

Tactic:
(ringHomComp_eq_one_iff hf).not

Premises used: Iff.not, MulChar.ringHomComp_eq_one_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
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'')
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'')

Tactic:
rcases hχ a with (ha | ha | ha)
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
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:
simp [ha]
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
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:
simp [ha]
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
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:
simp [ha]
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
h : ∀ (x : Rˣ), Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
⊢ χ⁻¹ = χ

Tactic:
ext x
-- Module: Mathlib.NumberTheory.MulChar.Basic
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') ((χ : (a : R) → R') (↑x : R) : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')

Tactic:
rw [inv_apply_eq_inv]

Premises used: MulChar.inv_apply_eq_inv
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
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')

Tactic:
rcases hχ x with (h₀ | h₁ | h₂)

Premises used: Units.val
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
h₁ 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')

Tactic:
rw [h₀, Ring.inverse_zero]

Premises used: Ring.inverse_zero
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
h₂ 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')

Tactic:
rw [h₁, Ring.inverse_one]

Premises used: Ring.inverse_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
norm_cast : Eq.{u_2 + 1} (α := R') (↑(Int.negSucc 0) : R') (-1)
⊢ Eq.{u_2 + 1} (α := R') (-1) (↑(-1) : R')

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.MulChar.Basic
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') (↑(Int.negSucc 0) : R') (-1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')

Tactic:
have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
h₅ 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')

Tactic:
rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]

Premises used: inv_one, inv_neg, Ring.inverse_unit, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.MulChar.Basic
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₁ : χ * χ = χ⁻¹ * χ
rw₂ rw₃ : χ * χ = χ * χ
⊢ HPow.hPow (β := ℕ) χ 2 = 1

Tactic:
rw [← inv_mul_cancel χ, pow_two, hχ.inv]

Premises used: inv_mul_cancel, pow_two, MulChar.IsQuadratic.inv
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
h : ∀ (x : Rˣ), Eq.{u_2 + 1} (α := R') ((χ ^ p : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
⊢ χ ^ p = χ

Tactic:
ext x
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 : HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)
⊢ Eq.{u_2 + 1} (α := R') ((χ ^ p : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')

Tactic:
rw [pow_apply_coe]

Premises used: MulChar.pow_apply_coe
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
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)

Tactic:
rcases hχ x with (hx | hx | hx)

Premises used: Units.val
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
h : HPow.hPow (α := R') 0 p = 0
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)

Tactic:
rw [hx]
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
h : HPow.hPow (α := R') 1 p = 1
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)

Tactic:
rw [hx]