awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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
⊢ Eq.{u_1 + 1} (α := 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) Q
            hQ)) :
      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 (↑(Int.quotientSpanNatEquivZMod p).symm : ZMod p →+* ℤ ⧸ span {(↑p : ℤ)}) Q) ⋯)) :
      Ideal (𝓞 K))

Tactic:
rfl

Premises used: Set.Mem, setOf, Ideal.comap, Polynomial.map, rfl
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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)
simp :
  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))))
⊢ 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))))

Tactic:
simp only [primesOverSpanEquivMonicFactorsMod_symm_apply, Polynomial.map_map,
    Int.quotientSpanNatEquivZMod_comp_castRingHom]

Premises used: Polynomial.map_map, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Int.quotientSpanNatEquivZMod_comp_castRingHom
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 :
  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 : ℤ)})
⊢ LiesOver (A := ℤ) (B := 𝓞 K) (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
    (span {(↑p : ℤ)})

Tactic:
rw [← Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span hp hQ]

Premises used: NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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.{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:
((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).prop.2

Premises used: NumberField.Ideal.primesOverSpanEquivMonicFactorsMod, Subtype.mk, And.right, Subtype.prop, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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.{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:
exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).prop.2

Premises used: NumberField.Ideal.primesOverSpanEquivMonicFactorsMod, Subtype.mk, And.right, Subtype.prop, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 : ℤ)})

Tactic:
have := liesOver_primesOverSpanEquivMonicFactorsMod_symm hp hQ
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 : ℤ)})
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}))
⊢ 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)

Tactic:
rw [primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, inertiaDeg_algebraMap,
    ← finrank_quotient_span_eq_natDegree]

Premises used: Ideal.inertiaDeg_algebraMap, finrank_quotient_span_eq_natDegree, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 : ℤ)})
h :
  ∀ (x : ℤ),
    Eq (α :=
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
      ((RingHom.comp
              (RingHom.comp
                (algebraMap (ZMod p)
                  (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
                    (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})))
                (Int.quotientSpanNatEquivZMod p).toRingHom)
              (Ideal.Quotient.mk (span {(↑p : ℤ)})) :
            (a : ℤ) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
          x :
        HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
      ((RingHom.comp (β := HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
              ((ZModXQuotSpanEquivQuotSpanPair hp hQ).symm.toRingHom.comp
                (algebraMap (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
                  (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
                    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))))))
              (Ideal.Quotient.mk (span {(↑p : ℤ)})) :
            (a : ℤ) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
          x :
        HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
⊢ RingHom.comp
      (algebraMap (ZMod p)
        (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
          (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})))
      (Int.quotientSpanNatEquivZMod p).toRingHom =
    (ZModXQuotSpanEquivQuotSpanPair hp hQ).symm.toRingHom.comp
      (algebraMap (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
        (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
          (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 : ℤ)})
x : ℤ
⊢ Eq (α :=
    HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
    ((RingHom.comp
            (RingHom.comp
              (algebraMap (ZMod p)
                (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
                  (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})))
              (Int.quotientSpanNatEquivZMod p).toRingHom)
            (Ideal.Quotient.mk (span {(↑p : ℤ)})) :
          (a : ℤ) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
        x :
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
    ((RingHom.comp (β := HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
            ((ZModXQuotSpanEquivQuotSpanPair hp hQ).symm.toRingHom.comp
              (algebraMap (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
                (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
                  (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))))))
            (Ideal.Quotient.mk (span {(↑p : ℤ)})) :
          (a : ℤ) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
        x :
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 : ℤ)})
refine :
  HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
      (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))) ≃+*
    HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
⊢ 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:
refine Algebra.finrank_eq_of_equiv_equiv (Int.quotientSpanNatEquivZMod p) ?_ (by ext; simp)

Premises used: Algebra.finrank_eq_of_equiv_equiv, Int.quotientSpanNatEquivZMod
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 : ℤ)})
⊢ HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
      (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))) ≃+*
    HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})

Tactic:
exact (ZModXQuotSpanEquivQuotSpanPair hp hQ).symm

Premises used: RingOfIntegers.ZModXQuotSpanEquivQuotSpanPair, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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
obtain :
  ∀ (S : ℤ[X])
    (hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) S)),
    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)) S) hQ)) :
          Ideal (𝓞 K)) =
      natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
⊢ 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)
              Q hQ)) :
        Ideal (𝓞 K)) =
    Q.natDegree

Tactic:
obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q

Premises used: Polynomial.map_surjective, ZMod, ZMod.ringHom_surjective, Int.castRingHom, rfl
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
S : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
rw rw₁ :
  natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S) =
    natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
⊢ 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)) S) hQ)) :
        Ideal (𝓞 K)) =
    natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S)

Tactic:
rw [inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply]

Premises used: NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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)
⊢ Ne (α := Ideal ℤ) (span {(↑p : ℤ)}) ⊥

Tactic:
simp [NeZero.ne p]

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 :
  multiplicity.{u_1} (α := 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))
      (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
⊢ ramificationIdx.{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)) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
rw [ramificationIdx_eq_multiplicity (map_ne_bot_of_ne_bot (by simp [NeZero.ne p])) inferInstance]

Premises used: inferInstance, Ideal.map_ne_bot_of_ne_bot, Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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)
h :
  emultiplicity.{u_1} (α := 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))
      (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
    emultiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
⊢ multiplicity.{u_1} (α := 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))
      (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
apply multiplicity_eq_of_emultiplicity_eq

Premises used: multiplicity_eq_of_emultiplicity_eq