-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
rw :
  Eq (α := Ideal (𝓞 K))
    (span
      ((↑(Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) : Set (𝓞 K)) ∪
        singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
rw₁ :
  Eq (α := Ideal (𝓞 K))
    (span (↑(Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) : Set (𝓞 K)) ⊔
      span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
rw₂ :
  Eq (α := Ideal (𝓞 K))
    (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)}) ⊔
      span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
rw₃ :
  Eq (α := Ideal (𝓞 K))
    (span (Set.image (α := ℤ) (⇑(algebraMap ℤ (𝓞 K)) : (a : ℤ) → 𝓞 K) {(↑p : ℤ)}) ⊔
      span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
rw₄ :
  Eq (α := Ideal (𝓞 K))
    (span (singleton (α := 𝓞 K) ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) (↑p : ℤ) : 𝓞 K)) ⊔
      span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
⊢ Eq (α := Ideal (𝓞 K))
    (↑(((Equiv.symm (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk ⋯ ⋯ ⋯ ⋯) :
              (↑{d : (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] |
                      Membership.mem (γ := Multiset (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
                        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ))) d} :
                  Type) ≃
                (↑{J : Ideal (𝓞 K) |
                      Membership.mem (γ := Multiset (Ideal (𝓞 K)))
                        (normalizedFactors (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})))
                        J} :
                  Type u_1)) :
            (a :
                (↑{d : (ℤ ⧸ span {(↑p : ℤ)})[X] |
                      d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ))} :
                  Type)) →
              (↑{J : Ideal (𝓞 K) | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)}))} :
                Type u_1))
          (Subtype.mk (p := fun (x : (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X]) ↦
            Membership.mem (γ := Set (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
              {d : (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] |
                Membership.mem (γ := Multiset (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
                  (normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ))) d}
              x)
            (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) Q) ⋯)) :
      Ideal (𝓞 K))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
have rw₅ : Eq (α := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)} ⊔ span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
  (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
Tactic: rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span,
    span_union, span_eq, map_span, Set.image_singleton, map_natCast, ← span_insert]