awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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).comp f : (a : A) → C) x : C) ((g : (a : A) → C) x : C)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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) (⇑g : (a : A) → C)

Tactic:
hg
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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)
⊢ 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))

Tactic:
convert! hg
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S_1 : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S_1
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
S : Type v
inst_7 : Ring S
I : Ideal R
J : Ideal S
inst_8 : I.IsTwoSided
inst_9 : J.IsTwoSided
f : R →+* S
hIJ : I ≤ comap f J
x : R
ha : x ∈ I
⊢ Eq.{v + 1} (α := S ⧸ J) (((RingHom.comp (Quotient.mk J) f : RingHom.{u, v} R (S ⧸ J)) : (a : R) → S ⧸ J) x : S ⧸ J)
    (0 : S ⧸ J)

Tactic:
simpa [Function.comp_apply, RingHom.coe_comp, Quotient.eq_zero_iff_mem] using hIJ ha

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
x : R
⊢ Eq.{v + 1} (α := S ⧸ I)
    (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
        ((Quotient.mk J : (a : R) → R ⧸ J) x) :
      S ⧸ I)
    ((Quotient.mk I : (a : S) → S ⧸ I) ((f : (a : R) → S) x) : S ⧸ I)

Tactic:
Quotient.lift_mk J _ _

Premises used: Submodule.Quotient.mk, Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
S : Type v
inst_3 : Ring S
J : Ideal A
I : Ideal S
inst_4 : I.IsTwoSided
inst_5 : J.IsTwoSided
f : A →+* S
H : J ≤ comap f I
x : R₁
⊢ Eq.{v + 1} (α := S ⧸ I)
    (((quotientMap I f H : RingHom.{u_3, v} (A ⧸ J) (S ⧸ I)) : (a : A ⧸ J) → S ⧸ I)
        ((algebraMap R₁ (A ⧸ J) : (a : R₁) → A ⧸ J) x) :
      S ⧸ I)
    ((Quotient.mk I : (a : S) → S ⧸ I) ((f : (a : A) → S) ((algebraMap R₁ A : (a : R₁) → A) x : A)) : S ⧸ I)

Tactic:
Quotient.lift_mk J _ _

Premises used: Submodule.Quotient.mk, Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
x : R
⊢ Eq.{v + 1} (α := S ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f H) (Quotient.mk J) :
            RingHom.{u, v} R (S ⧸ I)) :
          (a : R) → S ⧸ I)
        x :
      S ⧸ I)
    (((RingHom.comp (Quotient.mk I) f : RingHom.{u, v} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I)

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]

Premises used: Ideal.quotientMap_mk, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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)
rw₄ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) (J ⊔ comap (F := R →+* R ⧸ I) (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) (J ⊔ ker (F := R →+* R ⧸ I) (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) (J ⊔ I)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₇ :
  Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) J ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I)
    (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₈ : Eq (α := Ideal (R ⧸ J)) (⊥ ⊔ map (F := R →+* R ⧸ J) (Quotient.mk J) I) (map (F := R →+* R ⧸ J) (Quotient.mk J) I)
rw₉ rw₁₀ : Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) 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)

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]

Premises used: RingHom.comap_ker, bot_sup_eq, Ideal.map_quotient_self, Ideal.ker_quotient_lift, Ideal.map_sup, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.quotientMap, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S_1 : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S_1
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
S : Type v
inst_7 : Ring S
I : Ideal R
J : Ideal S
inst_8 : I.IsTwoSided
inst_9 : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (F := R →+* S) (↑f : R →+* S) I
x : R ⧸ I
r : R
⊢ Eq.{u + 1} (α := R ⧸ I)
    (((quotientMap I (↑f.symm : S →+* R) ⋯ : RingHom.{v, u} (S ⧸ J) (R ⧸ I)) : (a : S ⧸ J) → R ⧸ I)
        (OneHom.toFun (M := R ⧸ I) (↑(↑(quotientMap J (↑f : R →+* S) ⋯) : R ⧸ I →* S ⧸ J) : OneHom (R ⧸ I) (S ⧸ J))
          (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) r)) :
      R ⧸ I)
    (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) r : Quot (α := R) (⇑(Submodule.quotientRel I) : R → R → Prop))

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe,
      quotientMap_mk, RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]

Premises used: RingEquiv.symm_apply_apply, Ideal.quotientMap_mk, RingHom.toFun_eq_coe, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk, RingEquiv.coe_toRingHom
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S_1 : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S_1
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
S : Type v
inst_7 : Ring S
I : Ideal R
J : Ideal S
inst_8 : I.IsTwoSided
inst_9 : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (F := R →+* S) (↑f : R →+* S) I
x : S ⧸ J
s : S
⊢ OneHom.toFun (M := R ⧸ I) (↑(↑(quotientMap J (↑f : R →+* S) ⋯) : R ⧸ I →* S ⧸ J) : OneHom (R ⧸ I) (S ⧸ J))
      (((quotientMap I (↑f.symm : S →+* R) ⋯ : RingHom.{v, u} (S ⧸ J) (R ⧸ I)) : (a : S ⧸ J) → R ⧸ I)
        (Quot.mk (⇑(Submodule.quotientRel J) : S → S → Prop) s)) =
    Quot.mk (⇑(Submodule.quotientRel J) : S → S → Prop) s

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe,
      quotientMap_mk, RingEquiv.coe_toRingHom, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, Ideal.quotientMap_mk, RingHom.toFun_eq_coe, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk, RingEquiv.coe_toRingHom
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
I : Ideal R
J : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (F := R →+* S) (↑f : R →+* S) I
x : R
⊢ Eq.{v + 1} (α := S ⧸ J)
    (((I.quotientEquiv J f hIJ : RingEquiv.{u, v} (R ⧸ I) (S ⧸ J)) : (a : R ⧸ I) → S ⧸ J)
        ((Quotient.mk I : (a : R) → R ⧸ I) x) :
      S ⧸ J)
    ((Quotient.mk J : (a : S) → S ⧸ J) ((f : (a : R) → S) x) : S ⧸ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
I : Ideal R
J : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (F := R →+* S) (↑f : R →+* S) I
x : S
⊢ Eq.{u + 1} (α := R ⧸ I)
    (((RingEquiv.symm (I.quotientEquiv J f hIJ) : RingEquiv.{v, u} (S ⧸ J) (R ⧸ I)) : (a : S ⧸ J) → R ⧸ I)
        ((Quotient.mk J : (a : S) → S ⧸ J) x) :
      R ⧸ I)
    ((Quotient.mk I : (a : R) → R ⧸ I) ((f.symm : (a : S) → R) x) : R ⧸ I)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Injective.{u + 1, v + 1} (α := R ⧸ J) (β := S ⧸ I) (⇑(quotientMap I f H) : (a : R ⧸ J) → S ⧸ I)

Tactic:
(injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero, Ideal.quotientMap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
refine :
  ∀ (a : R ⧸ J)
    (ha :
      Eq.{v + 1} (α := S ⧸ I) (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
        (0 : S ⧸ I)),
    a = 0
⊢ Injective.{u + 1, v + 1} (α := R ⧸ J) (β := S ⧸ I) (⇑(quotientMap I f H) : (a : R ⧸ J) → S ⧸ I)

Tactic:
refine (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero, Ideal.quotientMap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
a : R ⧸ J
ha :
  Eq.{v + 1} (α := S ⧸ I) (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) a : S ⧸ I)
    (0 : S ⧸ I)
obtain :
  ∀ (r : R)
    (ha :
      Eq.{v + 1} (α := S ⧸ I)
        (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
            ((Quotient.mk J : (a : R) → R ⧸ J) r) :
          S ⧸ I)
        (0 : S ⧸ I)),
    Eq (α := R ⧸ J) ((Quotient.mk J : (a : R) → R ⧸ J) r : R ⧸ J) (0 : R ⧸ J)
⊢ a = 0

Tactic:
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha :
  Eq.{v + 1} (α := S ⧸ I)
    (((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
        ((Quotient.mk J : (a : R) → R ⧸ J) r) :
      S ⧸ I)
    (0 : S ⧸ I)
⊢ Membership.mem (α := S) I ((f : (a : R) → S) r : S)

Tactic:
rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha

Premises used: Ideal.quotientMap_mk, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : Membership.mem (α := S) I ((f : (a : R) → S) r : S)
⊢ Eq (α := R ⧸ J) ((Quotient.mk J : (a : R) → R ⧸ J) r : R ⧸ J) (0 : R ⧸ J)

Tactic:
Quotient.eq_zero_iff_mem.mpr (h ha)

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : Membership.mem (α := S) I ((f : (a : R) → S) r : S)
⊢ Eq (α := R ⧸ J) ((Quotient.mk J : (a : R) → R ⧸ J) r : R ⧸ J) (0 : R ⧸ J)

Tactic:
exact Quotient.eq_zero_iff_mem.mpr (h ha)

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
I : Ideal S
f : R →+* S
inst_2 : I.IsTwoSided
⊢ Injective.{u + 1, v + 1} (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (β := S ⧸ I)
    (⇑(quotientMap I f ⋯) : (a : R ⧸ comap f I) → S ⧸ I)

Tactic:
quotientMap_injective' le_rfl

Premises used: le_rfl, Ideal.quotientMap_injective'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
J : Ideal R
I : Ideal S
inst_2 : I.IsTwoSided
inst_3 : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x_1 : S ⧸ I
x : S
hx : (Quotient.mk I : (a : S) → S ⧸ I) x = x_1
y : R
hy : (f : (a : R) → S) y = x
⊢ ((quotientMap I f H : RingHom.{u, v} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I) ((Quotient.mk J : (a : R) → R ⧸ J) y) =
    x_1

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
⊢ let leq : LE.le (α := Ideal R) (comap f (comap g' I)) (comap g (comap f' I)) := ⋯;
  Eq (α := RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g leq))

Tactic:
RingHom.ext fun a => ?_

Premises used: RingHom.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
refine :
  ∀ (a : HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))),
    Eq.{u_6 + 1} (α := S' ⧸ I)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯) :
              RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
            (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
          a :
        S' ⧸ I)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g ⋯) :
              RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
            (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
          a :
        S' ⧸ I)
⊢ let leq : LE.le (α := Ideal R) (comap f (comap g' I)) (comap g (comap f' I)) := ⋯;
  Eq (α := RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g leq))

Tactic:
refine RingHom.ext fun a => ?_

Premises used: RingHom.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
a : HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))
obtain :
  ∀ (r : R),
    Eq.{u_6 + 1} (α := S' ⧸ I)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯) :
              RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
            (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
          ((Quotient.mk (comap f (comap g' I)) : (a : R) → R ⧸ comap f (comap g' I)) r) :
        S' ⧸ I)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g ⋯) :
              RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
            (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
          ((Quotient.mk (comap f (comap g' I)) : (a : R) → R ⧸ comap f (comap g' I)) r) :
        S' ⧸ I)
⊢ Eq.{u_6 + 1} (α := S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I g' ⋯) (quotientMap (comap g' I) f ⋯) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        a :
      S' ⧸ I)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I f' ⋯) (quotientMap (comap f' I) g ⋯) :
            RingHom.{u, u_6} (HasQuotient.Quotient R (B := Ideal R) (comap f (comap g' I))) (S' ⧸ I)) :
          (a : R ⧸ comap f (comap g' I)) → S' ⧸ I)
        a :
      S' ⧸ I)

Tactic:
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
r : R
⊢ Eq (α := S' ⧸ I) ((Quotient.mk I : (a : S') → S' ⧸ I) ((g' : (a : S) → S') ((f : (a : R) → S) r : S)) : S' ⧸ I)
    ((Quotient.mk I : (a : S') → S' ⧸ I) ((f' : (a : R') → S') ((g : (a : R) → R') r : R')) : S' ⧸ I)

Tactic:
(Ideal.Quotient.mk I).congr_arg (_root_.trans (g'.comp_apply f r).symm
    (hfg ▸ f'.comp_apply g r))

Premises used: trans, Ideal.Quotient.mk, Eq.rec, RingHom.comp_apply, RingHom.congr_arg, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
R' : Type u_5
S' : Type u_6
inst_2 : Ring R'
inst_3 : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst_4 : I.IsTwoSided
r : R
⊢ Eq (α := S' ⧸ I) ((Quotient.mk I : (a : S') → S' ⧸ I) ((g' : (a : S) → S') ((f : (a : R) → S) r : S)) : S' ⧸ I)
    ((Quotient.mk I : (a : S') → S' ⧸ I) ((f' : (a : R') → S') ((g : (a : R) → R') r : R')) : S' ⧸ I)

Tactic:
exact (Ideal.Quotient.mk I).congr_arg (_root_.trans (g'.comp_apply f r).symm
    (hfg ▸ f'.comp_apply g r))

Premises used: trans, Ideal.Quotient.mk, RingHom.comp_apply, RingHom.congr_arg, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 : Ring B
inst_8 : Algebra R₁ B
I : Ideal A
J : Ideal B
inst_9 : I.IsTwoSided
inst_10 : J.IsTwoSided
f : A →ₐ[R₁] B
hIJ : I ≤ comap f J
r : R₁
⊢ OneHom.toFun (↑(↑(quotientMap J (↑f : A →+* B) hIJ) : A ⧸ I →* B ⧸ J) : OneHom (A ⧸ I) (B ⧸ J))
      ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) r) =
    (algebraMap R₁ (B ⧸ J) : (a : R₁) → B ⧸ J) r

Tactic:
simp only [RingHom.toFun_eq_coe,
    quotientMap_algebraMap, AlgHom.coe_toRingHom, AlgHom.commutes, Quotient.mk_algebraMap]

Premises used: AlgHom.coe_toRingHom, RingHom.toFun_eq_coe, AlgHom.commutes, Ideal.quotientMap_algebraMap, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 : Ring B
inst_4 : Algebra R₁ B
I : Ideal A
J : Ideal B
inst_5 : I.IsTwoSided
inst_6 : J.IsTwoSided
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ Eq.{u_4 + 1} (α := B ⧸ J)
    (((quotientMapₐ J f H : AlgHom.{u_1, u_3, u_4} R₁ (A ⧸ I) (B ⧸ J)) : (a : A ⧸ I) → B ⧸ J)
        ((Quotient.mk I : (a : A) → A ⧸ I) x) :
      B ⧸ J)
    ((Quotient.mkₐ R₁ J : (a : B) → B ⧸ J) ((f : (a : A) → B) x) : B ⧸ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl