awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
suffices : Function.Surjective (β := RingQuot s) fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)
⊢ Function.Surjective (α := A) (β := RingQuot s) (⇑(mkAlgHom S s) : (a : A) → RingQuot s)

Tactic:
suffices Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s) by
    simpa [mkAlgHom_def, mkRingHom_def]
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
toQuot : Quot (Rel s)
a w : A
h : (fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)) a = mk (r := s) (Quot.mk (Rel s) a)
⊢ ∃ (a_1 : A), (fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)) a_1 = mk (r := s) (Quot.mk (Rel s) a)

Tactic:
use a
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
H : ∀ (x : RingQuot s), Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) x : B) ((g : (a : RingQuot s) → B) x : B)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : RingQuot s
H :
  ∀ (x : A),
    Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)
      ((g : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) x : B) ((g : (a : RingQuot s) → B) x : B)

Tactic:
rcases mkAlgHom_surjective S s x with ⟨x, rfl⟩

Premises used: RingQuot.mkAlgHom_surjective, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : A
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)
    ((g : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)

Tactic:
AlgHom.congr_fun w x

Premises used: AlgHom.congr_fun
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : A
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)
    ((g : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)

Tactic:
exact AlgHom.congr_fun w x

Premises used: AlgHom.congr_fun
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b x_1 y : A
r : s x_1 y
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x_1 : B) ((f : (a : A) → B) y : B)

Tactic:
h r
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b x_1 y : A
r : s x_1 y
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x_1 : B) ((f : (a : A) → B) y : B)

Tactic:
exact h r
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b a_1 b_1 c : A
h_1 : Rel s a_1 b_1
r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a_1 : B) ((f : (a : A) → B) b_1 : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a_1 + c) : B) ((f : (a : A) → B) (b_1 + c) : B)

Tactic:
simp only [map_add, r']

Premises used: map_add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b a_1 b_1 c : A
h_1 : Rel s a_1 b_1
r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a_1 : B) ((f : (a : A) → B) b_1 : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a_1 * c) : B) ((f : (a : A) → B) (b_1 * c) : B)

Tactic:
simp only [map_mul, r']

Premises used: map_mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b a_1 b_1 c : A
h_1 : Rel s b_1 c
r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) b_1 : B) ((f : (a : A) → B) c : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a_1 * b_1) : B) ((f : (a : A) → B) (a_1 * c) : B)

Tactic:
simp only [map_mul, r']

Premises used: map_mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b : A
r : Rel s a b
of : ∀ ⦃x y : A⦄ (r : s x y), Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
add_left :
  ∀ ⦃a b c : A⦄,
    Rel s a b →
      ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
        Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a + c) : B) ((f : (a : A) → B) (b + c) : B)
mul_left :
  ∀ ⦃a b c : A⦄,
    Rel s a b →
      ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
        Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a * c) : B) ((f : (a : A) → B) (b * c) : B)
mul_right :
  ∀ ⦃a b c : A⦄,
    Rel s b c →
      ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) b : B) ((f : (a : A) → B) c : B)),
        Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a * b) : B) ((f : (a : A) → B) (a * c) : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)

Tactic:
induction r with
              | of r => exact h r
              | add_left _ r' => simp only [map_add, r']
              | mul_left _ r' => simp only [map_mul, r']
              | mul_right _ r' => simp only [map_mul, r']

Premises used: map_add, map_mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ (toQuot (r := s) 1) = 1

Tactic:
simp only [← one_quot, map_one]

Premises used: map_one, RingQuot.one_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
toQuot : Quot (Rel s)
x : A
toQuot_1 : Quot (Rel s)
y : A
⊢ Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯
      ((mk (r := s) (Quot.mk (Rel s) x) * mk (r := s) (Quot.mk (Rel s) y)).toQuot (r := s)) =
    Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ ((mk (r := s) (Quot.mk (Rel s) x)).toQuot (r := s)) *
      Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ ((mk (r := s) (Quot.mk (Rel s) y)).toQuot (r := s))

Tactic:
simp only [mul_quot, map_mul _ x y]

Premises used: RingQuot.mul_quot, map_mul
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ (toQuot (r := s) 0) = 0

Tactic:
simp only [← zero_quot, map_zero]

Premises used: map_zero, RingQuot.zero_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
toQuot : Quot (Rel s)
x : A
toQuot_1 : Quot (Rel s)
y : A
⊢ Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯
      ((mk (r := s) (Quot.mk (Rel s) x) + mk (r := s) (Quot.mk (Rel s) y)).toQuot (r := s)) =
    Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ ((mk (r := s) (Quot.mk (Rel s) x)).toQuot (r := s)) +
      Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ ((mk (r := s) (Quot.mk (Rel s) y)).toQuot (r := s))

Tactic:
simp only [add_quot, map_add _ x y]

Premises used: RingQuot.add_quot, map_add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : S
⊢ Quot.lift (r := Rel s) (⇑f : (a : A) → B) ⋯ (toQuot (r := s) ((algebraMap S (RingQuot s) : (a : S) → RingQuot s) x)) =
    (algebraMap S B : (a : S) → B) x

Tactic:
simp [← one_quot, smul_quot, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, RingQuot.smul_quot, RingQuot.one_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }
a :
  ∀ (x : A),
    Eq.{u₄ + 1} (α := B)
      (((↑((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                    (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                        ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                        (F.comp (mkAlgHom S s)) ⋯ :
                      { f : A →ₐ[S] B //
                        ∀ ⦃x y : A⦄,
                          s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
                  ((fun
                        (f' :
                          { f : A →ₐ[S] B //
                            ∀ ⦃x y : A⦄,
                              s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                      preLiftAlgHom S (s := s) ⋯)
                    f)) :
              A →ₐ[S] B) :
            (a : A) → B)
          x :
        B)
      (((↑f : A →ₐ[S] B) : (a : A) → B) x : B)
⊢ (fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
        (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
            ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
            (F.comp (mkAlgHom S s)) ⋯ :
          { f : A →ₐ[S] B //
            ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
      ((fun
            (f' :
              { f : A →ₐ[S] B //
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
          preLiftAlgHom S (s := s) ⋯)
        f) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }
x : A
⊢ Eq.{u₄ + 1} (α := B)
    (((↑((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                  (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                      (F.comp (mkAlgHom S s)) ⋯ :
                    { f : A →ₐ[S] B //
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
                ((fun
                      (f' :
                        { f : A →ₐ[S] B //
                          ∀ ⦃x y : A⦄,
                            s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                    preLiftAlgHom S (s := s) ⋯)
                  f)) :
            A →ₐ[S] B) :
          (a : A) → B)
        x :
      B)
    (((↑f : A →ₐ[S] B) : (a : A) → B) x : B)

Tactic:
simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def,
        AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        Function.comp_apply]

Premises used: AlgHom.coe_mk, OneHom.coe_mk, RingQuot.mkRingHom_def, RingQuot.mkAlgHom_def, AlgHom.coe_comp, MonoidHom.coe_mk, RingHom.coe_mk, Function.comp_apply, RingQuot.preLiftAlgHom_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
F : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w :
  ∀ (x : A),
    Eq.{u₄ + 1} (α := B)
      ((AlgHom.comp
              ((fun
                    (f' :
                      { f : A →ₐ[S] B //
                        ∀ ⦃x y : A⦄,
                          s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                  preLiftAlgHom S (s := s) ⋯)
                ((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                    (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                        ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                        (F.comp (mkAlgHom S s)) ⋯ :
                      { f : A →ₐ[S] B //
                        ∀ ⦃x y : A⦄,
                          s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
                  F))
              (mkAlgHom S s) :
            (a : A) → B)
          x :
        B)
      ((F.comp (mkAlgHom S s) : (a : A) → B) x : B)
⊢ (fun
          (f' :
            { f : A →ₐ[S] B //
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
        preLiftAlgHom S (s := s) ⋯)
      ((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
          (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
              (F.comp (mkAlgHom S s)) ⋯ :
            { f : A →ₐ[S] B //
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
        F) =
    F

Tactic:
ext
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
F : AlgHom.{uS, uA, u₄} S (RingQuot s) B
x : A
⊢ Eq.{u₄ + 1} (α := B)
    ((AlgHom.comp
            ((fun
                  (f' :
                    { f : A →ₐ[S] B //
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                preLiftAlgHom S (s := s) ⋯)
              ((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                  (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                      (F.comp (mkAlgHom S s)) ⋯ :
                    { f : A →ₐ[S] B //
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
                F))
            (mkAlgHom S s) :
          (a : A) → B)
        x :
      B)
    ((F.comp (mkAlgHom S s) : (a : A) → B) x : B)

Tactic:
simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def,
                 AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk,
                 MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]

Premises used: AlgHom.coe_mk, OneHom.coe_mk, RingQuot.mkRingHom_def, RingQuot.mkAlgHom_def, AlgHom.coe_comp, MonoidHom.coe_mk, RingHom.coe_mk, Function.comp_apply, RingQuot.preLiftAlgHom_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : A
simp_rw :
  Eq.{u₄ + 1} (α := B)
    (((({
                  toFun :=
                    fun
                      (f' :
                        { f : A →ₐ[S] B //
                          ∀ ⦃x y : A⦄,
                            s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                    {
                      toFun := fun (x : RingQuot s) ↦
                        Quot.lift (r := Rel s) (⇑(↑f' : A →ₐ[S] B) : (a : A) → B) ⋯ (x.toQuot (r := s)),
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ },
                  invFun := fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                    Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                      (F.comp
                        { toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯,
                          map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ })
                      ⋯,
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                  RingQuot s →ₐ[S] B)
              (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w) :
            AlgHom.{uS, uA, u₄} S (RingQuot s) B) :
          (a : RingQuot s) → B)
        (({ toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯, commutes' := ⋯ } :
              (a : A) → RingQuot s)
            x :
          RingQuot s) :
      B)
    ((f : (a : A) → B) x : B)
⊢ Eq.{u₄ + 1} (α := B)
    ((((liftAlgHom S (s := s) :
                (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                  RingQuot s →ₐ[S] B)
              (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w) :
            AlgHom.{uS, uA, u₄} S (RingQuot s) B) :
          (a : RingQuot s) → B)
        ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]

Premises used: RingQuot.mkRingHom_def, RingQuot.mkAlgHom_def, RingQuot.liftAlgHom_def, RingQuot.preLiftAlgHom_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : A
⊢ Eq.{u₄ + 1} (α := B)
    (((({
                  toFun :=
                    fun
                      (f' :
                        { f : A →ₐ[S] B //
                          ∀ ⦃x y : A⦄,
                            s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                    {
                      toFun := fun (x : RingQuot s) ↦
                        Quot.lift (r := Rel s) (⇑(↑f' : A →ₐ[S] B) : (a : A) → B) ⋯ (x.toQuot (r := s)),
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ },
                  invFun := fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                    Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                      (F.comp
                        { toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯,
                          map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ })
                      ⋯,
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                  RingQuot s →ₐ[S] B)
              (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w) :
            AlgHom.{uS, uA, u₄} S (RingQuot s) B) :
          (a : RingQuot s) → B)
        (({ toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯, commutes' := ⋯ } :
              (a : A) → RingQuot s)
            x :
          RingQuot s) :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl