awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.RingQuot
Goal:
R_1 : Type uR
inst : Semiring R_1
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_1 → R_1 → Prop
R : Type uR
inst_4 : CommSemiring R
r : R → R → Prop
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
⊢ mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) a_1) =
    mk (r := r) (Quot.mk (Rel r) a_1) * mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp [mul_quot, mul_comm]

Premises used: RingQuot.mul_quot, mul_comm
-- 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 : Algebra S R
r : R → R → Prop
⊢ mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) 1)) = 1

Tactic:
simp [← one_quot]

Premises used: 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_1 : R → R → Prop
inst_4 : Algebra S R
r : R → R → Prop
⊢ ∀ (x y : S),
    mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) (x * y))) =
      mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) x)) *
        mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) y))

Tactic:
simp [mul_quot]

Premises used: RingQuot.mul_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_1 : R → R → Prop
inst_4 : Algebra S R
r : R → R → Prop
⊢ mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) 0)) = 0

Tactic:
simp [← zero_quot]

Premises used: 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_1 : R → R → Prop
inst_4 : Algebra S R
r : R → R → Prop
⊢ ∀ (x y : S),
    mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) (x + y))) =
      mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) x)) +
        mk (r := r) (Quot.mk (Rel r) ((algebraMap S R : (a : S) → R) y))

Tactic:
simp [add_quot]

Premises used: RingQuot.add_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_1 : R → R → Prop
inst_4 : Algebra S R
r_2 : R → R → Prop
r : S
toQuot : Quot (Rel r_2)
a : R
⊢ HMul.hMul (α := RingQuot r_2)
      (({ toFun := fun (r : S) ↦ mk (r := r_2) (Quot.mk (Rel r_2) ((algebraMap S R : (a : S) → R) r)), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : RingHom.{uS, uR} S (RingQuot r_2) } :
            (a : S) → RingQuot r_2)
          r :
        RingQuot r_2)
      (mk (r := r_2) (Quot.mk (Rel r_2) a)) =
    HMul.hMul (β := RingQuot r_2) (mk (r := r_2) (Quot.mk (Rel r_2) a))
      (({ toFun := fun (r : S) ↦ mk (r := r_2) (Quot.mk (Rel r_2) ((algebraMap S R : (a : S) → R) r)), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : S) → RingQuot r_2)
          r :
        RingQuot r_2)

Tactic:
simp [Algebra.commutes, mul_quot]

Premises used: RingQuot.mul_quot, Algebra.commutes
-- 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 : Algebra S R
r_2 : R → R → Prop
r : S
toQuot : Quot (Rel r_2)
a : R
⊢ r • mk (r := r_2) (Quot.mk (Rel r_2) a) =
    HMul.hMul (α := RingQuot r_2)
      (({ toFun := fun (r : S) ↦ mk (r := r_2) (Quot.mk (Rel r_2) ((algebraMap S R : (a : S) → R) r)), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : S) → RingQuot r_2)
          r :
        RingQuot r_2)
      (mk (r := r_2) (Quot.mk (Rel r_2) a))

Tactic:
simp [smul_quot, Algebra.smul_def, mul_quot]

Premises used: RingQuot.mul_quot, RingQuot.smul_quot, Algebra.smul_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_1 r : R → R → Prop
⊢ mk (r := r) (Quot.mk (Rel r) 1) = 1

Tactic:
simp [← one_quot]

Premises used: 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_1 r : R → R → Prop
⊢ ∀ (x y : R), mk (r := r) (Quot.mk (Rel r) (x * y)) = mk (r := r) (Quot.mk (Rel r) x) * mk (r := r) (Quot.mk (Rel r) y)

Tactic:
simp [mul_quot]

Premises used: RingQuot.mul_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_1 r : R → R → Prop
⊢ mk (r := r) (Quot.mk (Rel r) 0) = 0

Tactic:
simp [← zero_quot]

Premises used: 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_1 r : R → R → Prop
⊢ ∀ (x y : R), mk (r := r) (Quot.mk (Rel r) (x + y)) = mk (r := r) (Quot.mk (Rel r) x) + mk (r := r) (Quot.mk (Rel r) y)

Tactic:
simp [add_quot]

Premises used: RingQuot.add_quot
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x y : R
w : r x y
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r)
    ((mkRingHom r : (a : R) → RingQuot r) y : RingQuot r)

Tactic:
simp [mkRingHom_def, Quot.sound (Rel.of w)]

Premises used: Quot.sound, RingQuot.mkRingHom_def, RingQuot.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
simp : Function.Surjective (β := RingQuot r) fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x)
⊢ Function.Surjective (α := R) (β := RingQuot r) (⇑(mkRingHom r) : (a : R) → RingQuot r)

Tactic:
simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: OneHom.coe_mk, RingQuot.mkRingHom_def, MonoidHom.coe_mk, RingHom.coe_mk
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
toQuot : Quot (Rel r)
a : R
⊢ ∃ (a_1 : R), (fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x)) a_1 = mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : NonAssocSemiring T
r : R → R → Prop
f g : RingHom.{uR, uT} (RingQuot r) T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
a : ∀ (x : RingQuot r), Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) x : T) ((g : (a : RingQuot r) → T) x : T)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : NonAssocSemiring T
r : R → R → Prop
f g : RingHom.{uR, uT} (RingQuot r) T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : RingQuot r
a :
  ∀ (x : R),
    Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) : T)
      ((g : (a : RingQuot r) → T) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) : T)
⊢ Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) x : T) ((g : (a : RingQuot r) → T) x : T)

Tactic:
rcases mkRingHom_surjective r x with ⟨x, rfl⟩

Premises used: RingQuot.mkRingHom_surjective, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : NonAssocSemiring T
r : R → R → Prop
f g : RingHom.{uR, uT} (RingQuot r) T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : R
⊢ Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) : T)
    ((g : (a : RingQuot r) → T) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) : T)

Tactic:
(RingHom.congr_fun w x :)

Premises used: RingHom.congr_fun
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : NonAssocSemiring T
r : R → R → Prop
f g : RingHom.{uR, uT} (RingQuot r) T
w : f.comp (mkRingHom r) = g.comp (mkRingHom r)
x : R
⊢ Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) : T)
    ((g : (a : RingQuot r) → T) ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) : T)

Tactic:
exact (RingHom.congr_fun w x :)

Premises used: RingHom.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
r_2 : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r_2 x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : RingQuot r_2
a b x_1 y : R
r : r_2 x_1 y
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) x_1 : T) ((f : (a : R) → T) y : T)

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
r_2 : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r_2 x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : RingQuot r_2
a b x_1 y : R
r : r_2 x_1 y
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) x_1 : T) ((f : (a : R) → T) y : T)

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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : RingQuot r
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
r' : Eq.{uT + 1} (α := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) b_1 : T)
add_left :
  HAdd.hAdd (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T) = (f : (a : R) → T) (b_1 + c)
add_left₁ :
  HAdd.hAdd (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T) =
    HAdd.hAdd (α := T) (β := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T)
add_left₂ add_left₃ :
  HAdd.hAdd (α := T) (β := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T) =
    HAdd.hAdd (α := T) (β := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 + c) : T) ((f : (a : R) → T) (b_1 + c) : T)

Tactic:
rw [map_add, 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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : RingQuot r
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
r' : Eq.{uT + 1} (α := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) b_1 : T)
mul_left :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T) = (f : (a : R) → T) (b_1 * c)
mul_left₁ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T)
mul_left₂ mul_left₃ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * c) : T) ((f : (a : R) → T) (b_1 * c) : T)

Tactic:
rw [map_mul, 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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : RingQuot r
a b a_1 b_1 c : R
h_1 : Rel r b_1 c
r' : Eq.{uT + 1} (α := T) ((f : (a : R) → T) b_1 : T) ((f : (a : R) → T) c : T)
mul_right :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) b_1 : T) = (f : (a : R) → T) (a_1 * c)
mul_right₁ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) b_1 : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T)
mul_right₂ mul_right₃ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T) =
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) a_1 : T) ((f : (a : R) → T) c : T)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * b_1) : T) ((f : (a : R) → T) (a_1 * c) : T)

Tactic:
rw [map_mul, 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
r_2 : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r_2 x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : RingQuot r_2
a b : R
r : Rel r_2 a b
of : ∀ ⦃x y : R⦄ (r : r_2 x y), Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
add_left :
  ∀ ⦃a b c : R⦄,
    Rel r_2 a b →
      ∀ (r' : Eq.{uT + 1} (α := T) ((f : (a : R) → T) a : T) ((f : (a : R) → T) b : T)),
        Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a + c) : T) ((f : (a : R) → T) (b + c) : T)
mul_left :
  ∀ ⦃a b c : R⦄,
    Rel r_2 a b →
      ∀ (r' : Eq.{uT + 1} (α := T) ((f : (a : R) → T) a : T) ((f : (a : R) → T) b : T)),
        Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a * c) : T) ((f : (a : R) → T) (b * c) : T)
mul_right :
  ∀ ⦃a b c : R⦄,
    Rel r_2 b c →
      ∀ (r' : Eq.{uT + 1} (α := T) ((f : (a : R) → T) b : T) ((f : (a : R) → T) c : T)),
        Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a * b) : T) ((f : (a : R) → T) (a * c) : T)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) a : T) ((f : (a : R) → T) b : T)

Tactic:
induction r with
          | of r => exact h r
          | add_left _ r' => rw [map_add, map_add, r']
          | mul_left _ r' => rw [map_mul, map_mul, r']
          | mul_right _ r' => rw [map_mul, 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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
⊢ Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯ (toQuot (r := r) 1) = 1

Tactic:
simp only [← one_quot, f.map_one]

Premises used: RingHom.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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
toQuot : Quot (Rel r)
x : R
toQuot_1 : Quot (Rel r)
y : R
⊢ Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯
      ((mk (r := r) (Quot.mk (Rel r) x) * mk (r := r) (Quot.mk (Rel r) y)).toQuot (r := r)) =
    Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯ ((mk (r := r) (Quot.mk (Rel r) x)).toQuot (r := r)) *
      Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯ ((mk (r := r) (Quot.mk (Rel r) y)).toQuot (r := r))

Tactic:
simp only [mul_quot, f.map_mul x y]

Premises used: RingQuot.mul_quot, RingHom.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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
⊢ Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯ (toQuot (r := r) 0) = 0

Tactic:
simp only [← zero_quot, f.map_zero]

Premises used: RingHom.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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
toQuot : Quot (Rel r)
x : R
toQuot_1 : Quot (Rel r)
y : R
⊢ Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯
      ((mk (r := r) (Quot.mk (Rel r) x) + mk (r := r) (Quot.mk (Rel r) y)).toQuot (r := r)) =
    Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯ ((mk (r := r) (Quot.mk (Rel r) x)).toQuot (r := r)) +
      Quot.lift (r := Rel r) (⇑f : (a : R) → T) ⋯ ((mk (r := r) (Quot.mk (Rel r) y)).toQuot (r := r))

Tactic:
simp only [add_quot, f.map_add x y]

Premises used: RingQuot.add_quot, RingHom.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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }
a :
  ∀ (x : R),
    Eq.{uT + 1} (α := T)
      (((↑((fun (F : RingHom.{uR, uT} (RingQuot r) T) ↦
                    (Subtype.mk (p := fun (f : R →+* T) ↦
                        ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
                        (F.comp (mkRingHom r)) ⋯ :
                      { f : R →+* T //
                        ∀ ⦃x y : R⦄,
                          r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }))
                  ((fun
                        (f :
                          { f : R →+* T //
                            ∀ ⦃x y : R⦄,
                              r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }) ↦
                      preLift (r := r) ⋯)
                    f)) :
              R →+* T) :
            (a : R) → T)
          x :
        T)
      (((↑f : R →+* T) : (a : R) → T) x : T)
⊢ (fun (F : RingHom.{uR, uT} (RingQuot r) T) ↦
        (Subtype.mk (p := fun (f : R →+* T) ↦
            ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
            (F.comp (mkRingHom r)) ⋯ :
          { f : R →+* T //
            ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }))
      ((fun
            (f :
              { f : R →+* T //
                ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }) ↦
          preLift (r := r) ⋯)
        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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
f : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }
x : R
⊢ Eq.{uT + 1} (α := T)
    (((↑((fun (F : RingHom.{uR, uT} (RingQuot r) T) ↦
                  (Subtype.mk (p := fun (f : R →+* T) ↦
                      ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
                      (F.comp (mkRingHom r)) ⋯ :
                    { f : R →+* T //
                      ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }))
                ((fun
                      (f :
                        { f : R →+* T //
                          ∀ ⦃x y : R⦄,
                            r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }) ↦
                    preLift (r := r) ⋯)
                  f)) :
            R →+* T) :
          (a : R) → T)
        x :
      T)
    (((↑f : R →+* T) : (a : R) → T) x : T)

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

Premises used: OneHom.coe_mk, RingQuot.preLift_def, RingQuot.mkRingHom_def, MonoidHom.coe_mk, RingHom.coe_mk, RingHom.coe_comp, Function.comp_apply
-- 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
r : R → R → Prop
F : RingHom.{uR, uT} (RingQuot r) T
simp :
  {
      toFun := fun (x : RingQuot r) ↦
        Quot.lift (r := Rel r) (⇑(F.comp (mkRingHom r)) : (a : R) → T) ⋯ (x.toQuot (r := r)),
      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } =
    F
⊢ (fun
          (f :
            { f : R →+* T //
              ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }) ↦
        preLift (r := r) ⋯)
      ((fun (F : RingHom.{uR, uT} (RingQuot r) T) ↦
          (Subtype.mk (p := fun (f : R →+* T) ↦
              ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
              (F.comp (mkRingHom r)) ⋯ :
            { f : R →+* T //
              ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }))
        F) =
    F

Tactic:
simp only [preLift_def]

Premises used: RingQuot.preLift_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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
F : RingHom.{uR, uT} (RingQuot r) T
w :
  ∀ (x : R),
    Eq.{uT + 1} (α := T)
      ((RingHom.comp
              {
                toFun := fun (x : RingQuot r) ↦
                  Quot.lift (r := Rel r) (⇑(F.comp (mkRingHom r)) : (a : R) → T) ⋯ (x.toQuot (r := r)),
                map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
              (mkRingHom r) :
            (a : R) → T)
          x :
        T)
      ((F.comp (mkRingHom r) : (a : R) → T) x : T)
⊢ {
      toFun := fun (x : RingQuot r) ↦
        Quot.lift (r := Rel r) (⇑(F.comp (mkRingHom r)) : (a : R) → T) ⋯ (x.toQuot (r := r)),
      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } =
    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_1 : R → R → Prop
inst_4 : Semiring T
r : R → R → Prop
F : RingHom.{uR, uT} (RingQuot r) T
x : R
⊢ Eq.{uT + 1} (α := T)
    ((RingHom.comp
            {
              toFun := fun (x : RingQuot r) ↦
                Quot.lift (r := Rel r) (⇑(F.comp (mkRingHom r)) : (a : R) → T) ⋯ (x.toQuot (r := r)),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
            (mkRingHom r) :
          (a : R) → T)
        x :
      T)
    ((F.comp (mkRingHom r) : (a : R) → T) x : T)

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

Premises used: OneHom.coe_mk, RingQuot.mkRingHom_def, MonoidHom.coe_mk, RingHom.coe_mk, RingHom.coe_comp, Function.comp_apply