awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
A : Type u_1
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
I J : Ideal A
h : I ≤ J
x : A ⧸ I
H :
  ∀ (x : A),
    Eq (α := A ⧸ J)
      ((AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h) : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J →ₐ[R] A ⧸ J)
              (Quotient.mkₐ R (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) :
            (a : A ⧸ I) → A ⧸ J)
          ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x) :
        A ⧸ J)
      ((Quotient.factorₐ R h : (a : A ⧸ I) → A ⧸ J) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x) : A ⧸ J)
⊢ Eq (α := A ⧸ J)
    ((AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h) : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J →ₐ[R] A ⧸ J)
            (Quotient.mkₐ R (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) :
          (a : A ⧸ I) → A ⧸ J)
        x :
      A ⧸ J)
    ((Quotient.factorₐ R h : (a : A ⧸ I) → A ⧸ J) x : A ⧸ J)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
A : Type u_1
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
I J : Ideal A
h : I ≤ J
x : A
⊢ Eq (α := A ⧸ J)
    ((AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h) : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J →ₐ[R] A ⧸ J)
            (Quotient.mkₐ R (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) :
          (a : A ⧸ I) → A ⧸ J)
        ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x) :
      A ⧸ J)
    ((Quotient.factorₐ R h : (a : A ⧸ I) → A ⧸ J) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) x) : A ⧸ J)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
      ⋯
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)) ⋯ :
          (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))

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 }

Premises used: Ideal.Quotient.mk, Submodule.restrictScalars, Ideal.map, Submodule.mapQ, HPow.hPow, HAdd.hAdd, And.intro, Equiv.ofBijective, Submodule.subtype, LinearMap.codRestrict, HSMul.hSMul, Top.top, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : ↥(I ^ n)
⊢ x ∈ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ → x ∈ Submodule.comap (Submodule.subtype (I ^ n)) (I ^ (n + 1))

Tactic:
simp [Submodule.mem_smul_top_iff, pow_succ']

Premises used: Submodule.mem_smul_top_iff, pow_succ'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
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)) ⋯ :
            (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))
⊢ 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))

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ x

Premises used: Submodule.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
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)) ⋯ :
          (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:
simp [Ideal.mem_sup_left hy]

Premises used: Ideal.mem_sup_left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ I ^ n
⊢ Eq.{u_1 + 1} (α := ↥(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)))))
        (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx)))
      ((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)))))
        (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) y hy))) →
    Eq (α := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx))
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) y hy))

Tactic:
simp [Ideal.Quotient.eq, Submodule.Quotient.eq, Submodule.mem_smul_top_iff, pow_succ']

Premises used: Submodule.Quotient.eq, Ideal.Quotient.eq, Submodule.mem_smul_top_iff, pow_succ'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
⊢ ∃ 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

Premises used: Ideal.Quotient.mk_surjective, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
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)) ⋯ :
                      (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)))
⊢ ∃ (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

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)))

Tactic:
⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩

Premises used: Submodule.Quotient.mk, Subtype.mk, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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))
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)) ⋯ :
                  (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)))))
        (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)))
⊢ ∃ (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)))

Tactic:
refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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))
⊢ 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)))))
        (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:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
H : I ≤ J
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
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
⊢ Eq (α := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* R ⧸ J) (factor H)) (map (F := R →+* R ⧸ I) (mk I) J)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
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
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
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
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x

Tactic:
rcases Ideal.Quotient.mk_surjective x with ⟨r, hr⟩

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
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)
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (mk I) J) x

Tactic:
rw [← hr] at h ⊢
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
⊢ r ∈ J

Tactic:
simp only [factor, RingHom.mem_ker, lift_mk, eq_zero_iff_mem] at h

Premises used: RingHom.mem_ker, Ideal.Quotient.lift_mk, Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.factor
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
hr : (mk I : (a : R) → R ⧸ I) r = x
h : r ∈ J
⊢ 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:
Ideal.mem_map_of_mem _ h

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
hr : (mk I : (a : R) → R ⧸ I) r = x
h : r ∈ J
⊢ 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:
exact Ideal.mem_map_of_mem _ h

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
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
⊢ 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⟩

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Ideal.Quotient.mk_surjective, Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
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:
simpa [← eq, Ideal.Quotient.eq_zero_iff_mem] using hr

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
⊢ n = m + (n - m)

Tactic:
have : n = m + (n - m) := (Nat.add_sub_of_le g).symm