-- 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
rw :
  Nat.card.{u_2}
      ↥(((OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                  (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n)))) :
                OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))) :
              (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₁ :
  Nat.card.{u_2}
      ↥((OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))) :
              (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → Subgroup (DirichletCharacter R n))
            (((OrderIso.dual (subgroupGalEquivSubgroupChar n K R) :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) :
                (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
              ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F)) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₂ :
  Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            ((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              (((OrderIso.dual (subgroupGalEquivSubgroupChar n K R) :
                    OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) :
                  (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
                ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F))) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₃ :
  Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            ((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              (((OrderIso.dual (subgroupGalEquivSubgroupChar n K R) :
                    OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) :
                  (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
                ((OrderDual.toDual : (a : Subgroup Gal(K/ℚ)) → (Subgroup Gal(K/ℚ))ᵒᵈ) F.fixingSubgroup))) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₄ :
  Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            ((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              ((OrderDual.toDual :
                  (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
                (((subgroupGalEquivSubgroupChar n K R :
                      OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ)) (Subgroup (DirichletCharacter R n))ᵒᵈ) :
                    (a : Subgroup Gal(K/ℚ)) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
                  ((OrderDual.ofDual : (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → Subgroup Gal(K/ℚ))
                    ((OrderDual.toDual : (a : Subgroup Gal(K/ℚ)) → (Subgroup Gal(K/ℚ))ᵒᵈ) F.fixingSubgroup))))) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₅ :
  Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            (((subgroupGalEquivSubgroupChar n K R :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ)) (Subgroup (DirichletCharacter R n))ᵒᵈ) :
                (a : Subgroup Gal(K/ℚ)) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              ((OrderDual.ofDual : (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → Subgroup Gal(K/ℚ))
                ((OrderDual.toDual : (a : Subgroup Gal(K/ℚ)) → (Subgroup Gal(K/ℚ))ᵒᵈ) F.fixingSubgroup))) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₆ :
  Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            (((subgroupGalEquivSubgroupChar n K R :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ)) (Subgroup (DirichletCharacter R n))ᵒᵈ) :
                (a : Subgroup Gal(K/ℚ)) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              F.fixingSubgroup) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₇ : Nat.card.{u_1} (Gal(K/ℚ) ⧸ F.fixingSubgroup) = Module.finrank.{0, u_1} ℚ ↥F
⊢ Nat.card.{u_2}
      ↥(((OrderIso.trans IsGalois.intermediateFieldEquivSubgroup
                  (OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                    (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))))) :
                OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
              (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
            F :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
have rw₈ : Nat.card.{u_1} (Gal(K/ℚ) ⧸ F.fixingSubgroup) = F.fixingSubgroup.index
Tactic: rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
    ← Subgroup.index_eq_card]