-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem quotientToQuotientRangePowQuotSucc_injective [IsDedekindDomain S] [P.IsPrime]
    {i : ℕ} (hi : i < e) {a : S} (a_mem : a ∈ P ^ i) (a_not_mem : a ∉ P ^ (i + 1)) :
    Function.Injective (quotientToQuotientRangePowQuotSucc p P a_mem) := fun x =>
  Quotient.inductionOn' x fun x y =>
    Quotient.inductionOn' y fun y h => by
      have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1) := Ideal.pow_le_pow_right hi
      simp only [Submodule.Quotient.mk''_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
        Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff, Subtype.coe_mk,
        Submodule.coe_sub] at h ⊢
      rcases h with ⟨⟨⟨z⟩, hz⟩, h⟩
      rw [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.mem_quotient_iff_mem_sup,
        sup_eq_left.mpr Pe_le_Pi1] at hz
      rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.Quotient.quot_mk_eq_mk,
        Ideal.Quotient.mk_eq_mk, ← map_sub, Ideal.Quotient.eq, ← mul_sub] at h
      exact
        (Ideal.IsPrime.mem_pow_mul _
              ((Submodule.sub_mem_iff_right _ hz).mp (Pe_le_Pi1 h))).resolve_left
          a_not_mem

Proof state:
case intro.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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h :
  ↑((p.powQuotSuccInclusion P i) ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz✝⟩) =
    (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

Tactic:
rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.Quotient.quot_mk_eq_mk,
  Ideal.Quotient.mk_eq_mk, ← map_sub, Ideal.Quotient.eq, ← mul_sub] at h

Result:
case intro.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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h : z - a * (x - y) ∈ P ^ e
⊢ x - y ∈ P

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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
h :
  (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' x) =
    (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' y)
⊢ Quotient.mk'' x = Quotient.mk'' y

Tactic:
have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1) := Ideal.pow_le_pow_right hi

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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
h :
  (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' x) =
    (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' y)
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
⊢ Quotient.mk'' x = Quotient.mk'' y

Proof state:
case intro.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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h : z - a * (x - y) ∈ P ^ e
⊢ x - y ∈ P

Tactic:
exact
  (Ideal.IsPrime.mem_pow_mul _
        ((Submodule.sub_mem_iff_right _ hz).mp (Pe_le_Pi1 h))).resolve_left
    a_not_mem

Result:
no goals

Proof state:
case intro.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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
h :
  ↑((p.powQuotSuccInclusion P i) ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz⟩) =
    (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

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_Pi1] at hz

Result:
case intro.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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h :
  ↑((p.powQuotSuccInclusion P i) ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz✝⟩) =
    (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
h :
  (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' x) =
    (p.quotientToQuotientRangePowQuotSucc P a_mem) (Quotient.mk'' y)
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
⊢ Quotient.mk'' x = Quotient.mk'' y

Tactic:
simp only [Submodule.Quotient.mk''_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
  Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff, Subtype.coe_mk,
  Submodule.coe_sub] at h ⊢

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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
h : ∃ y_1, ↑((p.powQuotSuccInclusion P i) y_1) = (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
h : ∃ y_1, ↑((p.powQuotSuccInclusion P i) y_1) = (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

Tactic:
rcases h with ⟨⟨⟨z⟩, hz⟩, h⟩

Result:
case intro.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
inst✝ : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_not_mem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
h :
  ↑((p.powQuotSuccInclusion P i) ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz⟩) =
    (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P