-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst_6 : NeZero m
inst_7 : IsGalois.{0, u_1} ℚ ↥F
inst_8 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
simp_rw :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    m ∈ χ.conductorSet
simp_rw₁ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.FactorsThrough m
simp_rw₂ :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
simp_rw₃ :
  (∀ σ ∈ F.fixingSubgroup,
      Eq (α := R)
        ((χ : (a : ZMod n) → R)
            (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
          R)
        (1 : R)) ↔
    (ZMod.unitsMap hdiv).ker ≤ (toUnitHom χ).ker
simp_rw₄ :
  (∀ σ ∈ F.fixingSubgroup,
      Eq (α := R)
        ((χ : (a : ZMod n) → R)
            (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
          R)
        (1 : R)) ↔
    ∀ ⦃x : (ZMod n)ˣ⦄, x ∈ (ZMod.unitsMap hdiv).ker → x ∈ (toUnitHom χ).ker
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.conductor ∣ m
have simp_rw₅ : (∀ σ ∈ F.fixingSubgroup,
    Eq (α := R)
      ((χ : (a : ZMod n) → R)
          (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) :
        R)
      (1 : R)) ↔
  ∀ (a : Gal(K/ℚ)),
    Membership.mem (α := (ZMod n)ˣ) (ZMod.unitsMap hdiv).ker
        (((MulEquiv.toEquiv (galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) :
              (a : Gal(K/ℚ)) → (ZMod n)ˣ)
            a :
          (ZMod n)ˣ) →
      Membership.mem (α := (ZMod n)ˣ) (toUnitHom χ).ker
        (((MulEquiv.toEquiv (galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) :
              (a : Gal(K/ℚ)) → (ZMod n)ˣ)
            a :
          (ZMod n)ˣ)
Tactic: simp_rw [← χ.mem_conductorSet_iff_conductor_dvd hdiv, χ.mem_conductorSet_iff,
    factorsThrough_iff_ker_unitsMap hdiv, mem_intermediateFieldEquivSubgroupChar_iff,
    SetLike.le_def, ← (galEquivZMod n K).forall_congr_right, MonoidHom.mem_ker,
    MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe, ← (galEquivZMod_restrictNormal_apply n K F hdiv _),
    EmbeddingLike.map_eq_one_iff, AlgEquiv.restrictNormal_eq_one_iff,
    IntermediateField.mem_fixingSubgroup_iff, Units.ext_iff, toUnitHom_eq, coe_equivToUnitHom,
    Units.val_one]