-- 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:
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)
ha : span {a} = ⊥
⊢ False

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

Result:
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 : 0 ∉ 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)
ha : span {a} = ⊥
⊢ False

Proof state:
case intro.intro.intro.intro.intro
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
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ y_1, ↑((p.powQuotSuccInclusion P i) y_1) = (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)

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

Result:
case intro.intro.intro.intro.intro
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
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ↑((p.powQuotSuccInclusion P i) ⟨(Quotient.mk (P ^ e)) (-z), ⋯⟩) =
    (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)

Proof state:
case intro.intro.intro.intro.intro
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
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(LinearMap.range (p.powQuotSuccInclusion P i)).quotientRel
        ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z), hx✝⟩

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

Result:
case intro.intro.intro.intro.intro
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
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ (p.quotientToQuotientRangePowQuotSucc P a_mem) (Submodule.Quotient.mk y) =
    Quot.mk ⇑(LinearMap.range (p.powQuotSuccInclusion P i)).quotientRel
      ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z), hx✝⟩

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
this : DecidableEq (Ideal S) := Classical.decEq (Ideal S)
⊢ x ∈ P ^ (Multiset.count P (normalizedFactors (span {a})) ⊓ (i + 1))

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

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 : 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))

Proof state:
case intro.intro.intro.intro.intro
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
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ↑((p.powQuotSuccInclusion P i) ⟨(Quotient.mk (P ^ e)) (-z), ⋯⟩) =
    (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)

Tactic:
rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add,
  sub_add_cancel_left, map_neg]

Result:
no goals