awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x_1 : S ⧸ P
x : S
y_1 : S ⧸ P
y : S
h :
  Eq (α :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    ((p.quotientToQuotientRangePowQuotSucc P a_mem :
          (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
        (Quotient.mk'' x) :
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
    ((p.quotientToQuotientRangePowQuotSucc P a_mem :
          (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
        (Quotient.mk'' y) :
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
⊢ Eq (α := S ⧸ P) (Quotient.mk'' x) (Quotient.mk'' y)
have simp : ∀
  (h :
    ∃ (y_2 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
      (↑((p.powQuotSuccInclusion P i :
                (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
              y_2) :
          S ⧸ P ^ e) =
        HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x) : S ⧸ P ^ e)
          ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)),
  x - y ∈ P
Tactic: simp only [Submodule.Quotient.mk''_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
        Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff,
        Submodule.coe_sub] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x_1 : S ⧸ P
x : S
y_1 : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
h :
  ∃ (y_2 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
    (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            y_2) :
        S ⧸ P ^ e) =
      HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x) : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
⊢ x - y ∈ P
have mk : ∀ (val : S ⧸ P ^ e) (z : S)
  (hz :
    Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))
      (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) z))
  (h :
    (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
              Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))
                x)
              (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) z) hz)) :
        S ⧸ P ^ e) =
      HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x) : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)),
  x - y ∈ P
Tactic: rcases h with ⟨⟨⟨z⟩, hz⟩, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x_1 : S ⧸ P
x : S
y_1 : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val : S ⧸ P ^ e
z : S
hz :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) z)
h :
  (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) z) hz)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x) : S ⧸ P ^ e)
      ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
⊢ x - y ∈ P
have hz₁ : z ∈ P ^ (i + 1)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x_1 : S ⧸ P
x : S
y_1 : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val : S ⧸ P ^ e
z : S
hz_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) z)
hz : z ∈ P ^ (i + 1)
h :
  (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) z) hz_1)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x) : S ⧸ P ^ e)
      ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
⊢ x - y ∈ P
have h₁ : z - a * (x - y) ∈ P ^ e
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
⊢ ∃ (a_1 : S ⧸ P),
    Eq (α :=
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
      ((p.quotientToQuotientRangePowQuotSucc P a_mem :
            (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
          a_1 :
        HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i)))
      (Quot.mk
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x) hx) :
        Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))
have Pe_le_Pi : P ^ e ≤ P ^ i
Tactic: have Pe_le_Pi : P ^ e ≤ P ^ i := Ideal.pow_le_pow_right hi.le
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
x : S
hx :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x)
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ ∃ (a_1 : S ⧸ P),
    Eq (α :=
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
      ((p.quotientToQuotientRangePowQuotSucc P a_mem :
            (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
          a_1 :
        HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i)))
      (Quot.mk
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) x) hx) :
        Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))
have hx₁ : x ∈ P ^ i
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
Cleared hypotheses: Pe_le_Pi
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (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' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ Eq (α :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    ((p.quotientToQuotientRangePowQuotSucc P a_mem :
          (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
        (Submodule.Quotient.mk y) :
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
    (Quot.mk
        (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
          ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
        (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
          (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z)) hx_1) :
      Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
          ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))
have simp : ∃ (y_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
  (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          y_1) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
Tactic: simp only [Submodule.Quotient.quot_mk_eq_mk, quotientToQuotientRangePowQuotSucc_mk,
      Submodule.Quotient.eq, LinearMap.mem_range, Subtype.ext_iff,
      Submodule.coe_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (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' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ (y_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
    (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            y_1) :
        S ⧸ P ^ e) =
      HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
        (Submodule.Quotient.mk (a * y + z))
have refine : (↑((p.powQuotSuccInclusion P i :
          (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
        (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
          ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) sorry)) :
    S ⧸ P ^ e) =
  HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
    (Submodule.Quotient.mk (a * y + z))
Tactic: refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (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' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) ⋯)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
have rw : (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
        Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) sorry) :
    S ⧸ P ^ e) =
  HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
    (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (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' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
rw :
  (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
          ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) ⋯) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
⊢ (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) ⋯)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
have rw₁ : (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) =
  HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
    (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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (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' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
rw :
  (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
          ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) ⋯) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
rw₁ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
⊢ (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z)) ⋯)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
have rw₂ : (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) =
  HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
    ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y + z) : S ⧸ P ^ e)
Tactic: rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add,
      sub_add_cancel_left, map_neg]