-- 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)
⊢ span {a} ≠ ⊥

Tactic:
intro ha

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

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)
⊢ ∃ 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:
have Pe_le_Pi : P ^ e ≤ P ^ i := Ideal.pow_le_pow_right hi.le

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

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
hx' : x ∈ 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))) x, hx✝⟩

Tactic:
obtain ⟨y', hy', z, hz, rfl⟩ := Submodule.mem_sup.mp hx'

Result:
case 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
y' : S
hy' : y' ∈ span {a}
z : S
hz : z ∈ P ^ (i + 1)
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (y' + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : y' + z ∈ P ^ i
hx' : 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))) (y' + z), hx✝⟩

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 : 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} = ⊥
this : 0 ∈ P ^ (i + 1)
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case 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
y' : S
hy' : y' ∈ span {a}
z : S
hz : z ∈ P ^ (i + 1)
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (y' + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : y' + z ∈ P ^ i
hx' : 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))) (y' + z), hx✝⟩

Tactic:
obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hy'

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)
⊢ ∃ 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✝⟩