awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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ˣ)
⊢ Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
have 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)
Tactic: rwa [Units.ext_iff, coe_toUnitHom] at hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
have 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)
Tactic: rwa [Units.ext_iff, coe_toUnitHom] at hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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ˣ)
⊢ Ne.{u_2 + 1} (α := R) ((ofUnitHom φ : (a : M) → R) (↑a : M) : R) (1 : R)
have 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ˣ)
Tactic: contrapose hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)
have pos : ∀ (hu : IsUnit a), ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)
Tactic: by_cases hu : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)
have neg : ∀ (hu : ¬IsUnit a), ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) a : R) (1 : R)
Tactic: by_cases hu : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
have pos : ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) hu.unit : Rˣ) (1 : Rˣ)
Tactic: refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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ˣ)
have pos : hu.unit ≠ 1
Tactic: refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ hu.unit ≠ 1
have pos : ∀ (ha : hu.unit = 1), a = 1
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ a = 1
have pos : (↑hu.unit : M) = 1
Tactic: rw [← hu.unit_spec, ha, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ a = 1
have pos₁ : Eq.{u_1 + 1} (α := M) (↑1 : M) 1
Tactic: rw [← hu.unit_spec, ha, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ a = 1
have pos₂ : Eq.{u_1 + 1} (α := Mˣ) 1 1
Tactic: rw [← hu.unit_spec, ha, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ ∃ (a : MulChar M R), (restrictHom N R : (a : MulChar M R) → MulChar (↥N) R) a = χ
have 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 = χ
Tactic: obtain ⟨ψ, hψ⟩ := (χ.toUnitHom.comp N.unitsEquivUnitsType).restrict_surjective R N.units
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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 = χ
have 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)
Tactic: refine ⟨MulChar.ofUnitHom ψ, ext fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)ˣ
⊢ 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)
have 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)
Tactic: rw [MonoidHom.restrictHom_apply] at hψ
Cleared hypotheses: hψ, x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
    ((((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)
have 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)
Tactic: rw [restrictHom_apply, restrict_ofUnitHom]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
    ((χ : (a : M) → R) (↑m : M) : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have rw₃ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
    ((χ : (a : M) → R) (↑m : M) : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have rw₃ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑m : M) : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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
⊢ 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)
have 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)
Tactic: rw [← mulCharEquiv_symm_apply_apply (mulCharEquiv M R η) χ, MulEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_2 + 1} (α := R) ((η : (a : MulChar M R) → R) χ : R) ((η : (a : MulChar M R) → R) χ : R)
Tactic: rw [← mulCharEquiv_symm_apply_apply (mulCharEquiv M R η) χ, MulEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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 (γ := 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)
have 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)
Tactic: rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
    MulEquiv.coe_mapSubgroup, OrderDual.ofDual_toDual, Subgroup.mem_map_equiv]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
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ˣ
⊢ Nat.card
      ↥((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)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
have rw : Nat.card
    ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
          ((OrderIso.trans (CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R)
                (OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom))) :
              (a : Subgroup Mˣ) → (Subgroup (MulChar M R))ᵒᵈ)
            H) :
        Subgroup (MulChar M R)) =
  Nat.card.{u_1} (Mˣ ⧸ H)
Tactic: rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
    OrderDual.ofDual_toDual, Subgroup.card_mapSubgroup,
    CommGroup.card_subgroupOrderIsoSubgroupMonoidHom]