-- 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
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)ˣ)
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/ℚ)),
      Eq (α := (ZMod m)ˣ)
          ((ZMod.unitsMap hdiv : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
              (((MulEquiv.toEquiv (galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) :
                  (a : Gal(K/ℚ)) → (ZMod n)ˣ)
                a) :
            (ZMod m)ˣ)
          (1 : (ZMod m)ˣ) →
        Eq (α := Rˣ)
          ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ)
              (((MulEquiv.toEquiv (galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) :
                    (a : Gal(K/ℚ)) → (ZMod n)ˣ)
                  a :
                (ZMod n)ˣ) :
            Rˣ)
          (1 : Rˣ)
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/ℚ)),
      Eq (α := (ZMod m)ˣ)
          ((ZMod.unitsMap hdiv : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
              (((↑(galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a) :
            (ZMod m)ˣ)
          (1 : (ZMod m)ˣ) →
        Eq (α := Rˣ)
          ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ)
              (((↑(galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : Gal(K/ℚ) ≃ (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a :
                (ZMod n)ˣ) :
            Rˣ)
          (1 : Rˣ)
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/ℚ)),
      Eq (α := (ZMod m)ˣ)
          ((ZMod.unitsMap hdiv : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
              (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a) :
            (ZMod m)ˣ)
          (1 : (ZMod m)ˣ) →
        Eq (α := Rˣ)
          ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ)
              (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a : (ZMod n)ˣ) :
            Rˣ)
          (1 : Rˣ)
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/ℚ)),
      Eq (α := (ZMod m)ˣ)
          (((galEquivZMod m ↥F : Gal(↥F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(↥F/ℚ)) → (ZMod m)ˣ) (a.restrictNormal ↥F) :
            (ZMod m)ˣ)
          (1 : (ZMod m)ˣ) →
        Eq (α := Rˣ)
          ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ)
              (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a : (ZMod n)ˣ) :
            Rˣ)
          (1 : Rˣ)
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/ℚ)),
      Eq (α := Gal(↥F/ℚ)) (a.restrictNormal ↥F) 1 →
        Eq (α := Rˣ)
          ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ)
              (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a : (ZMod n)ˣ) :
            Rˣ)
          (1 : Rˣ)
⊢ 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/ℚ)),
    (∀ x ∈ F, (a : (a : K) → K) x = x) →
      Eq (α := Rˣ)
        ((toUnitHom χ : (a : (ZMod n)ˣ) → Rˣ)
            (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) a : (ZMod n)ˣ) :
          Rˣ)
        (1 : Rˣ)
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]