-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
h_main : Module.finrank.{0, u_1} ℚ ↥Fₘ * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K
rwa :
  ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K),
    Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
rwa₁ :
  ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Nat.card.{u_1} Gal(↥Fₚ/ℚ) = Module.finrank ℚ K),
    Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
rwa₂ :
  ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Nat.card.{u_1} Gal(↥Fₚ/ℚ) = Nat.card.{u_1} Gal(K/ℚ)),
    Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
have rwa₃ : ∀
  (h_main :
    Set.ncard.{u_1} (α := Ideal (𝓞 ↥Fₘ)) (primesOver (A := ℤ) 𝒑 (𝓞 ↥Fₘ)) *
          (ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 ↥Fₘ) * inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 ↥Fₘ)) *
        Nat.card.{u_1} Gal(↥Fₚ/ℚ) =
      Nat.card.{u_1} Gal(K/ℚ)),
  Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
Tactic: rwa [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank,
    ← IsGalois.card_aut_eq_finrank,
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₘ) Gal(Fₘ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₚ) Gal(Fₚ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 K) Gal(K/ℚ),
    ← ncard_primesOver_mul_ncard_primesOver Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ) hp',
    ramificationIdxIn_eq_of_not_dvd p Fₘ hm, inertiaDegIn_eq_of_prime_pow p k Fₚ,
    ncard_primesOver_of_prime_pow p k Fₚ, one_mul, one_mul, mul_one, mul_assoc, mul_assoc,
    mul_right_inj' (IsDedekindDomain.primesOver_ncard_ne_zero 𝒑 _), ← mul_assoc,
    ← mul_rotate (𝒑.inertiaDegIn (𝓞 K)),
    ← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ), mul_assoc, mul_assoc,
    mul_right_inj' (inertiaDegIn_ne_zero Gal(Fₘ/ℚ)), ← mul_rotate',
    ← ramificationIdxIn_mul_ramificationIdxIn' (p := 𝒑) Pₚ Gal(Fₚ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₚ),
    eq_comm, mul_assoc, mul_eq_left₀ (ramificationIdxIn_ne_zero Gal(Fₚ/ℚ) hp'), ← mul_assoc]
    at h_main
Cleared hypotheses: h_main