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)
rw : IsCoatom (α := Ideal ℤ) (span {(↑p : ℤ)})
⊢ ¬p ∣ exponent θ ↔
    Codisjoint (α := Ideal ℤ) (comap (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (conductor ℤ θ)) (span {(↑p : ℤ)})

Tactic:
rw [codisjoint_comm, ← IsCoatom.not_le_iff_codisjoint, ← under_def, ← Ideal.dvd_iff_le,
    ← Int.ideal_span_absNorm_eq_self (under ℤ (conductor ℤ θ)),
    Ideal.span_singleton_dvd_span_singleton_iff_dvd, Int.natCast_dvd_natCast, exponent]

Premises used: Ideal.dvd_iff_le, Ideal.span_singleton_dvd_span_singleton_iff_dvd, codisjoint_comm, Int, Ideal.under_def, RingOfIntegers.exponent, conductor, Int.ideal_span_absNorm_eq_self, Int.natCast_dvd_natCast, IsCoatom.not_le_iff_codisjoint, Ideal.under
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
⊢ IsCoatom (α := Ideal ℤ) (span {(↑p : ℤ)})

Tactic:
isMaximal_def.mp <| Int.ideal_span_isMaximal_of_prime p

Premises used: Int.ideal_span_isMaximal_of_prime, Iff.mp, Ideal.isMaximal_def
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
⊢ IsCoatom (α := Ideal ℤ) (span {(↑p : ℤ)})

Tactic:
exact isMaximal_def.mp <| Int.ideal_span_isMaximal_of_prime p

Premises used: Int.ideal_span_isMaximal_of_prime, Iff.mp, Ideal.isMaximal_def
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
rw :
  Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ (conductor ℤ θ)) : ℕ)
    (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)} : ℕ)
rw₁ rw₂ :
  Eq (α := ℕ) (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)})
    (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)})
⊢ exponent θ = sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)}

Tactic:
rw [exponent, Int.absNorm_under_eq_sInf]

Premises used: RingOfIntegers.exponent, Int.absNorm_under_eq_sInf
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 θ
⊢ Eq (α := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)})
    (Ideal.map (R := (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X]) (F :=
      (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] →+* (ZMod p)[X])
      (↑(mapEquiv (Int.quotientSpanNatEquivZMod p)) : (ℤ ⧸ span {(↑p : ℤ)})[X] →+* (ZMod p)[X])
      (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}))

Tactic:
simp [Ideal.map_span, Polynomial.map_map]

Premises used: Ideal.map_span, Polynomial.map_map
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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 θ
⊢ Eq (α := Ideal (𝓞 K)) (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) (span {(↑p : 𝓞 K)})

Tactic:
simp [map_span]

Premises used: Ideal.map_span
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
simp :
  Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((quotientEquivAlgOfEq ℤ ⋯ :
          (a : 𝓞 K ⧸ Ideal.map (Int.castRingHom (𝓞 K)) (span {(↑p : ℤ)})) → 𝓞 K ⧸ span {(↑p : 𝓞 K)})
        (((quotMapEquivQuotQuotMap ⋯ ⋯).symm :
            (a : (ℤ ⧸ span {(↑p : ℤ)})[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}) →
              𝓞 K ⧸ Ideal.map (Int.castRingHom (𝓞 K)) (span {(↑p : ℤ)}))
          ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}) :
                (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) →
                  (ℤ ⧸ span {(↑p : ℤ)})[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)})
              (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) Q) :
            HasQuotient.Quotient (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] (B :=
              Ideal (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
              (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}))) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((Ideal.Quotient.mk (span {(↑p : 𝓞 K)}) : (a : 𝓞 K) → 𝓞 K ⧸ span {(↑p : 𝓞 K)}) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
⊢ Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((ZModXQuotSpanEquivQuotSpan hp :
          (a : (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}) → 𝓞 K ⧸ span {(↑p : 𝓞 K)})
        ((Ideal.Quotient.mk (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}) :
              (a : (ZMod p)[X]) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)})
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) :
          HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
            (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)})) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((Ideal.Quotient.mk (span {(↑p : 𝓞 K)}) : (a : 𝓞 K) → 𝓞 K ⧸ span {(↑p : 𝓞 K)}) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))

Tactic:
simp only [ZModXQuotSpanEquivQuotSpan, algebraMap_int_eq,
    RingEquiv.trans_apply, AlgEquiv.coe_ringEquiv, quotientEquivAlgOfEq_mk,
    quotientEquiv_symm_apply, quotientMap_mk, RingHom.coe_coe, mapEquiv_symm_apply,
    Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom]

Premises used: Ideal.quotientEquiv_symm_apply, RingOfIntegers.ZModXQuotSpanEquivQuotSpan, Polynomial.mapEquiv_symm_apply, RingHom.coe_coe, Ideal.quotientMap_mk, RingEquiv.trans_apply, AlgEquiv.coe_ringEquiv, Ideal.quotientEquivAlgOfEq_mk, algebraMap_int_eq, Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
⊢ Eq (α := Ideal (𝓞 K)) (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) (span {(↑p : 𝓞 K)})

Tactic:
simp [map_span]

Premises used: Ideal.map_span
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
⊢ Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((quotientEquivAlgOfEq ℤ ⋯ :
          (a : 𝓞 K ⧸ Ideal.map (Int.castRingHom (𝓞 K)) (span {(↑p : ℤ)})) → 𝓞 K ⧸ span {(↑p : 𝓞 K)})
        (((quotMapEquivQuotQuotMap ⋯ ⋯).symm :
            (a : (ℤ ⧸ span {(↑p : ℤ)})[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}) →
              𝓞 K ⧸ Ideal.map (Int.castRingHom (𝓞 K)) (span {(↑p : ℤ)}))
          ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}) :
                (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) →
                  (ℤ ⧸ span {(↑p : ℤ)})[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)})
              (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) Q) :
            HasQuotient.Quotient (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] (B :=
              Ideal (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
              (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}))) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((Ideal.Quotient.mk (span {(↑p : 𝓞 K)}) : (a : 𝓞 K) → 𝓞 K ⧸ span {(↑p : 𝓞 K)}) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))

Tactic:
exact congr_arg (quotientEquivAlgOfEq ℤ (by simp [map_span])) <|
    quotMapEquivQuotQuotMap_symm_apply (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral Q

Premises used: Ideal.quotientEquivAlgOfEq, RingOfIntegers.not_dvd_exponent_iff, Int, congr_arg, Iff.mp, NumberField.RingOfIntegers.isIntegral, DFunLike.coe, Codisjoint.eq_top, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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
rw :
  Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
⊢ 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})

Tactic:
rw [← span_insert, span_pair_comm, span_pair_eq_span_left_iff_dvd.mpr]

Premises used: Iff.mpr, Ideal.span_pair_comm, Ideal.span_pair_eq_span_left_iff_dvd, Ideal.span_insert
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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
⊢ Membership.mem (γ := Multiset (ZMod p)[X])
    (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))
    (Polynomial.map (Int.castRingHom (ZMod p)) Q)

Tactic:
simp only [Multiset.mem_toFinset] at hQ

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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]
h₀ : Ne (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) 0
hQ :
  Membership.mem (γ := Multiset (ZMod p)[X])
    (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))
    (Polynomial.map (Int.castRingHom (ZMod p)) Q)
⊢ Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
((Polynomial.mem_normalizedFactors_iff h₀).mp hQ).2.2

Premises used: And.right, Polynomial.mem_normalizedFactors_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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]
h₀ : Ne (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) 0
hQ :
  Membership.mem (γ := Multiset (ZMod p)[X])
    (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))
    (Polynomial.map (Int.castRingHom (ZMod p)) Q)
⊢ Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
exact ((Polynomial.mem_normalizedFactors_iff h₀).mp hQ).2.2

Premises used: And.right, Polynomial.mem_normalizedFactors_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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})
rw 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)))
⊢ 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 [span_insert]

Premises used: Ideal.span_insert
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
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})
h_eq₂ :
  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))))
⊢ Eq (α := Ideal (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)})))
    (Ideal.map (R := 𝓞 K) (F := 𝓞 K →+* HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
      (Ideal.Quotient.mk (span {(↑p : 𝓞 K)})) (span (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
    (Ideal.map (R :=
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
        (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
      (F :=
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
          (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}) →+*
        HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
      (↑(ZModXQuotSpanEquivQuotSpan hp) :
        (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} →+* 𝓞 K ⧸ span {(↑p : 𝓞 K)})
      (Ideal.map (R := (ZMod p)[X]) (F :=
        (ZMod p)[X] →+*
          HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
            (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (Ideal.Quotient.mk (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})))

Tactic:
simp [map_span, ZModXQuotSpanEquivQuotSpan_mk_apply]

Premises used: Ideal.map_span, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
A : ℤ[X]
⊢ ∀ (x : (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X]),
    Eq (α := (ZMod p)[X])
      ((normalize : (a : (ZMod p)[X]) → (ZMod p)[X])
          (((mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv : (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) → (ZMod p)[X]) x) :
        (ZMod p)[X])
      (((mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv : (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) → (ZMod p)[X])
          ((normalize : (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) → (ℤ ⧸ span {(↑p : ℤ)})[X]) x) :
        (ZMod p)[X])

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
A : ℤ[X]
x : (ZMod p)[X]
⊢ Membership.mem (γ := Multiset (ZMod p)[X])
      (normalizedFactors
          (((mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv : (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) → (ZMod p)[X])
            (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) A)) :
        Multiset (ZMod p)[X])
      x ↔
    Membership.mem (γ := Finset (ZMod p)[X])
      (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A))) x

Tactic:
simp [Polynomial.map_map]

Premises used: Polynomial.map_map
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
A : ℤ[X]
Q : (ZMod p)[X]
hQ :
  Membership.mem (γ := Finset (ZMod p)[X])
    (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A))) Q
⊢ Eq (α := (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsModAux A) :
            (a : ↥(normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A)).toFinset) →
              { Q : (ℤ ⧸ span {(↑p : ℤ)})[X] //
                Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) A) })
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦
            Membership.mem (γ := Finset (ZMod p)[X])
              (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A))) x)
            Q hQ)) :
      (ℤ ⧸ span {(↑p : ℤ)})[X])
    (Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm : ZMod p →+* ℤ ⧸ span {(↑p : ℤ)}) Q)

Tactic:
rfl

Premises used: 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 θ
⊢ 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 θ
h : Ne (α := Ideal ℤ) (span {(↑p : ℤ)}) ⊥
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
⊢ 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}

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 θ
h : Ne (α := Ideal ℤ) (span {(↑p : ℤ)}) ⊥
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:
simp [mem_primesOver_iff_mem_normalizedFactors _ h]

Premises used: Ideal.mem_primesOver_iff_mem_normalizedFactors
-- 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
⊢ 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 : (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]
hQ₁ :
  Membership.mem (γ := Finset (ZMod p)[X])
    (Multiset.toFinset (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))) 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)

Tactic:
rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]

Premises used: _private.0.NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux_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 : (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}
    (↑((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:
((primesOverSpanEquivMonicFactorsModAux _).symm ⟨Q, hQ⟩).prop

Premises used: Set.Mem, _private.0.NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux, setOf, Subtype.mk, Multiset.Mem, Subtype.prop, Equiv.symm, DFunLike.coe