awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
inst_7 : Semiring B
inst_8 : Algebra R₁ B
I : Ideal A
inst_9 : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
r : R₁
this :
  Eq.{u_3 + 1} (α := A ⧸ I) ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) r : A ⧸ I)
    ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r) : A ⧸ I)
rw :
  OneHom.toFun (↑(↑(lift I (↑f : A →+* B) hI) : A ⧸ I →* B) : OneHom (A ⧸ I) B)
      ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r)) =
    (algebraMap R₁ B : (a : R₁) → B) r
rw₁ :
  Eq.{u_4 + 1} (α := B)
    ((lift I (↑f : A →+* B) hI : (a : A ⧸ I) → B)
        ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r) : A ⧸ I) :
      B)
    ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₂ :
  Eq.{u_4 + 1} (α := B) (((↑f : A →+* B) : (a : A) → B) ((algebraMap R₁ A : (a : R₁) → A) r : A) : B)
    ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₃ :
  Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) ((algebraMap R₁ A : (a : R₁) → A) r : A) : B)
    ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₄ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) r 1) : B) ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₅ : (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r 1
rw₆ : HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B) = HSMul.hSMul (β := B) r 1
⊢ OneHom.toFun (↑(↑(lift I (↑f : A →+* B) hI) : A ⧸ I →* B) : OneHom (A ⧸ I) B)
      ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) r) =
    (algebraMap R₁ B : (a : R₁) → B) r
have rw₇ : HSMul.hSMul (β := B) r 1 = HSMul.hSMul (β := B) r 1
Tactic: rw [this, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk,
        AlgHom.coe_toRingHom, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one,
        map_smul, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₄ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (A ∙ 1))
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
rw₄ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (A ∙ 1))
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₅ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
  (Submodule.span A (Set.image (α := A) (⇑(Submodule.mkQ I) : (a : A) → A ⧸ I) {1}))
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
rw₄ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (A ∙ 1))
rw₅ :
  Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
    (Submodule.span A (Set.image (α := A) (⇑(Submodule.mkQ I) : (a : A) → A ⧸ I) {1}))
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₆ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ (Submodule.mkQ I : (a : A) → A ⧸ I) 1)
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
rw₄ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (A ∙ 1))
rw₅ :
  Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
    (Submodule.span A (Set.image (α := A) (⇑(Submodule.mkQ I) : (a : A) → A ⧸ I) {1}))
rw₆ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ (Submodule.mkQ I : (a : A) → A ⧸ I) 1)
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₇ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ Submodule.Quotient.mk 1)
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
rw₄ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (A ∙ 1))
rw₅ :
  Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
    (Submodule.span A (Set.image (α := A) (⇑(Submodule.mkQ I) : (a : A) → A ⧸ I) {1}))
rw₆ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ (Submodule.mkQ I : (a : A) → A ⧸ I) 1)
rw₇ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ Submodule.Quotient.mk 1)
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤
have rw₈ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
Tactic: rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : HasQuotient.Quotient A (B := Ideal A) (ker f)
⊢ (f.kerLift : (a : A ⧸ ker f.toRingHom) → B) (r • x) =
    HSMul.hSMul (β := B) r ((f.kerLift : (a : A ⧸ ker f.toRingHom) → B) x : B)
have obtain : ∀ (a : A),
  (f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
      (HSMul.hSMul (β := HasQuotient.Quotient A (B := Ideal A) (ker f)) r
        ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f))) =
    HSMul.hSMul (β := B) r
      ((f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
          ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
        B)
Tactic: obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
⊢ Eq.{u_3 + 1} (α := HasQuotient.Quotient A (B := Ideal A) (ker f))
    (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) a) :
      HasQuotient.Quotient A (B := Ideal A) (ker f))
    ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f))
have a₁ : Eq.{u_4 + 1} (α := B)
  ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
      (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) a) :
        HasQuotient.Quotient A (B := Ideal A) (ker f)) :
    B)
  ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
      ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
    B)
Tactic: apply (Ideal.quotientKerAlgEquivOfSurjective hf).injective
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
⊢ Eq.{u_8 + 1} (α := C) ((f.liftOfSurjective hf g H : (a : B) → C) ((f : (a : A) → B) x : B) : C)
    ((g : (a : A) → C) x : C)
have dsimp : Eq.{u_8 + 1} (α := C)
  ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
      (((↑(quotientKerAlgEquivOfSurjective hf).symm : B →ₐ[R] A ⧸ ker f) : (a : B) → A ⧸ ker (↑f : A →+* B))
          ((f : (a : A) → B) x) :
        HasQuotient.Quotient A (B := Ideal A) (ker (F := A →+* B) (↑f : A →+* B))) :
    C)
  ((g : (a : A) → C) x : C)
Tactic: dsimp [AlgHom.liftOfSurjective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
⊢ Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        (((↑(quotientKerAlgEquivOfSurjective hf).symm : B →ₐ[R] A ⧸ ker f) : (a : B) → A ⧸ ker (↑f : A →+* B))
            ((f : (a : A) → B) x) :
          HasQuotient.Quotient A (B := Ideal A) (ker (F := A →+* B) (↑f : A →+* B))) :
      C)
    ((g : (a : A) → C) x : C)
have erw : Eq.{u_8 + 1} (α := C)
  ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
      (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) x) :
        HasQuotient.Quotient A (B := Ideal A) (ker f)) :
    C)
  ((g : (a : A) → C) x : C)
Tactic: erw [AlgEquiv.coe_algHom]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
⊢ Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) x) :
          HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      C)
    ((g : (a : A) → C) x : C)
have rw : Eq.{u_8 + 1} (α := C)
  ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
      ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) x : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
    C)
  ((g : (a : A) → C) x : C)
Tactic: rw [Ideal.quotientKerAlgEquivOfSurjective_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
⊢ (f.liftOfSurjective hf g H).comp f = g
have H₁ : ∀ (x : A), Eq.{u_8 + 1} (α := C) (((f.liftOfSurjective hf g H).comp f : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
hg : Surjective.{u_6 + 1, u_8 + 1} (α := A) (β := C) (⇑g : (a : A) → C)
⊢ Surjective.{u_6 + 1, u_8 + 1} (α := A) (β := C)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := B) (⇑(f.liftOfSurjective hf g H) : (a : B) → C) (⇑f : (a : A) → B))
have h : Eq (α := A → C)
  (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := B) (⇑(f.liftOfSurjective hf g H) : (a : B) → C) (⇑f : (a : A) → B))
  (⇑g : (a : A) → C)
Tactic: convert! hg
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
hg : Surjective.{u_6 + 1, u_8 + 1} (α := A) (β := C) (⇑g : (a : A) → C)
⊢ Eq (α := A → C)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := B) (⇑(f.liftOfSurjective hf g H) : (a : B) → C) (⇑f : (a : A) → B))
    (⇑g : (a : A) → C)
have h : ∀ (x : A),
  Eq.{u_8 + 1} (α := C)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := B) (⇑(f.liftOfSurjective hf g H) : (a : B) → C) (⇑f : (a : A) → B)
        x :
      C)
    ((g : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw : Eq (α := Ideal (R ⧸ J))
  (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
    (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) sorry))
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₁ : Eq (α := Ideal (R ⧸ J))
  (map (F := R →+* R ⧸ J) (Quotient.mk J)
    (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₂ : Eq (α := Ideal (R ⧸ J))
  (map (F := R →+* R ⧸ J) (Quotient.mk J)
    (comap (F := R →+* R ⧸ I) (Quotient.mk I)
      (ker (F := R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
rw :
  Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (Quotient.lift J (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I)) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₁ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (ker (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        (RingHom.comp (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) (Quotient.mk I))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₂ :
  Eq (α := Ideal (R ⧸ J))
    (map (F := R →+* R ⧸ J) (Quotient.mk J)
      (comap (F := R →+* R ⧸ I) (Quotient.mk I)
        (ker (F :=
          R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
          (Quotient.mk (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
⊢ Eq (α := Ideal (R ⧸ J))
    (ker (F := R ⧸ J →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      (quotientMap (map (F := R →+* R ⧸ I) (Quotient.mk I) J) (Quotient.mk I) ⋯))
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
have rw₃ : Eq (α := Ideal (R ⧸ J))
  (map (F := R →+* R ⧸ J) (Quotient.mk J)
    (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)))
  (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
Tactic: rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]