-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
have have₁ have₂ :
  ∀ (this : IsGalois ℚ K),
    Eq (α := Subgroup (ZMod n)ˣ)
      (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
            (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
          (stabilizer Gal(K/ℚ) P) :
        Subgroup (ZMod n)ˣ)
      (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
h :
  ∀ (this : IsGalois ℚ K),
    (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
              (stabilizer Gal(K/ℚ) P) :
            Subgroup (ZMod n)ˣ) :
        Set (ZMod n)ˣ) =
      (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
h₁ :
  ∀ (this : IsGalois ℚ K),
    (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
              (stabilizer Gal(K/ℚ) P) :
            Subgroup (ZMod n)ˣ) :
        Set (ZMod n)ˣ) ⊆
      (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
h₂ h₃ :
  ∀ (this : IsGalois ℚ K),
    Fintype.card (↑(↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ) : Type) ≤
      Fintype.card
        (↑(↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                      (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
                    (stabilizer Gal(K/ℚ) P) :
                  Subgroup (ZMod n)ˣ) :
              Set (ZMod n)ˣ) :
          Type)
⊢ Eq (α := Subgroup (ZMod n)ˣ)
    (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
          (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
        (stabilizer Gal(K/ℚ) P) :
      Subgroup (ZMod n)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)

Tactic:
classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)})
      (by simp [hp.out.ne_zero]), inertiaDegIn_eq_of_not_dvd p K hn,
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime]

Premises used: SetLike.coe_sort_coe, MulEquiv.mapSubgroup_apply, Subgroup.coe_map, Ideal.card_stabilizer_eq, Set.Elem, IsCyclotomicExtension.Rat.galEquivZMod, Nat.card, MulEquiv.toEquiv, Nat.cast, SetLike.ext', Nat.card_zpowers, Set.eq_of_subset_of_card_le, Nat.card_image_equiv, Units.coeHom_apply, Set.image, Ideal.span, ZMod.coe_unitOfCoprime, Singleton.singleton, DFunLike.coe, orderOf_injective, Units.coeHom_injective, one_mul, rfl, Fintype.card_eq_nat_card