awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
refine_1 : HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ ≤ Submodule.comap (Submodule.subtype (I ^ n)) (I ^ (n + 1))
refine_2 :
  ∀ (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤),
    Membership.mem (α := R ⧸ I ^ (n + 1)) (γ := Submodule R (R ⧸ I ^ (n + 1)))
      (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
      (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
            (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
          c :
        R ⧸ I ^ (n + 1))
refine_3 :
  Function.Injective (β := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
    fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
    Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
      Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
        (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
      (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
          (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
        c)
      ⋯
⊢ (↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ≃ₗ[R]
    ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))
have refine_4 : Function.Surjective (β := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
  fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
  Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
    Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
      (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
    (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) sorry :
        (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
      c)
    sorry
Tactic: refine { LinearMap.codRestrict
    (Submodule.restrictScalars _ (Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n)))
    (Submodule.mapQ (I • ⊤) (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?_) ?_,
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
⊢ Membership.mem (α := R ⧸ I ^ (n + 1)) (γ := Submodule R (R ⧸ I ^ (n + 1)))
    (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
    (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
          (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
        x :
      R ⧸ I ^ (n + 1))
have refine_2 : ∀ (y : R) (hy : y ∈ I ^ n),
  Membership.mem (α := R ⧸ I ^ (n + 1)) (γ := Submodule R (R ⧸ I ^ (n + 1)))
    (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
    (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) sorry :
          (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
        (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) y hy)) :
      R ⧸ I ^ (n + 1))
Tactic: obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : R ⧸ I ^ (n + 1)
hx :
  Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1))) (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x
⊢ ∃ (a : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤),
    (fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
          (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
              Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
              (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
                  (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                c)
              ⋯ :
            ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
        a =
      Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
        Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1)))
          (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x)
        x hx
have hx₁ : ∃ x_1 ∈ I ^ n, (Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) x_1 = x
Tactic: rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : R ⧸ I ^ (n + 1)
hx_1 :
  Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1))) (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x
hx : ∃ x_1 ∈ I ^ n, (Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) x_1 = x
⊢ ∃ (a : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤),
    (fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
          (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
              Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
              (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
                  (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                c)
              ⋯ :
            ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
        a =
      Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
        Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1)))
          (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x)
        x hx_1
have refine_4 : ∀ (y : R) (hy : y ∈ I ^ n)
  (hx :
    Membership.mem (α := R ⧸ I ^ (n + 1)) (γ := Ideal (R ⧸ I ^ (n + 1)))
      (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))
      ((Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) y : R ⧸ I ^ (n + 1))),
  ∃ (a : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤),
    Eq (α := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
      ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
            (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
                Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                  (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
                  x)
                (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) sorry :
                    (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                  c)
                sorry :
              ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
          a :
        ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))))
      (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
          Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1)))
            (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x)
          ((Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) y) hx :
        ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
Tactic: obtain ⟨y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
y : R
hy : y ∈ I ^ n
hx :
  Membership.mem (α := R ⧸ I ^ (n + 1)) (γ := Ideal (R ⧸ I ^ (n + 1)))
    (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))
    ((Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) y : R ⧸ I ^ (n + 1))
⊢ ∃ (a : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤),
    Eq (α := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
      ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
            (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
                Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                  (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
                  x)
                (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
                    (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                  c)
                ⋯ :
              ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
          a :
        ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))))
      (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
          Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1)))
            (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x)
          ((Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) y) hx :
        ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
have refine_4 : Eq (α := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
  ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
        (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
            Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
              (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
            (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) sorry :
                (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
              c)
            sorry :
          ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) y hy)) :
    ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))))
  (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
      Membership.mem (γ := Ideal (R ⧸ I ^ (n + 1)))
        (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)) x)
      ((Quotient.mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) y) hx :
    ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
Tactic: refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
⊢ Eq (α := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) (map (F := R →+* R ⧸ I) (mk I) J)
have h : ∀ (x : R ⧸ I),
  Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
x : R ⧸ I
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
have h : ∀ (h : Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x),
  Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
x : R ⧸ I
h :
  ∀ (h : Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x),
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
have h₁ : ∀ (h : Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x),
  Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
x : R ⧸ I
h : Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
have h₁ : ∀ (r : R) (hr : (mk I : (a : R) → R ⧸ I) r = x), Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
Tactic: rcases Ideal.Quotient.mk_surjective x with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
x : R ⧸ I
h : Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x
r : R
hr : (mk I : (a : R) → R ⧸ I) r = x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
have h₁ : ∀
  (h :
    Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H))
      ((mk I : (a : R) → R ⧸ I) r : R ⧸ I))
  (hr : (mk I : (a : R) → R ⧸ I) r = x),
  Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J)
    ((mk I : (a : R) → R ⧸ I) r : R ⧸ I)
Tactic: rw [← hr] at h ⊢
Cleared hypotheses: h, hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
x : R ⧸ I
r : R
h :
  Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H))
    ((mk I : (a : R) → R ⧸ I) r : R ⧸ I)
hr : (mk I : (a : R) → R ⧸ I) r = x
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J)
    ((mk I : (a : R) → R ⧸ I) r : R ⧸ I)
have h₁ : r ∈ J
Tactic: simp only [factor, RingHom.mem_ker, lift_mk, eq_zero_iff_mem] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
x : R ⧸ I
h : Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x
have h₁ : ∀ (r : R) (hr : r ∈ (↑J : Set R)) (eq : (mk I : (a : R) → R ⧸ I) r = x),
  Membership.mem (γ := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) x
Tactic: rcases mem_image_of_mem_map_of_surjective _ Ideal.Quotient.mk_surjective h with ⟨r, hr, eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
have this : n = m + (n - m)
Tactic: have : n = m + (n - m) := (Nat.add_sub_of_le g).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
hmn : n - m = 0
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
have this₁ : n = m
Tactic: rw [hmn, Nat.add_zero] at this
Cleared hypotheses: this, hmn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m
hmn : n - m = 0
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
have zero : ∀ (g : n ≤ n) (hmn : n - n = 0), x n = (factor sorry : (a : M ⧸ p n) → M ⧸ p n) (x n)
Tactic: subst this
Cleared hypotheses: m, g, this, hmn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
hmn : n - m = k + 1
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
have this₁ : n = m + k + 1
Tactic: rw [hmn, ← add_assoc] at this
Cleared hypotheses: this, hmn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m n : ℕ
g : m ≤ n
this : n = m + k + 1
hmn : n - m = k + 1
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
have succ : ∀ (g : m ≤ m + k + 1) (hmn : m + k + 1 - m = k + 1),
  x m = (factor sorry : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1))
Tactic: subst this
Cleared hypotheses: n, g, this, hmn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
⊢ x m = (factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1))
have succ : Eq (α := M ⧸ p m)
  ((factor sorry : (a : M ⧸ p (m + k)) → M ⧸ p m) ((factor sorry : (a : M ⧸ p (m + k).succ) → M ⧸ p (m + k)) (x (m + k + 1))) :
    M ⧸ p m)
  ((factor sorry : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1)) : M ⧸ p m)
Tactic: rw [ih (m.le_add_right k) (by simp), h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
succ :
  Eq (α := M ⧸ p m)
    ((factor ⋯ : (a : M ⧸ p (m + k)) → M ⧸ p m)
        ((factor ⋯ : (a : M ⧸ p (m + k).succ) → M ⧸ p (m + k)) (x (m + k + 1))) :
      M ⧸ p m)
    ((factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1)) : M ⧸ p m)
⊢ x m = (factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1))
have succ₁ : m + k - m = k
Tactic: rw [ih (m.le_add_right k) (by simp), h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
have induction : ∀ (x_1 : ℕ) (hmn : n - m = x_1), x m = (factor sorry : (a : M ⧸ p n) → M ⧸ p m) (x n)
Tactic: induction hmn : n - m generalizing m n with
  | zero =>
    rw [hmn, Nat.add_zero] at this
    subst this
    simp
  | succ k ih =>
    rw [hmn, ← add_assoc] at this
    subst this
    rw [ih (m.le_add_right k) (by simp), h]
    · simp
    · lia
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
⊢ Eq (α := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I))
    (map (F := R →+* R ⧸ K) (mk K) I)
have h : ∀ (x : R ⧸ K),
  Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x ↔
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x ↔
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
have h : ∀
  (h :
    Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I))
      x),
  Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h :
  ∀
    (h :
      Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I))
        x),
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x ↔
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
have h₁ : ∀ (h : Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x),
  Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
have h₁ : ∀ (r : R) (hr : r ∈ (↑I : Set R))
  (eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)),
  Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
Tactic: rcases mem_image_of_mem_map_of_surjective (mk J) Quotient.mk_surjective h with ⟨r, hr, eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
have this : Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
  (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))
Tactic: have : x - ((mk K) r) ∈ J.map (mk K) := by
      simp [← factor_ker hJK, ← eq]