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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : (Submodule.quotientRel P : S → S → Prop) x 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)
have 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)) sorry :
            ↥(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)) sorry :
            ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))))
        y))
Tactic: rw [Submodule.quotientRel_def] 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
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))
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 =
    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))
        sorry)
      (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))
        sorry)
Tactic: simp only [map_mul, LinearMap.mem_range]
-- 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
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))
          ⋯)
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) (a * (x - y))) sorry) =
  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))
      sorry)
    (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))
      sorry)
Tactic: refine ⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ (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))
        ⋯)
have 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))) sorry)) :
    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))
          sorry)
        (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))
          sorry)) :
    S ⧸ P ^ e)
Tactic: ext
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
⊢ (↑((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)
have a₁ : (↑(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))) sorry) :
    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))
          sorry)
        (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))
          sorry)) :
    S ⧸ P ^ e)
Tactic: rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.coe_sub, Subtype.coe_mk,
      Subtype.coe_mk, map_mul, map_sub, mul_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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S ⧸ P
⊢ 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)
have 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))
Tactic: induction x, y using Quotient.inductionOn₂' with | _ x y
Cleared hypotheses: x, y
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R ⧸ p
y : S ⧸ P
⊢ 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)
have 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))
Tactic: induction x, y using Quotient.inductionOn₂' with | _ x y
Cleared hypotheses: x, y
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
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))
have 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)) sorry) :
      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: simp only [Submodule.Quotient.mk''_eq_mk, RingHom.id_apply,
      quotientToQuotientRangePowQuotSuccAux_mk]
-- 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
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)))
have 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)) sorry :
        ↥(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)) sorry))
Tactic: refine congr_arg Submodule.Quotient.mk ?_
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ 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)) ⋯))
have 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)) sorry :
            ↥(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)) sorry)) :
    S ⧸ P ^ e)
Tactic: ext
-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ 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)
have 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))
Tactic: simp only [map_mul, Quotient.mk_eq_mk, Submodule.coe_smul_of_tower,
      Algebra.smul_def, Quotient.algebraMap_quotient_pow_ramificationIdx]
-- 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
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)))
⊢ Eq (α := S ⧸ P) (Quotient.mk'' x) (Quotient.mk'' y)
have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
Tactic: have Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1) := Ideal.pow_le_pow_right hi