awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
refine_1 :
  (∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)) →
    ∀ (χ : MulChar M R) (hχ : Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)),
      Ne.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
refine_2 :
  (∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)) →
    ∀ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ) (hφ : Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)),
      Ne.{u_2 + 1} (α := R) ((ofUnitHom φ : (a : M) → R) (↑a : M) : R) (1 : R)
⊢ (∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)) ↔
    ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)

Tactic:
refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
h : ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
χ : MulChar M R
hχ : Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
refine_1 :
  ∀ (hχ : Eq.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)),
    Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
⊢ Ne.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)

Tactic:
contrapose hχ
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
h : ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
χ : MulChar M R
hχ : Eq.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
refine_1 :
  ∀ (hχ : Eq.{u_2 + 1} (α := R) (↑((χ.toUnitHom : (a : Mˣ) → Rˣ) a) : R) (↑1 : R)),
    Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  ∀ (hχ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) ((↑1 : R) : R)),
    Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)

Tactic:
rwa [Units.ext_iff, coe_toUnitHom] at hχ

Premises used: Units.ext_iff, MulChar.coe_toUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
h : ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
φ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hφ : Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
refine_2 :
  ∀ (hφ : Eq.{u_2 + 1} (α := R) ((ofUnitHom φ : (a : M) → R) (↑a : M) : R) (1 : R)),
    Eq.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
⊢ Ne.{u_2 + 1} (α := R) ((ofUnitHom φ : (a : M) → R) (↑a : M) : R) (1 : R)

Tactic:
contrapose hφ
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
h : ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
φ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hφ : Eq.{u_2 + 1} (α := R) ((ofUnitHom φ : (a : M) → R) (↑a : M) : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)

Tactic:
simpa only [ofUnitHom_eq, equivToUnitHom_symm_coe, Units.val_eq_one] using hφ

Premises used: MulChar.equivToUnitHom_symm_coe, MulChar.ofUnitHom_eq, Units.val_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
pos : ∀ (hu : IsUnit a), ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)
neg : ∀ (hu : ¬IsUnit a), ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)
⊢ ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)

Tactic:
by_cases hu : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)

Tactic:
(exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_

Premises used: Iff.mpr, MulChar.exists_apply_ne_one_iff_exists_monoidHom, IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
pos : ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) hu.unit : Rˣ) (1 : Rˣ)
⊢ ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)

Tactic:
refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_

Premises used: Iff.mpr, MulChar.exists_apply_ne_one_iff_exists_monoidHom, IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) hu.unit : Rˣ) (1 : Rˣ)

Tactic:
CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_

Premises used: CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity, Units
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
pos : hu.unit ≠ 1
⊢ ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) hu.unit : Rˣ) (1 : Rˣ)

Tactic:
refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_

Premises used: CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity, Units
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
pos : ∀ (ha : hu.unit = 1), a = 1
⊢ hu.unit ≠ 1

Tactic:
contrapose ha
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
hu : IsUnit a
ha : hu.unit = 1
pos : (↑hu.unit : M) = 1
pos₁ : Eq.{u_1 + 1} (α := M) (↑1 : M) 1
pos₂ pos₃ : Eq.{u_1 + 1} (α := Mˣ) 1 1
⊢ a = 1

Tactic:
rw [← hu.unit_spec, ha, Units.val_eq_one]

Premises used: Units.val_eq_one, IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ Ne.{u_2 + 1} (α := R) ((1 : (a : M) → R) a : R) (1 : R)

Tactic:
simpa only [map_nonunit _ hu] using zero_ne_one

Premises used: zero_ne_one, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
inst_4 : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)

Tactic:
exact ⟨1, by simpa only [map_nonunit _ hu] using zero_ne_one⟩
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
⊢ Nonempty (MulChar M R ≃* Mˣ)

Tactic:
⟨mulEquivToUnitHom.trans
    (CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity Mˣ R).some⟩

Premises used: CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, MulEquiv.trans, Units, Nonempty.some, Nonempty.intro, MulChar.mulEquivToUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
⊢ Nat.card (MulChar M R) = Nat.card.{u_1} Mˣ

Tactic:
Nat.card_congr (mulEquiv_units M R).some.toEquiv

Premises used: MulChar.mulEquiv_units, Nonempty.some, MulEquiv.toEquiv, Nat.card_congr
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
N : Submonoid M
χ : MulChar.{u_1, u_2} (↥N) R
obtain :
  ∀ (ψ : MonoidHom.{u_1, u_2} Mˣ Rˣ)
    (hψ :
      Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
        ((MonoidHom.restrictHom N.units Rˣ : (a : Mˣ →* Rˣ) → ↥N.units →* Rˣ) ψ : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
        (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ) : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)),
    ∃ (a : MulChar M R), (restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) a = χ
⊢ ∃ (a : MulChar M R), (restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) a = χ

Tactic:
obtain ⟨ψ, hψ⟩ := (χ.toUnitHom.comp N.unitsEquivUnitsType).restrict_surjective R N.units

Premises used: Submonoid.units, MonoidHom.comp, MulChar.toUnitHom, MonoidHom.restrict_surjective
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
N : Submonoid M
χ : MulChar.{u_1, u_2} (↥N) R
ψ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hψ :
  Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
    ((MonoidHom.restrictHom N.units Rˣ : (a : Mˣ →* Rˣ) → ↥N.units →* Rˣ) ψ : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
    (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ) : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
⊢ ∃ (a : MulChar M R), (restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) a = χ

Tactic:
⟨MulChar.ofUnitHom ψ, ext fun _ ↦ ?_⟩

Premises used: MulChar.ext, Exists.intro, MulChar.ofUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
N : Submonoid M
χ : MulChar.{u_1, u_2} (↥N) R
ψ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hψ :
  Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
    ((MonoidHom.restrictHom N.units Rˣ : (a : Mˣ →* Rˣ) → ↥N.units →* Rˣ) ψ : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
    (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ) : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
refine :
  ∀ (x : (↥N)ˣ),
    Eq.{u_2 + 1} (α := R)
      ((((restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) (ofUnitHom ψ) : MulChar.{u_1, u_2} (↥N) R) :
            (a : ↥N) → R)
          (↑x : ↥N) :
        R)
      ((χ : (a : ↥N) → R) (↑x : ↥N) : R)
⊢ ∃ (a : MulChar M R), (restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) a = χ

Tactic:
refine ⟨MulChar.ofUnitHom ψ, ext fun _ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
N : Submonoid M
χ : MulChar.{u_1, u_2} (↥N) R
ψ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hψ :
  Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
    ((MonoidHom.restrictHom N.units Rˣ : (a : Mˣ →* Rˣ) → ↥N.units →* Rˣ) ψ : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
    (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ) : MonoidHom.{u_1, u_2} (↥N.units) Rˣ)
x : (↥N)ˣ
rw :
  ∀
    (hψ :
      Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ) (ψ.restrict N.units)
        (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ)))
    (x : (↥N)ˣ),
    Eq.{u_2 + 1} (α := R)
      ((((restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) (ofUnitHom ψ) : MulChar.{u_1, u_2} (↥N) R) :
            (a : ↥N) → R)
          (↑x : ↥N) :
        R)
      ((χ : (a : ↥N) → R) (↑x : ↥N) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) (ofUnitHom ψ) : MulChar.{u_1, u_2} (↥N) R) : (a : ↥N) → R)
        (↑x : ↥N) :
      R)
    ((χ : (a : ↥N) → R) (↑x : ↥N) : R)

Tactic:
rw [MonoidHom.restrictHom_apply] at hψ

Premises used: MonoidHom.restrictHom_apply
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
N : Submonoid M
χ : MulChar.{u_1, u_2} (↥N) R
ψ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hψ :
  Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ) (ψ.restrict N.units)
    (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ))
x : (↥N)ˣ
rw :
  Eq.{u_2 + 1} (α := R)
    ((ofUnitHom (MonoidHom.comp (ψ.restrict N.units) (↑N.unitsEquivUnitsType.symm : (↥N)ˣ →* ↥N.units)) : (a : ↥N) → R)
        (↑x : ↥N) :
      R)
    ((χ : (a : ↥N) → R) (↑x : ↥N) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) (ofUnitHom ψ) : MulChar.{u_1, u_2} (↥N) R) : (a : ↥N) → R)
        (↑x : ↥N) :
      R)
    ((χ : (a : ↥N) → R) (↑x : ↥N) : R)

Tactic:
rw [restrictHom_apply, restrict_ofUnitHom]

Premises used: MulChar.restrict_ofUnitHom, MulChar.restrictHom_apply
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
N : Submonoid M
χ : MulChar.{u_1, u_2} (↥N) R
ψ : MonoidHom.{u_1, u_2} Mˣ Rˣ
hψ :
  Eq (α := MonoidHom.{u_1, u_2} (↥N.units) Rˣ) (ψ.restrict N.units)
    (χ.toUnitHom.comp (↑N.unitsEquivUnitsType : ↥N.units →* (↥N)ˣ))
x : (↥N)ˣ
⊢ Eq.{u_2 + 1} (α := R)
    ((ofUnitHom (MonoidHom.comp (ψ.restrict N.units) (↑N.unitsEquivUnitsType.symm : (↥N)ˣ →* ↥N.units)) : (a : ↥N) → R)
        (↑x : ↥N) :
      R)
    ((χ : (a : ↥N) → R) (↑x : ↥N) : R)

Tactic:
simp [hψ]
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
m : Mˣ
χ : MulChar M R
⊢ Eq.{u_2 + 1} (α := R)
    ((((MulEquiv.symm (mulCharEquiv M R) : (a : Mˣ) → MulChar (MulChar M R) R) m : MulChar (MulChar M R) R) :
          (a : MulChar M R) → R)
        χ :
      R)
    (if IsUnit χ then
        (↑((((mulEquivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R)
      else 0 :
      R)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
m : Mˣ
χ : MulChar M R
rw :
  Eq.{u_2 + 1} (α := R)
    (if IsUnit χ then
        (↑((((mulEquivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R)
      else 0 :
      R)
    ((χ : (a : M) → R) (↑m : M) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((↑((((mulEquivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R) :
      R)
    ((χ : (a : M) → R) (↑m : M) : R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((↑((((equivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R) : R)
    ((χ : (a : M) → R) (↑m : M) : R)
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : R) ((χ : (a : M) → R) (↑m : M) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((MulEquiv.symm (mulCharEquiv M R) : (a : Mˣ) → MulChar (MulChar M R) R) m : MulChar (MulChar M R) R) :
          (a : MulChar M R) → R)
        χ :
      R)
    ((χ : (a : M) → R) (↑m : M) : R)

Tactic:
rw [show ((mulCharEquiv M R).symm m) χ =
    if IsUnit χ then ↑(mulEquivToUnitHom χ m) else (0 : R) by rfl, if_pos (Group.isUnit χ),
    mulEquivToUnitHom_apply, coe_equivToUnitHom]

Premises used: MulChar.mulEquivToUnitHom_apply, Group.isUnit, if_pos, MulChar.coe_equivToUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
m : Mˣ
χ : MulChar M R
rw :
  Eq.{u_2 + 1} (α := R)
    (if IsUnit χ then
        (↑((((mulEquivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R)
      else 0 :
      R)
    ((χ : (a : M) → R) (↑m : M) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((↑((((mulEquivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R) :
      R)
    ((χ : (a : M) → R) (↑m : M) : R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((↑((((equivToUnitHom : (a : MulChar M R) → Mˣ →* Rˣ) χ : MonoidHom.{u_1, u_2} Mˣ Rˣ) : (a : Mˣ) → Rˣ) m) : R) : R)
    ((χ : (a : M) → R) (↑m : M) : R)
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : R) ((χ : (a : M) → R) (↑m : M) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((MulEquiv.symm (mulCharEquiv M R) : (a : Mˣ) → MulChar (MulChar M R) R) m : MulChar (MulChar M R) R) :
          (a : MulChar M R) → R)
        χ :
      R)
    ((χ : (a : M) → R) (↑m : M) : R)

Tactic:
classical
  rw [show ((mulCharEquiv M R).symm m) χ =
    if IsUnit χ then ↑(mulEquivToUnitHom χ m) else (0 : R) by rfl, if_pos (Group.isUnit χ),
    mulEquivToUnitHom_apply, coe_equivToUnitHom]

Premises used: MulChar.mulEquivToUnitHom_apply, Group.isUnit, if_pos, MulChar.coe_equivToUnitHom
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
χ : MulChar M R
η : MulChar (MulChar M R) R
rw :
  Eq.{u_2 + 1} (α := R)
    ((((MulEquiv.symm (mulCharEquiv M R) : (a : Mˣ) → MulChar (MulChar M R) R)
              ((mulCharEquiv M R : (a : MulChar (MulChar M R) R) → Mˣ) η) :
            MulChar (MulChar M R) R) :
          (a : MulChar M R) → R)
        χ :
      R)
    ((η : (a : MulChar M R) → R) χ : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) ((η : (a : MulChar M R) → R) χ : R) ((η : (a : MulChar M R) → R) χ : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑((mulCharEquiv M R : (a : MulChar (MulChar M R) R) → Mˣ) η) : M) : R)
    ((η : (a : MulChar M R) → R) χ : R)

Tactic:
rw [← mulCharEquiv_symm_apply_apply (mulCharEquiv M R η) χ, MulEquiv.symm_apply_apply]

Premises used: MulChar.mulCharEquiv, MulChar.mulCharEquiv_symm_apply_apply, DFunLike.coe, MulEquiv.symm_apply_apply
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
H : Subgroup Mˣ
χ : MulChar M R
rw :
  Membership.mem (α := MonoidHom.{u_1, u_2} Mˣ Rˣ) (γ := Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))
      ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
          ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H) :
        Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))
      ((MulEquiv.symm (MulEquiv.symm mulEquivToUnitHom) : (a : MulChar M R) → Mˣ →* Rˣ) χ :
        MonoidHom.{u_1, u_2} Mˣ Rˣ) ↔
    ∀ m ∈ H, Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : R) (1 : R)
⊢ Membership.mem (γ := Subgroup (MulChar M R))
      ((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
          ((subgroupOrderIsoSubgroupMulChar M R : (a : Subgroup Mˣ) → (Subgroup (MulChar M R))ᵒᵈ) H) :
        Subgroup (MulChar M R))
      χ ↔
    ∀ m ∈ H, Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : R) (1 : R)

Tactic:
rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
    MulEquiv.coe_mapSubgroup, OrderDual.ofDual_toDual, Subgroup.mem_map_equiv]

Premises used: OrderIso.dual_apply, Subgroup.mem_map_equiv, OrderIso.trans_apply, MulEquiv.coe_mapSubgroup, MulChar.subgroupOrderIsoSubgroupMulChar, OrderDual.ofDual_toDual
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ Membership.mem (α := MonoidHom.{u_1, u_2} Mˣ Rˣ) (γ := Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))
      ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
          ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H) :
        Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))
      ((MulEquiv.symm (MulEquiv.symm mulEquivToUnitHom) : (a : MulChar M R) → Mˣ →* Rˣ) χ :
        MonoidHom.{u_1, u_2} Mˣ Rˣ) ↔
    ∀ m ∈ H, Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : R) (1 : R)

Tactic:
simp [← Units.val_eq_one]

Premises used: Units.val_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Lemmas
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
g : Rˣ
hg : ∀ (x : Rˣ), Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers g) x
χ₁ χ₂ : MulChar R R'
rw :
  Eq (α := MonoidHom.{u_1, u_3} Rˣ R'ˣ)
      ((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ)
      ((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) ↔
    Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
rw₁ :
  Eq.{u_3 + 1} (α := R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g : R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g :
        R'ˣ) ↔
    Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
rw₂ :
  Eq.{u_3 + 1} (α := R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g : R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g :
        R'ˣ) ↔
    Eq.{u_3 + 1} (α := R')
      ((↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
          R') :
        R')
      ((χ₂ : (a : R) → R') (↑g : R) : R')
rw₃ :
  Eq.{u_3 + 1} (α := R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g : R'ˣ)
      ((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g :
        R'ˣ) ↔
    Eq.{u_3 + 1} (α := R')
      (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
        R')
      (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
        R')
rw₄ rw₅ :
  Eq.{u_3 + 1} (α := R')
      (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
        R')
      (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
        R') ↔
    Eq.{u_3 + 1} (α := R')
      (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₁ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
        R')
      (↑((((equivToUnitHom : (a : MulChar R R') → Rˣ →* R'ˣ) χ₂ : MonoidHom.{u_1, u_3} Rˣ R'ˣ) : (a : Rˣ) → R'ˣ) g) :
        R')
⊢ χ₁ = χ₂ ↔ Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')

Tactic:
rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
    ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]

Premises used: Units.ext_iff, MonoidHom.eq_iff_eq_on_generator, MulChar.equivToUnitHom, Equiv.apply_eq_iff_eq, MulChar.coe_equivToUnitHom