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
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
H : Subgroup Mˣ
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)
⊢ 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.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom)) :
                (Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))ᵒᵈ ≃o (Subgroup (MulChar M R))ᵒᵈ) :
              (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → (Subgroup (MulChar M R))ᵒᵈ)
            ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (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]
-- 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ˣ
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)
rw₁ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            (((OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom)) :
                  (Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))ᵒᵈ ≃o (Subgroup (MulChar M R))ᵒᵈ) :
                (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → (Subgroup (MulChar M R))ᵒᵈ)
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
⊢ 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))
          ((OrderDual.toDual : (a : Subgroup (MulChar M R)) → (Subgroup (MulChar M R))ᵒᵈ)
            ((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) :
                (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
              ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
                ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (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]
-- 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ˣ
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)
rw₁ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            (((OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom)) :
                  (Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))ᵒᵈ ≃o (Subgroup (MulChar M R))ᵒᵈ) :
                (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → (Subgroup (MulChar M R))ᵒᵈ)
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₂ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            ((OrderDual.toDual : (a : Subgroup (MulChar M R)) → (Subgroup (MulChar M R))ᵒᵈ)
              ((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) :
                  (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
                ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
                  ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ)
                    H)))) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
⊢ 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
    ↥((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) : (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
          ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
            ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (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]
-- 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ˣ
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)
rw₁ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            (((OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom)) :
                  (Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))ᵒᵈ ≃o (Subgroup (MulChar M R))ᵒᵈ) :
                (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → (Subgroup (MulChar M R))ᵒᵈ)
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₂ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            ((OrderDual.toDual : (a : Subgroup (MulChar M R)) → (Subgroup (MulChar M R))ᵒᵈ)
              ((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) :
                  (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
                ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
                  ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ)
                    H)))) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₃ :
  Nat.card
      ↥((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) : (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
            ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
⊢ 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 (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
          ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H) :
        Subgroup (MonoidHom.{u_1, u_2} 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]
-- 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ˣ
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)
rw₁ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            (((OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom)) :
                  (Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))ᵒᵈ ≃o (Subgroup (MulChar M R))ᵒᵈ) :
                (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → (Subgroup (MulChar M R))ᵒᵈ)
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₂ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            ((OrderDual.toDual : (a : Subgroup (MulChar M R)) → (Subgroup (MulChar M R))ᵒᵈ)
              ((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) :
                  (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
                ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
                  ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ)
                    H)))) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₃ :
  Nat.card
      ↥((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) : (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
            ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₄ :
  Nat.card
      ↥((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ˣ)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
⊢ 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.{u_1} (Mˣ ⧸ H) = Nat.card.{u_1} (Mˣ ⧸ H)
Tactic: rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
    OrderDual.ofDual_toDual, Subgroup.card_mapSubgroup,
    CommGroup.card_subgroupOrderIsoSubgroupMonoidHom]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
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'
⊢ χ₁ = χ₂ ↔ Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
have 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')
Tactic: rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
    ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
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')
⊢ χ₁ = χ₂ ↔ Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
have 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')
Tactic: rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
    ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
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')
⊢ χ₁ = χ₂ ↔ Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
have 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')
Tactic: rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
    ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
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')
⊢ χ₁ = χ₂ ↔ Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
have 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')
Tactic: rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
    ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
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')
⊢ χ₁ = χ₂ ↔ Eq.{u_3 + 1} (α := R') ((χ₁ : (a : R) → R') (↑g : R) : R') ((χ₂ : (a : R) → R') (↑g : R) : R')
have 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')
Tactic: rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
    ← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_3} Rˣ R'ˣ
S : Submonoid R
⊢ restrict S (ofUnitHom f) =
    ofUnitHom (MonoidHom.comp (f.restrict S.units) (↑S.unitsEquivUnitsType.symm : (↥S)ˣ →* ↥S.units))
have h : ∀ (x : (↥S)ˣ),
  Eq.{u_3 + 1} (α := R') ((restrict S (ofUnitHom f) : (a : ↥S) → R') (↑x : ↥S) : R')
    ((ofUnitHom (MonoidHom.comp (f.restrict S.units) (↑S.unitsEquivUnitsType.symm : (↥S)ˣ →* ↥S.units)) : (a : ↥S) → R')
        (↑x : ↥S) :
      R')
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_3} Rˣ R'ˣ
S : Submonoid R
x : (↥S)ˣ
⊢ Eq.{u_3 + 1} (α := R') ((restrict S (ofUnitHom f) : (a : ↥S) → R') (↑x : ↥S) : R')
    ((ofUnitHom (MonoidHom.comp (f.restrict S.units) (↑S.unitsEquivUnitsType.symm : (↥S)ˣ →* ↥S.units)) : (a : ↥S) → R')
        (↑x : ↥S) :
      R')
have h : Eq (α := R')
  ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R') (↑(↑x : ↥S) : R) :
    R')
  ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
Tactic: simp only [ofUnitHom_eq, restrict_apply, Units.isUnit, reduceIte, equivToUnitHom_symm_coe,
    MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, MonoidHom.restrict_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Lemmas (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_3
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_3} Rˣ R'ˣ
S : Submonoid R
x : (↥S)ˣ
⊢ Eq (α := R')
    ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R') (↑(↑x : ↥S) : R) :
      R')
    ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
have h : Eq (α := R')
  ((((Equiv.symm equivToUnitHom : (a : Rˣ →* R'ˣ) → MulChar R R') f : MulChar R R') : (a : R) → R')
      (↑(↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ) : R) :
    R')
  ((↑((f : (a : Rˣ) → R'ˣ) (↑((S.unitsEquivUnitsType.symm : (a : (↥S)ˣ) → ↥S.units) x) : Rˣ)) : R') : R')
Tactic: rw [← Submonoid.val_unitsEquivUnitsType_symm_apply_coe S x, equivToUnitHom_symm_coe]