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'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
intro intro₁ :
  ∀ (x y : R),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
pos :
  ∀ (x y : R) (hx : IsUnit x),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
neg neg₁ :
  ∀ (x y : R) (hx : ¬IsUnit x),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
⊢ ∀ (x y : R),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)

Tactic:
classical
      intro x y
      by_cases hx : IsUnit x
      · simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
        by_cases hy : IsUnit y
        · simp only [hy, dif_pos]
          have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
          rw [hm, map_mul]
          norm_cast
        · simp only [hy, not_false_iff, dif_neg, mul_zero]
      · simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]

Premises used: IsUnit.mul_iff, MulZeroClass.zero_mul, false_and, dif_pos, dif_neg, MulZeroClass.mul_zero, map_mul, not_false_iff, true_and
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
a : R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') (if hx : IsUnit a then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) 0

Tactic:
simp only [ha, not_false_iff, dif_neg]

Premises used: dif_neg, not_false_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((ofUnitHom f : (a : R) → R') (↑a : R) : R') ((↑((f : (a : Rˣ) → R'ˣ) a) : R') : R')

Tactic:
simp [ofUnitHom]

Premises used: MulChar.ofUnitHom
-- 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') ((ofUnitHom χ.toUnitHom : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
⊢ ofUnitHom χ.toUnitHom = χ

Tactic:
ext x
-- 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ˣ
h : Eq.{u_2 + 1} (α := R') ((↑((χ.toUnitHom : (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') ((χ : (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')

Tactic:
rw [ofUnitHom_coe, coe_toUnitHom]

Premises used: MulChar.coe_toUnitHom, MulChar.ofUnitHom_coe
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
h :
  ∀ (x : Rˣ),
    Eq.{u_2 + 1} (α := R') (↑(((ofUnitHom f).toUnitHom : (a : Rˣ) → R'ˣ) x) : R') (↑((f : (a : Rˣ) → R'ˣ) x) : R')
⊢ (ofUnitHom f).toUnitHom = f

Tactic:
ext x
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x : Rˣ
⊢ Eq.{u_2 + 1} (α := R') (↑(((ofUnitHom f).toUnitHom : (a : Rˣ) → R'ˣ) x) : R') (↑((f : (a : Rˣ) → R'ˣ) x) : R')

Tactic:
simp only [coe_toUnitHom, ofUnitHom_coe]

Premises used: MulChar.coe_toUnitHom, MulChar.ofUnitHom_coe
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ.toUnitHom = (equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ

Tactic:
rfl

Premises used: MonoidHom.mk', MulChar.toUnitHom, rfl, Units.map
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ
⊢ ofUnitHom χ = (Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') χ

Tactic:
rfl

Premises used: MulChar.ofUnitHom, rfl
-- 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ˣ
⊢ Eq.{u_2 + 1} (α := R')
    ((↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ : MonoidHom.{u_1, u_2} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) a) :
        R') :
      R')
    ((χ : (a : R) → R') (↑a : R) : R')

Tactic:
coe_toUnitHom χ a

Premises used: MulChar.coe_toUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R')
    ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R') (↑a : R) : R')
    ((↑((f : (a : Rˣ) → R'ˣ) a) : R') : R')

Tactic:
ofUnitHom_coe f a

Premises used: MulChar.ofUnitHom_coe
-- 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') ((χ.toMonoidHom : (a : R) → R') x : R') ((χ : (a : R) → R') x : R')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') 1 : R') (1 : R')

Tactic:
χ.map_one'

Premises used: OneHom.map_one', MonoidHom.toOneHom, MulChar.toMonoidHom
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
inst_2 : Nontrivial R
χ : MulChar R R'
rw rw₁ : Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') 0 : R') (0 : R')

Tactic:
rw [map_nonunit χ not_isUnit_zero]

Premises used: not_isUnit_zero, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
rw₁ rw₂ : Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑(ringChar R) : R) : R') (0 : R')

Tactic:
rw [ringChar.Nat.cast_ringChar, χ.map_zero]

Premises used: ringChar.Nat.cast_ringChar, MulChar.map_zero
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (↑a : R) : R') (1 : R')

Tactic:
dif_pos a.isUnit

Premises used: dif_pos, dite, Units.isUnit, ite
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (↑a : R) : R') (1 : R')

Tactic:
exact dif_pos a.isUnit

Premises used: dif_pos, Units.isUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (↑a : R) : R') (1 : R')

Tactic:
classical exact dif_pos a.isUnit

Premises used: dif_pos, Units.isUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x : R
hx : IsUnit x
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') x : R') (1 : R')

Tactic:
one_apply_coe hx.unit

Premises used: MulChar.one_apply_coe, IsUnit.unit
-- 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
ha : ¬IsUnit a
⊢ HMul.hMul (α := (a : R) → R') (β := (a : R) → R') (⇑χ : (a : R) → R') (⇑χ' : (a : R) → R') a = 0

Tactic:
simp only [map_nonunit χ ha, zero_mul, Pi.mul_apply]

Premises used: Pi.mul_apply, MulZeroClass.zero_mul, MulChar.map_nonunit
-- 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
⊢ (χ * χ' : (a : R) → R') a = HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')

Tactic:
rfl

Premises used: rfl
-- 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) → R') = HMul.hMul (α := (a : R) → R') (⇑χ : (a : R) → R') (⇑χ' : (a : R) → R')

Tactic:
rfl

Premises used: rfl
-- 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 : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((1 * χ : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')
⊢ 1 * χ = χ

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'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((1 * χ : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')

Tactic:
simp only [one_mul, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]

Premises used: Pi.mul_apply, MulChar.one_apply_coe, MulChar.coeToFun_mul, one_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 : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ * 1 : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')
⊢ χ * 1 = χ

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'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ * 1 : (a : R) → R') (↑a : R) : R') ((χ : (a : R) → R') (↑a : R) : R')

Tactic:
simp only [mul_one, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]

Premises used: Pi.mul_apply, MulChar.one_apply_coe, mul_one, 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'
a : R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((MonoidWithZero.inverse : (a : R') → R') ((χ : (a : R) → R') a : R') : R') (0 : R')

Tactic:
simp [map_nonunit _ ha]

Premises used: MulChar.map_nonunit
-- 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
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') (((χ : (a : R) → R') a)⁻¹ʳ : R')

Tactic:
Eq.refl <| inv χ a

Premises used: Ring.inverse, MulChar.inv, dite, Eq.refl, DFunLike.coe
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommGroupWithZero R'
χ : MulChar R R'
a : R
⊢ Eq.{u_3 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') (((χ : (a : R) → R') a)⁻¹ : R')

Tactic:
(inv_apply_eq_inv χ a).trans <| Ring.inverse_eq_inv (χ a)

Premises used: MulChar.inv_apply_eq_inv, Ring.inverse_eq_inv, DFunLike.coe, Eq.trans
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
neg : ∀ (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')

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
pos : 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')

Tactic:
rw [inv_apply_eq_inv]

Premises used: MulChar.inv_apply_eq_inv
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ IsUnit.{u_2} (M := R') ((χ : (a : R) → R') a : R')

Tactic:
have h := IsUnit.map χ ha
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
⊢ Function.Injective (β := R') fun (x : R') ↦ HMul.hMul (α := R') ((χ : (a : R) → R') a : R') x

Tactic:
IsUnit.mul_right_injective h

Premises used: IsUnit.mul_right_injective
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 :
  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⁻¹ʳ))
⊢ Eq.{u_2 + 1} (α := R') (((χ : (a : R) → R') a)⁻¹ʳ : R') ((χ : (a : R) → R') a⁻¹ʳ : R')

Tactic:
apply_fun (χ a * ·) using IsUnit.mul_right_injective h

Premises used: HMul.hMul, IsUnit.mul_right_injective, DFunLike.coe
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
pos₃ pos₄ : Eq.{u_2 + 1} (α := R') 1 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')

Tactic:
rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]

Premises used: Ring.mul_inverse_cancel, map_mul, map_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
neg : ∀ (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')

Tactic:
revert ha
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
rw₂ rw₃ : Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ʳ : R')

Tactic:
rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]

Premises used: Ring.inverse_non_unit, MulChar.map_nonunit, MulChar.map_zero
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R' : Type u_2
inst : CommMonoidWithZero R'
R : Type u_3
inst_1 : CommGroupWithZero R
χ : MulChar R R'
a : R
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ : (a : R) → R') a : R') ((χ : (a : R) → R') a⁻¹ : R')

Tactic:
(inv_apply χ a).trans <| congr_arg _ (Ring.inverse_eq_inv a)

Premises used: Ring.inverse_eq_inv, congr_arg, MulChar.inv_apply, Eq.trans
-- 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') ((χ⁻¹ * χ : (a : R) → R') (↑x : R) : R') ((1 : (a : R) → R') (↑x : R) : R')
⊢ χ⁻¹ * χ = 1

Tactic:
ext x
-- 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ˣ
h :
  HMul.hMul (α := R') (β := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R') =
    (1 : (a : R) → R') (↑x : R)
⊢ Eq.{u_2 + 1} (α := R') ((χ⁻¹ * χ : (a : R) → R') (↑x : R) : R') ((1 : (a : R) → R') (↑x : R) : R')

Tactic:
rw [coeToFun_mul, Pi.mul_apply, inv_apply_eq_inv]

Premises used: Pi.mul_apply, MulChar.inv_apply_eq_inv, 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'
x : Rˣ
h : Eq.{u_2 + 1} (α := R') (1 : R') ((1 : (a : R) → R') (↑x : R) : R')
⊢ HMul.hMul (α := R') (β := R') (((χ : (a : R) → R') (↑x : R))⁻¹ʳ : R') ((χ : (a : R) → R') (↑x : R) : R') =
    (1 : (a : R) → R') (↑x : R)

Tactic:
simp only [Ring.inverse_mul_cancel _ (IsUnit.map χ x.isUnit)]

Premises used: Ring.inverse_mul_cancel, IsUnit.map, Units.isUnit
-- 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ˣ
h h₁ : Eq.{u_2 + 1} (α := R') 1 1
⊢ Eq.{u_2 + 1} (α := R') (1 : R') ((1 : (a : R) → R') (↑x : R) : R')

Tactic:
rw [one_apply_coe]

Premises used: MulChar.one_apply_coe
-- 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 :
  ∀ (a : Rˣ),
    Eq.{u_2 + 1} (α := R') ((χ₁ * χ₂ * χ₃ : (a : R) → R') (↑a : R) : R') ((χ₁ * (χ₂ * χ₃) : (a : R) → R') (↑a : R) : R')
⊢ χ₁ * χ₂ * χ₃ = χ₁ * (χ₂ * χ₃)

Tactic:
ext a
-- 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ˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ₁ * χ₂ * χ₃ : (a : R) → R') (↑a : R) : R') ((χ₁ * (χ₂ * χ₃) : (a : R) → R') (↑a : R) : R')

Tactic:
simp only [mul_assoc, Pi.mul_apply, MulChar.coeToFun_mul]

Premises used: Pi.mul_apply, mul_assoc, 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 : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ₁ * χ₂ : (a : R) → R') (↑a : R) : R') ((χ₂ * χ₁ : (a : R) → R') (↑a : R) : R')
⊢ χ₁ * χ₂ = χ₂ * χ₁

Tactic:
ext a
-- 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ˣ
⊢ Eq.{u_2 + 1} (α := R') ((χ₁ * χ₂ : (a : R) → R') (↑a : R) : R') ((χ₂ * χ₁ : (a : R) → R') (↑a : R) : R')

Tactic:
simp only [mul_comm, Pi.mul_apply, MulChar.coeToFun_mul]

Premises used: Pi.mul_apply, mul_comm, 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'
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')
zero₂ zero₃ : Eq.{u_2 + 1} (α := R') 1 1
⊢ (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0

Tactic:
rw [pow_zero, pow_zero, one_apply_coe]

Premises used: MulChar.one_apply_coe, pow_zero
-- 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ˣ
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')
succ₃ 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')
⊢ (χ ^ (n + 1) : (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]

Premises used: pow_succ, MulChar.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'
n : ℕ
a : Rˣ
zero :
  (HPow.hPow (β := ℕ) χ 0 : (a : R) → R') (↑a : R) = HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑a : R) : R') 0
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)
⊢ (χ ^ n : (a : R) → R') (↑a : R) = HPow.hPow (α := R') ((χ : (a : R) → R') (↑a : R) : R') n

Tactic:
induction n with
  | zero => rw [pow_zero, pow_zero, one_apply_coe]
  | succ n ih => rw [pow_succ, pow_succ, mul_apply, ih]

Premises used: MulChar.one_apply_coe, pow_succ, pow_zero, MulChar.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'
n : ℕ
hn : n ≠ 0
a : R
pos : ∀ (ha : IsUnit a), (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n
neg : ∀ (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

Tactic:
by_cases ha : IsUnit a

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

Tactic:
pow_apply_coe χ n ha.unit

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

Tactic:
exact pow_apply_coe χ n ha.unit

Premises used: MulChar.pow_apply_coe, IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
neg₂ neg₃ : Eq.{u_2 + 1} (α := R') 0 0
⊢ (χ ^ n : (a : R) → R') a = HPow.hPow (α := R') ((χ : (a : R) → R') a : R') n

Tactic:
rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]

Premises used: HPow.hPow, MulChar.map_nonunit, zero_pow
-- 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ˣ
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := R'ˣ) Units.val

Tactic:
Units.val_injective

Premises used: Units.val_injective