awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
h :
  Eq.{v + 1} (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    ((fun (x : S) ↦
        (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)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x)) ⋯ :
          ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))))
      (x • y))
    ((fun (x_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))) ↦
        HSMul.hSMul (α := R ⧸ p) (Submodule.Quotient.mk x) x_1)
      (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)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y)) ⋯))
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem
      (HSMul.hSMul (α := R ⧸ p) (β := S ⧸ P) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)) =
    HSMul.hSMul (α := R ⧸ p) (β :=
      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)))
      (Submodule.Quotient.mk x)
      (Submodule.Quotient.mk
          (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)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * 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)))

Tactic:
refine congr_arg Submodule.Quotient.mk ?_

Premises used: Submodule.Quotient.mk, congr_arg
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
h :
  Eq.{v + 1} (α := S ⧸ P ^ e)
    (↑((fun (x : S) ↦
            (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)
                ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x)) ⋯ :
              ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))))
          (x • y)) :
      S ⧸ P ^ e)
    (↑((fun (x_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))) ↦
            HSMul.hSMul (α := R ⧸ p) (Submodule.Quotient.mk x) x_1)
          (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)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y)) ⋯)) :
      S ⧸ P ^ e)
⊢ Eq.{v + 1} (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    ((fun (x : S) ↦
        (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)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x)) ⋯ :
          ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))))
      (x • y))
    ((fun (x_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))) ↦
        HSMul.hSMul (α := R ⧸ p) (Submodule.Quotient.mk x) x_1)
      (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)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y)) ⋯))

Tactic:
ext
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
h :
  HMul.hMul (α := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
      (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) ((f : (a : R) → S) x) : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e)) =
    HMul.hMul (α := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) ((f : (a : R) → S) x) : S ⧸ P ^ e)
      (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))
⊢ Eq.{v + 1} (α := S ⧸ P ^ e)
    (↑((fun (x : S) ↦
            (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)
                ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * x)) ⋯ :
              ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))))
          (x • y)) :
      S ⧸ P ^ e)
    (↑((fun (x_1 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))) ↦
            HSMul.hSMul (α := R ⧸ p) (Submodule.Quotient.mk x) x_1)
          (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)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y)) ⋯)) :
      S ⧸ P ^ e)

Tactic:
simp only [map_mul, Quotient.mk_eq_mk, Submodule.coe_smul_of_tower,
      Algebra.smul_def, Quotient.algebraMap_quotient_pow_ramificationIdx]

Premises used: Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx, map_mul, Submodule.coe_smul_of_tower, Ideal.Quotient.mk_eq_mk, Algebra.smul_def
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ HMul.hMul (α := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
      (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) ((f : (a : R) → S) x) : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e)) =
    HMul.hMul (α := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) ((f : (a : R) → S) x) : S ⧸ P ^ e)
      (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))

Tactic:
ring
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : S
⊢ 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 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)))
    (Submodule.Quotient.mk
        (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)
          ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * 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)))

Tactic:
quotientToQuotientRangePowQuotSuccAux_mk p P a_mem x

Premises used: Ideal.quotientToQuotientRangePowQuotSuccAux, Quot.map, Quotient.map', Ideal.quotientToQuotientRangePowQuotSuccAux_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)))
⊢ P ^ e ≤ P ^ (i + 1)

Tactic:
have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1) := Ideal.pow_le_pow_right hi
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
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
⊢ Eq (α := S ⧸ P) (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,
        Submodule.coe_sub] at h ⊢

Premises used: Submodule.Quotient.eq, Ideal.quotientToQuotientRangePowQuotSucc_mk, Subtype.ext_iff, Submodule.coe_sub, LinearMap.mem_range, Submodule.Quotient.mk''_eq_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
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
⊢ x - y ∈ P

Tactic:
rcases h with ⟨⟨⟨z⟩, hz⟩, h⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
⊢ 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

Premises used: Iff.mpr, sup_eq_left, Ideal.mem_quotient_iff_mem_sup, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
hz₁ : z ∈ 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)
            (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)

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

Premises used: Iff.mpr, sup_eq_left, Ideal.mem_quotient_iff_mem_sup, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
⊢ 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

Premises used: Subtype.coe_mk, map_sub, mul_sub, Ideal.powQuotSuccInclusion_apply_coe, Ideal.Quotient.eq, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : z - a * (x - y) ∈ P ^ e
⊢ x - y ∈ P

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

Premises used: Ideal.IsPrime.mem_pow_mul, Set.Mem, Or.resolve_left, Iff.mp, Submodule.sub_mem_iff_right
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : 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_notMem

Premises used: Ideal.IsPrime.mem_pow_mul, Or.resolve_left, Iff.mp, Submodule.sub_mem_iff_right
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
⊢ P ^ e ≤ P ^ i

Tactic:
have Pe_le_Pi : P ^ e ≤ P ^ i := Ideal.pow_le_pow_right hi.le
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
⊢ 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

Premises used: Iff.mpr, sup_eq_left, Ideal.mem_quotient_iff_mem_sup, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hx₁ : x ∈ P ^ i
⊢ P ^ e ≤ 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

Premises used: Iff.mpr, sup_eq_left, Ideal.mem_quotient_iff_mem_sup, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk