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
inst_3 : NeZero e
x : R
⊢ Eq.{v + 1} (α := S ⧸ P) ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) ((mk p : (a : R) → R ⧸ p) x) : S ⧸ P)
    ((mk P : (a : S) → S ⧸ P) ((f : (a : R) → S) x) : S ⧸ P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- 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
i : ℕ
rw :
  ∀ (m : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
    Eq (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        ((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            m :
          ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (0 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))) →
      m = 0
⊢ Function.Injective (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))) (β :=
    ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (⇑(p.powQuotSuccInclusion P i) :
      (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))

Tactic:
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']

Premises used: LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'
-- 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
i : ℕ
x : S ⧸ P ^ e
hx : Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x
hx0 :
  Eq (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    ((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) x
          hx) :
      ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (0 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
rw :
  ∀
    (hx0 :
      Eq.{v + 1} (α := S ⧸ P ^ e)
        (↑((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)
                x hx)) :
          S ⧸ P ^ e)
        (↑0 : S ⧸ P ^ e)),
    (↑(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)
            x hx) :
        S ⧸ P ^ e) =
      (↑0 : S ⧸ P ^ e)
⊢ 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) x hx =
    0

Tactic:
rw [Subtype.ext_iff] at hx0 ⊢

Premises used: Subtype.ext_iff
-- 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
i : ℕ
x : S ⧸ P ^ e
hx : Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x
hx0 :
  Eq.{v + 1} (α := S ⧸ P ^ e)
    (↑((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)
            x hx)) :
      S ⧸ P ^ e)
    (↑0 : S ⧸ P ^ e)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hx0 :
      (↑(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)
              x hx) :
          S ⧸ P ^ e) =
        (↑0 : S ⧸ P ^ e)),
    (↑(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)
            x hx) :
        S ⧸ P ^ e) =
      (↑0 : S ⧸ P ^ e)
⊢ (↑(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) x
          hx) :
      S ⧸ P ^ e) =
    (↑0 : S ⧸ P ^ e)

Tactic:
rwa [powQuotSuccInclusion_apply_coe] at hx0

Premises used: Ideal.powQuotSuccInclusion_apply_coe
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : (Submodule.quotientRel P : S → S → Prop) x y
rw :
  ∀ (h : x - y ∈ P),
    Membership.mem (γ := Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i))
      (HSub.hSub (α := ↥(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)
        ((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))))
          y))
⊢ ((p.powQuotSuccInclusion P i).range.quotientRel :
      ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
    ((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)
    ((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))))
      y)

Tactic:
rw [Submodule.quotientRel_def] at h ⊢

Premises used: Submodule.quotientRel_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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
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 =
      HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (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)) x)
          (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) x : S ⧸ P ^ e))
          ⋯)
        (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)
          (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))
          ⋯)
⊢ Membership.mem (γ := Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
    (HSub.hSub (α := ↥(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)
      ((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))))
        y))

Tactic:
simp only [map_mul, LinearMap.mem_range]

Premises used: map_mul, LinearMap.mem_range
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ ∃ (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 =
      HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (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)) x)
          (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) x : S ⧸ P ^ e))
          ⋯)
        (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)
          (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:
⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem h)⟩, ?_⟩

Premises used: Ideal.mem_map_of_mem, Ideal.mul_mem_mul, Subtype.mk, Exists.intro
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
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) (a * (x - y))) ⋯) =
    HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (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)) x)
        (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) x : S ⧸ P ^ e))
        ⋯)
      (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)
        (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))
        ⋯)
⊢ ∃ (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 =
      HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (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)) x)
          (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) x : S ⧸ P ^ e))
          ⋯)
        (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)
          (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:
refine ⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
a₁ :
  (↑((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) (a * (x - y))) ⋯)) :
      S ⧸ P ^ e) =
    (↑(HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (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)) x)
            (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) x : S ⧸ P ^ e))
            ⋯)
          (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)
            (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))
            ⋯)) :
      S ⧸ P ^ e)
⊢ (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) (a * (x - y))) ⋯) =
    HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (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)) x)
        (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) x : S ⧸ P ^ e))
        ⋯)
      (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)
        (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:
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
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.quotientToQuotientRangePowQuotSuccAux P a_mem (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 * x)) ⋯))

Tactic:
apply Quotient.map'_mk''

Premises used: Quotient.map'_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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S ⧸ P
h :
  ∀ (x y : S),
    p.quotientToQuotientRangePowQuotSuccAux P a_mem (HAdd.hAdd (α := S ⧸ P) (Quotient.mk'' x) (Quotient.mk'' y)) =
      HAdd.hAdd (α :=
        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.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x))
        (p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y))
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (x + y) =
    HAdd.hAdd (α :=
      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.quotientToQuotientRangePowQuotSuccAux P a_mem x) (p.quotientToQuotientRangePowQuotSuccAux P a_mem y)

Tactic:
induction x, y using Quotient.inductionOn₂' with | _ x y
-- 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 y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (HAdd.hAdd (α := S ⧸ P) (Quotient.mk'' x) (Quotient.mk'' y)) =
    HAdd.hAdd (α :=
      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.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x))
      (p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y))

Tactic:
simp only [Submodule.Quotient.mk''_eq_mk, ← Submodule.Quotient.mk_add,
      quotientToQuotientRangePowQuotSuccAux_mk, mul_add, map_add, map_mul, AddMemClass.mk_add_mk]

Premises used: Submodule.Quotient.mk_add, map_add, map_mul, AddMemClass.mk_add_mk, mul_add, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R ⧸ p
y : S ⧸ P
h :
  ∀ (x : R) (y : S),
    p.quotientToQuotientRangePowQuotSuccAux P a_mem
        (HSMul.hSMul (α := R ⧸ p) (β := S ⧸ P) (Quotient.mk'' x) (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)))
        ((RingHom.id (R ⧸ p) : (a : R ⧸ p) → R ⧸ p) (Quotient.mk'' x) : R ⧸ p)
        (p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y))
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (x • 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)))
      ((RingHom.id (R ⧸ p) : (a : R ⧸ p) → R ⧸ p) x : R ⧸ p) (p.quotientToQuotientRangePowQuotSuccAux P a_mem y)

Tactic:
induction x, y using Quotient.inductionOn₂' with | _ x y
-- 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 :
  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)))
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem
      (HSMul.hSMul (α := R ⧸ p) (β := S ⧸ P) (Quotient.mk'' x) (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)))
      ((RingHom.id (R ⧸ p) : (a : R ⧸ p) → R ⧸ p) (Quotient.mk'' x) : R ⧸ p)
      (p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y))

Tactic:
simp only [Submodule.Quotient.mk''_eq_mk, RingHom.id_apply,
      quotientToQuotientRangePowQuotSuccAux_mk]

Premises used: RingHom.id_apply, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ 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:
congr_arg Submodule.Quotient.mk ?_

Premises used: Set.Mem, Submodule.Quotient.mk, Ideal.quotientToQuotientRangePowQuotSuccAux, setOf, congr_arg, Quot.map, Quotient.map'