R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ ↑lift (↑lift.symm f) =
    ↑lift
      { val := RingHom.comp f (mkRingHom r),
        property := (_ : ∀ (x y : R), r x y → ↑f (↑(mkRingHom r) x) = ↑f (↑(mkRingHom r) y)) }
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ f =
    ↑lift
      { val := RingHom.comp f (mkRingHom r),
        property := (_ : ∀ (x y : R), r x y → ↑f (↑(mkRingHom r) x) = ↑f (↑(mkRingHom r) y)) }
conv_lhs => rw [← lift.apply_symm_apply f]
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ ↑{ toFun := fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y),
          invFun := fun F =>
            { val := RingHom.comp F (mkRingHom r),
              property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) },
          left_inv :=
            (_ :
              ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }),
                (fun F =>
                      { val := RingHom.comp F (mkRingHom r),
                        property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                    ((fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) =
                  f),
          right_inv :=
            (_ :
              ∀ (F : RingQuot r →+* T),
                (fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y))
                    ((fun F =>
                        { val := RingHom.comp F (mkRingHom r),
                          property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                      F) =
                  F) }
      (↑{ toFun := fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y),
              invFun := fun F =>
                { val := RingHom.comp F (mkRingHom r),
                  property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) },
              left_inv :=
                (_ :
                  ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }),
                    (fun F =>
                          { val := RingHom.comp F (mkRingHom r),
                            property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                        ((fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) =
                      f),
              right_inv :=
                (_ :
                  ∀ (F : RingQuot r →+* T),
                    (fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y))
                        ((fun F =>
                            { val := RingHom.comp F (mkRingHom r),
                              property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                          F) =
                      F) }.symm
        f) =
    ↑{ toFun := fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y),
          invFun := fun F =>
            { val := RingHom.comp F (mkRingHom r),
              property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) },
          left_inv :=
            (_ :
              ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }),
                (fun F =>
                      { val := RingHom.comp F (mkRingHom r),
                        property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                    ((fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) =
                  f),
          right_inv :=
            (_ :
              ∀ (F : RingQuot r →+* T),
                (fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y))
                    ((fun F =>
                        { val := RingHom.comp F (mkRingHom r),
                          property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                      F) =
                  F) }
      { val := RingHom.comp f (mkRingHom r),
        property := (_ : ∀ (x y : R), r x y → ↑f (↑(mkRingHom r) x) = ↑f (↑(mkRingHom r) y)) }
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ ↑lift (↑lift.symm f) =
    ↑lift
      { val := RingHom.comp f (mkRingHom r),
        property := (_ : ∀ (x y : R), r x y → ↑f (↑(mkRingHom r) x) = ↑f (↑(mkRingHom r) y)) }
rw [lift_def]
no goals
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ ↑{ toFun := fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y),
          invFun := fun F =>
            { val := RingHom.comp F (mkRingHom r),
              property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) },
          left_inv :=
            (_ :
              ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }),
                (fun F =>
                      { val := RingHom.comp F (mkRingHom r),
                        property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                    ((fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) =
                  f),
          right_inv :=
            (_ :
              ∀ (F : RingQuot r →+* T),
                (fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y))
                    ((fun F =>
                        { val := RingHom.comp F (mkRingHom r),
                          property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                      F) =
                  F) }
      (↑{ toFun := fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y),
              invFun := fun F =>
                { val := RingHom.comp F (mkRingHom r),
                  property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) },
              left_inv :=
                (_ :
                  ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }),
                    (fun F =>
                          { val := RingHom.comp F (mkRingHom r),
                            property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                        ((fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) =
                      f),
              right_inv :=
                (_ :
                  ∀ (F : RingQuot r →+* T),
                    (fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y))
                        ((fun F =>
                            { val := RingHom.comp F (mkRingHom r),
                              property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                          F) =
                      F) }.symm
        f) =
    ↑{ toFun := fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y),
          invFun := fun F =>
            { val := RingHom.comp F (mkRingHom r),
              property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) },
          left_inv :=
            (_ :
              ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }),
                (fun F =>
                      { val := RingHom.comp F (mkRingHom r),
                        property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                    ((fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) =
                  f),
          right_inv :=
            (_ :
              ∀ (F : RingQuot r →+* T),
                (fun f => preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y))
                    ((fun F =>
                        { val := RingHom.comp F (mkRingHom r),
                          property := (_ : ∀ (x y : R), r x y → ↑F (↑(mkRingHom r) x) = ↑F (↑(mkRingHom r) y)) })
                      F) =
                  F) }
      { val := RingHom.comp f (mkRingHom r),
        property := (_ : ∀ (x y : R), r x y → ↑f (↑(mkRingHom r) x) = ↑f (↑(mkRingHom r) y)) }
rfl