-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem quotientToQuotientRangePowQuotSucc_surjective [IsDedekindDomain S]
    (hP0 : P ≠ ⊥) [hP : P.IsPrime] {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i)
    (a_not_mem : a ∉ P ^ (i + 1)) :
    Function.Surjective (quotientToQuotientRangePowQuotSucc p P a_mem)

Proof state:
case mk.mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
p : Ideal R
P : Ideal S
inst✝¹ : Algebra R S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ x ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
letI := Classical.decEq (Ideal S)

Result:
case mk.mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
p : Ideal R
P : Ideal S
inst✝¹ : Algebra R S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
⊢ x ∈ span {a} ⊔ P ^ (i + 1)

Proof state:
case mk.mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
p : Ideal R
P : Ideal S
inst✝¹ : Algebra R S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_not_mem : ¬span {a} ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
⊢ x ∈ P ^ (Multiset.count P (normalizedFactors (span {a})) ⊓ (i + 1))

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

Result:
no goals

Proof state:
case mk.mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
p : Ideal R
P : Ideal S
inst✝¹ : Algebra R S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(LinearMap.range (p.powQuotSuccInclusion P i)).quotientRel
        ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x, hx✝⟩

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, Subtype.coe_mk,
    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]

Result:
case mk.mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
p : Ideal R
P : Ideal S
inst✝¹ : Algebra R S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ x ∈ span {a} ⊔ P ^ (i + 1)