awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ (a_1 : S ⧸ P),
    Eq (α :=
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
      ((p.quotientToQuotientRangePowQuotSucc P a_mem :
            (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
          a_1 :
        HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i)))
      (Quot.mk
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z)) hx_1) :
        Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))

Tactic:
⟨Submodule.Quotient.mk y, ?_⟩

Premises used: Submodule.Quotient.mk, Exists.intro
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
simp :
  ∃ (y_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
    (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            y_1) :
        S ⧸ P ^ e) =
      HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
        (Submodule.Quotient.mk (a * y + z))
⊢ Eq (α :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    ((p.quotientToQuotientRangePowQuotSucc P a_mem :
          (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
        (Submodule.Quotient.mk y) :
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
    (Quot.mk
        (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
          ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
        (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
          (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z)) hx_1) :
      Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
          ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
      Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff,
      Submodule.coe_sub]

Premises used: Submodule.Quotient.eq, Ideal.quotientToQuotientRangePowQuotSucc_mk, Subtype.ext_iff, Submodule.coe_sub, LinearMap.mem_range, Submodule.Quotient.quot_mk_eq_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ (y_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
    (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            y_1) :
        S ⧸ P ^ e) =
      HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
        (Submodule.Quotient.mk (a * y + z))

Tactic:
⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩

Premises used: Ideal.mem_map_of_mem, Submodule.neg_mem, Subtype.mk, Exists.intro
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
refine :
  (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) ⋯)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
⊢ ∃ (y_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
    (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            y_1) :
        S ⧸ P ^ e) =
      HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
        (Submodule.Quotient.mk (a * y + z))

Tactic:
refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
mk : x ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ (a_1 : S ⧸ P),
    Eq (α :=
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
      ((p.quotientToQuotientRangePowQuotSucc P a_mem :
            (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
          a_1 :
        HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i)))
      (Quot.mk
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x) hx_1) :
        Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))

Tactic:
suffices hx' : x ∈ Ideal.span {a} ⊔ P ^ (i + 1) by
    obtain ⟨y', hy', z, hz, rfl⟩ := Submodule.mem_sup.mp hx'
    obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hy'
    refine ⟨Submodule.Quotient.mk y, ?_⟩
    simp only [Submodule.Quotient.quot_mk_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
      Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff,
      Submodule.coe_sub]
    refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩
    rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add,
      sub_add_cancel_left, map_neg]
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
mk : x ∈ P ^ min (Multiset.count P (normalizedFactors (span {a}))) (i + 1)
rw : Ne (α := Ideal S) (span {a}) ⊥
⊢ x ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
rw [sup_eq_prod_inf_factors _ (pow_ne_zero _ hP0), normalizedFactors_pow,
    normalizedFactors_irreducible ((Ideal.prime_iff_isPrime hP0).mpr hP).irreducible, normalize_eq,
    Multiset.nsmul_singleton, Multiset.inter_replicate, Multiset.prod_replicate]

Premises used: Prime.irreducible, Iff.mpr, Multiset.prod_replicate, Ideal.sup_eq_prod_inf_factors, pow_ne_zero, Ideal.prime_iff_isPrime, UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton, Multiset.inter_replicate, normalize_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
mk :
  ∀ (a_mem : span {a} ≤ P ^ i) (a_notMem : ¬span {a} ≤ P ^ (i + 1))
    (b :
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
    (val : S ⧸ P ^ e) (x : S)
    (hx :
      Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
        (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x))
    (hx : x ∈ P ^ i) (Pe_le_Pi : P ^ e ≤ P ^ i), x ∈ P ^ min (Multiset.count P (normalizedFactors (span {a}))) (i + 1)
⊢ x ∈ P ^ min (Multiset.count P (normalizedFactors (span {a}))) (i + 1)

Tactic:
rw [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq] at a_mem a_notMem

Premises used: Ideal.submodule_span_eq, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_notMem : ¬span {a} ≤ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
mk : x ∈ P ^ min i (i + 1)
mk₁ mk₂ mk₃ mk₄ : x ∈ P ^ i
⊢ x ∈ P ^ min (Multiset.count P (normalizedFactors (span {a}))) (i + 1)

Tactic:
rwa [Ideal.count_normalizedFactors_eq a_mem a_notMem, min_eq_left i.le_succ]

Premises used: Ideal.count_normalizedFactors_eq, Nat.le_succ, min_eq_left
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
ha : Eq (α := Ideal S) (span {a}) ⊥
rw :
  ∀ (a_notMem : 0 ∉ P ^ (i + 1))
    (b :
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
    (val : S ⧸ P ^ e) (x : S)
    (hx :
      Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
        (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x))
    (hx : x ∈ P ^ i) (Pe_le_Pi : P ^ e ≤ P ^ i) (ha : Eq (α := Ideal S) (span {a}) ⊥), False
⊢ False

Tactic:
rw [Ideal.span_singleton_eq_bot.mp ha] at a_notMem

Premises used: Ideal.span_singleton_eq_bot, Iff.mp
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : 0 ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
ha : Eq (α := Ideal S) (span {a}) ⊥
⊢ 0 ∈ P ^ (i + 1)

Tactic:
have := (P ^ (i + 1)).zero_mem
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : 0 ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this_1 : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
ha : Eq (α := Ideal S) (span {a}) ⊥
this : 0 ∈ P ^ (i + 1)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
choose :
  (a : S) →
    (a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a) →
      (a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ) →
        HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
            Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
            (LinearMap.range (p.powQuotSuccInclusion P i)) ≃ₗ[R ⧸ p]
          S ⧸ P
⊢ HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)) ≃ₗ[R ⧸ p]
    S ⧸ P

Tactic:
choose a a_mem a_notMem using
    SetLike.exists_of_lt
      (Ideal.pow_right_strictAnti P hP (Ideal.IsPrime.ne_top inferInstance) (le_refl i.succ))

Premises used: le_refl, SetLike.exists_of_lt, inferInstance, Ideal.pow_right_strictAnti, Ideal.IsPrime.ne_top, Nat.succ
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
a : S
a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a
a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ
refine_1 :
  LinearMap.{u, u, v, v} (R := R ⧸ p) (RingHom.id (R ⧸ p)) (S ⧸ P)
    (HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
refine_2 :
  Function.Injective (α := S ⧸ P) (β :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    (⇑(p.quotientToQuotientRangePowQuotSucc P a_mem) :
      (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
refine_3 :
  Function.Surjective (α := S ⧸ P) (β :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    (⇑(p.quotientToQuotientRangePowQuotSucc P a_mem) :
      (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
⊢ HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)) ≃ₗ[R ⧸ p]
    S ⧸ P

Tactic:
refine (LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩).symm

Premises used: LinearEquiv.symm, And.intro, LinearEquiv.ofBijective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
a : S
a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a
a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ
⊢ LinearMap.{u, u, v, v} (R := R ⧸ p) (RingHom.id (R ⧸ p)) (S ⧸ P)
    (HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))

Tactic:
exact quotientToQuotientRangePowQuotSucc p P a_mem

Premises used: Ideal.quotientToQuotientRangePowQuotSucc
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
a : S
a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a
a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ
⊢ Function.Injective (α := S ⧸ P) (β :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    (⇑(p.quotientToQuotientRangePowQuotSucc P a_mem) :
      (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)

Tactic:
quotientToQuotientRangePowQuotSucc_injective p P hi a_mem a_notMem

Premises used: Ideal.quotientToQuotientRangePowQuotSucc_injective