-- 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)
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:
rw [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.mem_quotient_iff_mem_sup,
  sup_eq_left.mpr Pe_le_Pi] at hx

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

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

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)
⊢ ∃ y_1, ↑((p.powQuotSuccInclusion P i) y_1) = (Quotient.mk (P ^ e)) (a * y) - Submodule.Quotient.mk (a * y + z)

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 ∈ 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]

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 ∈ P ^ (Multiset.count P (normalizedFactors (span {a})) ⊓ (i + 1))

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} ≠ ⊥

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} = ⊥
⊢ False

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

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)
⊢ Function.Surjective ⇑(p.quotientToQuotientRangePowQuotSucc P a_mem)

Tactic:
rintro ⟨⟨⟨x⟩, hx⟩⟩

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