awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h :
  (((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp
          (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp
        (RingHom.id
          (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
        (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)
⊢ ((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp
      (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)) =
    RingHom.comp
      (RingHom.id (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))

Tactic:
apply Ideal.Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h :
  (((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp
          (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp
        (RingHom.id
          (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
        (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)
⊢ (liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J) =
    RingHom.id (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))

Tactic:
repeat apply Ideal.Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
⊢ (((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp
          (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp
        (RingHom.id
          (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
        (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
x : R
⊢ Eq (α := R ⧸ I ⊔ J)
    ((quotQuotEquivQuotSup I J : (a : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → R ⧸ I ⊔ J)
        ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x) :
      R ⧸ I ⊔ J)
    ((Ideal.Quotient.mk (I ⊔ J) : (a : R) → R ⧸ I ⊔ J) x : R ⧸ I ⊔ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
x : R
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
    (((quotQuotEquivQuotSup I J).symm : (a : R ⧸ I ⊔ J) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk (I ⊔ J) : (a : R) → R ⧸ I ⊔ J) x) :
      HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
    ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x :
      HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
x : R
⊢ Eq (α := HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I))
    ((quotQuotEquivComm I J : (a : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)
        ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x) :
      HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I))
    ((quotQuotMk J I : (a : R) → (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I) x :
      HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
⊢ RingHom.comp
      (↑(quotQuotEquivComm I J) : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J →+* (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)
      (quotQuotMk I J) =
    quotQuotMk J I

Tactic:
RingHom.ext <| quotQuotEquivComm_quotQuotMk I J

Premises used: DoubleQuot.quotQuotEquivComm_quotQuotMk, RingHom.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
⊢ (quotQuotEquivComm I J).symm = quotQuotEquivComm J I

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
x : R
h : I ≤ J
⊢ Eq (α := R ⧸ J)
    ((quotQuotEquivQuotOfLE h : (a : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → R ⧸ J)
        ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x) :
      R ⧸ J)
    ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
x : R
h : I ≤ J
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
    (((quotQuotEquivQuotOfLE h).symm : (a : R ⧸ J) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
        ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) x) :
      HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
    ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x :
      HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h : I ≤ J
a :
  ∀ (x : R),
    Eq (α := R ⧸ J)
      ((RingHom.comp (↑(quotQuotEquivQuotOfLE h) : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J →+* R ⧸ J) (quotQuotMk I J) :
            (a : R) → R ⧸ J)
          x :
        R ⧸ J)
      ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) x : R ⧸ J)
⊢ Eq (α := R →+* R ⧸ J)
    (RingHom.comp (↑(quotQuotEquivQuotOfLE h) : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J →+* R ⧸ J) (quotQuotMk I J))
    (Ideal.Quotient.mk J)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h : I ≤ J
x : R
⊢ Eq (α := R ⧸ J)
    ((RingHom.comp (↑(quotQuotEquivQuotOfLE h) : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J →+* R ⧸ J) (quotQuotMk I J) :
          (a : R) → R ⧸ J)
        x :
      R ⧸ J)
    ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h : I ≤ J
a :
  ∀ (x : R),
    Eq (α := HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(quotQuotEquivQuotOfLE h).symm : R ⧸ J →+* (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
              (Ideal.Quotient.mk J) :
            (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
          x :
        HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
      ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x :
        HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(quotQuotEquivQuotOfLE h).symm : R ⧸ J →+* (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) (Ideal.Quotient.mk J) =
    quotQuotMk I J

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h : I ≤ J
x : R
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(quotQuotEquivQuotOfLE h).symm : R ⧸ J →+* (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) (Ideal.Quotient.mk J) :
          (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
        x :
      HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
    ((quotQuotMk I J : (a : R) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) x :
      HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
x : R
⊢ Eq (α := HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I))
    ((quotQuotEquivComm I J : (a : (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)
        ((Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J) :
            (a : R ⧸ I) → (R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
          ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x)) :
      HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I))
    ((algebraMap R
            (HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I)) :
          (a : R) → (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)
        x :
      HasQuotient.Quotient (R ⧸ J) (B := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommRing A
inst_2 : Algebra R A
I J : Ideal A
x : R
⊢ Eq (α := A ⧸ I ⊔ J)
    ((quotQuotEquivQuotSup I J : (a : (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → A ⧸ I ⊔ J)
        ((algebraMap R
              (HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →+* A ⧸ I) (Ideal.Quotient.mk I) J)) :
            (a : R) → (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
          x) :
      A ⧸ I ⊔ J)
    ((algebraMap R (A ⧸ I ⊔ J) : (a : R) → A ⧸ I ⊔ J) x : A ⧸ I ⊔ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : CommRing A
inst_2 : Algebra R A
I J : Ideal A
x : R
⊢ Eq (α := HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I))
    ((quotQuotEquivComm I J : (a : (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → (A ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)
        ((algebraMap R
              (HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →+* A ⧸ I) (Ideal.Quotient.mk I) J)) :
            (a : R) → (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
          x) :
      HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I))
    ((algebraMap R
            (HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)) :
          (a : R) → (A ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)
        x :
      HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, 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
⊢ (↑(quotLeftToQuotSupₐ R I J) : A ⧸ I →+* A ⧸ I ⊔ J) = quotLeftToQuotSup I J

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Ideal.Quotient.factor, Ideal.Quotient.lift, DoubleQuot.quotLeftToQuotSup, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, 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
⊢ Eq (α := (a : A ⧸ I) → A ⧸ I ⊔ J) (⇑(quotLeftToQuotSupₐ R I J) : (a : A ⧸ I) → A ⧸ I ⊔ J)
    (⇑(quotLeftToQuotSup I J) : (a : A ⧸ I) → A ⧸ I ⊔ J)

Tactic:
rfl

Premises used: 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
⊢ (↑(quotQuotToQuotSupₐ R I J) : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J →+* A ⧸ I ⊔ J) = quotQuotToQuotSup I J

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, setOf, Ideal.map, MonoidHomClass.toMonoidHom, DoubleQuot.quotQuotToQuotSup, RingHomClass.toRingHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Quotient.mkₐ, 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
⊢ Eq (α :=
    (a : HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) → A ⧸ I ⊔ J)
    (⇑(quotQuotToQuotSupₐ R I J) : (a : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J) → A ⧸ I ⊔ J)
    (⇑(quotQuotToQuotSup I J) : (a : (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → A ⧸ I ⊔ J)

Tactic:
rfl

Premises used: 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
⊢ (↑(quotQuotMkₐ R I J) : A →+* (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J) = quotQuotMk I J

Tactic:
rfl

Premises used: Ideal.Quotient.mk, Submodule.Quotient.mk, Ideal.map, MonoidHomClass.toMonoidHom, DoubleQuot.quotQuotMk, RingHomClass.toRingHom, Ideal.Quotient.mkₐ, 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
⊢ Eq (α := (a : A) → HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J))
    (⇑(quotQuotMkₐ R I J) : (a : A) → (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)
    (⇑(quotQuotMk I J) : (a : A) → (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
rfl

Premises used: 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
⊢ (↑(liftSupQuotQuotMkₐ R I J) : A ⧸ I ⊔ J →+* (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J) = liftSupQuotQuotMk I J

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, Ideal.map, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, DoubleQuot.liftSupQuotQuotMk, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Quotient.mkₐ, 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
⊢ Eq (α :=
    (a : A ⧸ I ⊔ J) → HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J))
    (⇑(liftSupQuotQuotMkₐ R I J) : (a : A ⧸ I ⊔ J) → (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)
    (⇑(liftSupQuotQuotMk I J) : (a : A ⧸ I ⊔ J) → (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
rfl

Premises used: 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
⊢ AlgEquiv.toRingEquiv (quotQuotEquivQuotSupₐ R I J) = quotQuotEquivQuotSup I J

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, setOf, Ideal.map, RingEquiv.ofRingHom, DoubleQuot.quotQuotEquivQuotSup, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Quotient.mkₐ, 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
⊢ Eq (α :=
    (a : HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) → A ⧸ I ⊔ J)
    (⇑(quotQuotEquivQuotSupₐ R I J) : (a : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J) → A ⧸ I ⊔ J)
    (⇑(quotQuotEquivQuotSup I J) : (a : (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → A ⧸ I ⊔ J)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, setOf, Ideal.map, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Quotient.mkₐ, 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
⊢ AlgEquiv.toRingEquiv (AlgEquiv.symm (quotQuotEquivQuotSupₐ R I J)) = (quotQuotEquivQuotSup I J).symm

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, setOf, Ideal.map, Submodule.quotientRel, AddAction.orbitRel, Equiv.symm, AddCon.Quotient, Ideal.Quotient.mkₐ, RingEquiv.symm, 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
⊢ Eq (α :=
    (a : A ⧸ I ⊔ J) → HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J))
    (⇑(AlgEquiv.symm (quotQuotEquivQuotSupₐ R I J)) : (a : A ⧸ I ⊔ J) → (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)
    (⇑(quotQuotEquivQuotSup I J).symm : (a : A ⧸ I ⊔ J) → (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, setOf, Ideal.map, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Quotient.mkₐ, 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
⊢ AlgEquiv.toRingEquiv (quotQuotEquivCommₐ R I J) = quotQuotEquivComm I J

Tactic:
rfl

Premises used: Quotient.liftOn', Equiv.trans, Ideal.Quotient.mk, AddCon.liftOn, Ideal.map, RingEquiv.trans, DoubleQuot.quotQuotEquivComm, Ideal.Quotient.mkₐ, 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
⊢ Eq (α :=
    (a : HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) →
      HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →ₐ[R] A ⧸ J) (Quotient.mkₐ R J) I))
    (⇑(quotQuotEquivCommₐ R I J) : (a : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J) → (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)
    (⇑(quotQuotEquivComm I J) : (a : (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → (A ⧸ J) ⧸ map (Ideal.Quotient.mk J) I)

Tactic:
rfl

Premises used: Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Ideal.map, Ideal.Quotient.mkₐ, 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
⊢ Eq (α :=
    HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →ₐ[R] A ⧸ J) (Quotient.mkₐ R J) I) ≃ₐ[R]
      HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J))
    (AlgEquiv.symm (quotQuotEquivCommₐ R I J)) (quotQuotEquivCommₐ R J I)

Tactic:
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
⊢ Eq (α := A →ₐ[R] HasQuotient.Quotient (A ⧸ J) (B := Ideal (A ⧸ J)) (map (F := A →ₐ[R] A ⧸ J) (Quotient.mkₐ R J) I))
    (AlgHom.comp
      (↑(quotQuotEquivCommₐ R I J) : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J →ₐ[R] (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)
      (quotQuotMkₐ R I J))
    (quotQuotMkₐ R J I)

Tactic:
AlgHom.ext <| quotQuotEquivComm_quotQuotMk I J

Premises used: DoubleQuot.quotQuotEquivComm_quotQuotMk, AlgHom.ext
-- 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
⊢ AlgEquiv.toRingEquiv (quotQuotEquivQuotOfLEₐ R h) = quotQuotEquivQuotOfLE h

Tactic:
rfl

Premises used: Quotient.liftOn', Equiv.trans, Ideal.Quotient.mk, AddCon.liftOn, Ideal.map, DoubleQuot.quotQuotEquivQuotOfLE, Quot.map, RingEquiv.trans, Ideal.Quotient.mkₐ, 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
⊢ Eq (α :=
    (a : HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J)) → A ⧸ J)
    (⇑(quotQuotEquivQuotOfLEₐ R h) : (a : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J) → A ⧸ J)
    (⇑(quotQuotEquivQuotOfLE h) : (a : (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J) → A ⧸ J)

Tactic:
rfl

Premises used: Ideal.Quotient.mk, Ideal.map, Quot.map, Ideal.Quotient.mkₐ, 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
⊢ AlgEquiv.toRingEquiv (AlgEquiv.symm (quotQuotEquivQuotOfLEₐ R h)) = (quotQuotEquivQuotOfLE h).symm

Tactic:
rfl

Premises used: Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Ideal.map, Quot.map, Equiv.symm, Ideal.Quotient.mkₐ, RingEquiv.symm, 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
⊢ Eq (α :=
    (a : A ⧸ J) → HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J))
    (⇑(AlgEquiv.symm (quotQuotEquivQuotOfLEₐ R h)) : (a : A ⧸ J) → (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)
    (⇑(quotQuotEquivQuotOfLE h).symm : (a : A ⧸ J) → (A ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
rfl

Premises used: Quotient.liftOn', Equiv.trans, Ideal.Quotient.mk, AddCon.liftOn, Ideal.map, Quot.map, Ideal.Quotient.mkₐ, 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
⊢ Eq (α := A →ₐ[R] A ⧸ J)
    (AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h) : (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J →ₐ[R] A ⧸ J) (quotQuotMkₐ R I J))
    (Quotient.mkₐ R J)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, AlgHom.comp, Ideal.Quotient.mkₐ, 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
⊢ Eq (α := A →ₐ[R] HasQuotient.Quotient (A ⧸ I) (B := Ideal (A ⧸ I)) (map (F := A →ₐ[R] A ⧸ I) (Quotient.mkₐ R I) J))
    (AlgHom.comp (↑(AlgEquiv.symm (quotQuotEquivQuotOfLEₐ R h)) : A ⧸ J →ₐ[R] (A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)
      (Quotient.mkₐ R J))
    (quotQuotMkₐ R I J)

Tactic:
rfl

Premises used: AddAction.orbit, DoubleQuot.quotQuotMkₐ, Quotient.liftOn', Set.Mem, Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, setOf, Ideal.map, DoubleQuot.quotQuotMk, Quotient, Set.preimage, Submodule.quotientRel, Set.range, AddAction.orbitRel, AlgHom.comp, Ideal.Quotient.mkₐ, 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
H :
  ∀ (x : A ⧸ I),
    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)
⊢ Eq (α := A ⧸ I →ₐ[R] 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)))
    (Quotient.factorₐ R h)

Tactic:
ext x