awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ_1 : 𝓞 K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
h₀ : Ne (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) 0
h_eq₁ :
  Eq (α := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
    (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔
      span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
⊢ 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))))
have rw : Eq (α := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)} ⊔ span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
  (span {(↑p : 𝓞 K)} ⊔ span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))
Tactic: rw [span_insert]
-- 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 θ
h : Ne (α := Ideal ℤ) (span {(↑p : ℤ)}) ⊥
⊢ Eq.{u_1 + 1} (α := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K))
    {J : Ideal (𝓞 K) |
      Membership.mem (γ := Multiset (Ideal (𝓞 K)))
        (normalizedFactors (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)}))) J}
have h₁ : ∀ (x : Ideal (𝓞 K)),
  Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) x ↔
    Membership.mem (γ := Set (Ideal (𝓞 K)))
      {J : Ideal (𝓞 K) |
        Membership.mem (γ := Multiset (Ideal (𝓞 K)))
          (normalizedFactors (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)}))) J}
      x
Tactic: ext
-- 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 : (ZMod p)[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) Q
⊢ 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}
    (Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm : ZMod p →+* ℤ ⧸ span {(↑p : ℤ)}) Q)
have rw : 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}
  (↑((Equiv.symm (primesOverSpanEquivMonicFactorsModAux (minpoly ℤ θ)) :
          (a : ↥(normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))).toFinset) →
            { Q : (ℤ ⧸ span {(↑p : ℤ)})[X] //
              Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)) })
        (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦
          Membership.mem (γ := Finset (ZMod p)[X])
            (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))) x)
          Q hQ)) :
    (ℤ ⧸ span {(↑p : ℤ)})[X])
Tactic: rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]
-- 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 : (ZMod p)[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) Q
rw :
  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}
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsModAux (minpoly ℤ θ)) :
            (a : ↥(normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))).toFinset) →
              { Q : (ℤ ⧸ span {(↑p : ℤ)})[X] //
                Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)) })
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦
            Membership.mem (γ := Finset (ZMod p)[X])
              (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))) x)
            Q hQ)) :
      (ℤ ⧸ 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}
    (Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm : ZMod p →+* ℤ ⧸ span {(↑p : ℤ)}) Q)
have A : ℤ[X]
Tactic: rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]
-- 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 : (ZMod p)[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) Q
rw :
  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}
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsModAux (minpoly ℤ θ)) :
            (a : ↥(normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))).toFinset) →
              { Q : (ℤ ⧸ span {(↑p : ℤ)})[X] //
                Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)) })
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦
            Membership.mem (γ := Finset (ZMod p)[X])
              (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))) x)
            Q hQ)) :
      (ℤ ⧸ span {(↑p : ℤ)})[X])
A : ℤ[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}
    (Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm : ZMod p →+* ℤ ⧸ span {(↑p : ℤ)}) Q)
have hQ₁ : Membership.mem (γ := Finset (ZMod p)[X])
  (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))) Q
Tactic: rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]
-- 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)
⊢ Eq (α := Ideal (𝓞 K))
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
            (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
      Ideal (𝓞 K))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
have simp : Eq (α := Ideal (𝓞 K))
  (↑(((Equiv.symm (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk sorry sorry sorry sorry) :
            (↑{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) sorry)) :
    Ideal (𝓞 K))
  (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
Tactic: simp only [primesOverSpanEquivMonicFactorsMod_symm_apply, Polynomial.map_map,
    Int.quotientSpanNatEquivZMod_comp_castRingHom]
-- 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)
⊢ 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
    ((↑(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))))
Tactic: rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span,
    span_union, span_eq, map_span, Set.image_singleton, map_natCast, ← span_insert]
-- 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))))
⊢ 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 (↑(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))))
Tactic: rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span,
    span_union, span_eq, map_span, Set.image_singleton, map_natCast, ← span_insert]
-- 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))))
⊢ 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))
  (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))))
Tactic: rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span,
    span_union, span_eq, map_span, Set.image_singleton, map_natCast, ← span_insert]
-- 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)
⊢ LiesOver (A := ℤ) (B := 𝓞 K) (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
    (span {(↑p : ℤ)})
have rw : LiesOver.{0, u_1} (A := ℤ) (B := 𝓞 K)
  (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
          (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
        (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
          (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
    Ideal (𝓞 K))
  (span {(↑p : ℤ)})
Tactic: rw [← Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span hp hQ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (hypothesis)
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)
⊢ inertiaDeg.{0, u_1} (R := ℤ) (S := 𝓞 K) (span {(↑p : ℤ)})
      (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
              (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
            (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
              (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
        Ideal (𝓞 K)) =
    natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
have this : LiesOver (A := ℤ) (B := 𝓞 K) (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
  (span {(↑p : ℤ)})
Tactic: have := liesOver_primesOverSpanEquivMonicFactorsMod_symm hp hQ
-- 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)
this :
  LiesOver (A := ℤ) (B := 𝓞 K) (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
    (span {(↑p : ℤ)})
⊢ inertiaDeg.{0, u_1} (R := ℤ) (S := 𝓞 K) (span {(↑p : ℤ)})
      (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
              (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
            (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
              (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
        Ideal (𝓞 K)) =
    natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
have rw : Module.finrank.{0, u_1} (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
    (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
      (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))) =
  Module.finrank (ZMod p)
    (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
Tactic: rw [primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, inertiaDeg_algebraMap,
    ← finrank_quotient_span_eq_natDegree]