awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
h₁ : ∀ (x y : R), r x y → Relation.EqvGen (Rel r) x y
h₂ : ∀ (x : R), Relation.EqvGen (Rel r) x x
h₃ : ∀ {x y : R}, RingConGen.Rel r x y → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y x
⊢ Relation.EqvGen (Rel r) x₁ x₂
have h₄ : ∀ {x y z : R},
  RingConGen.Rel r x y →
    RingConGen.Rel r y z → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) x z
Tactic: induction h with
    | of => exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)
    | refl => exact (RingQuot.ringCon r).refl _
    | symm => exact (RingQuot.ringCon r).symm ‹_›
    | trans => exact (RingQuot.ringCon r).trans ‹_› ‹_›
    | add => exact (RingQuot.ringCon r).add ‹_› ‹_›
    | mul => exact (RingQuot.ringCon r).mul ‹_› ‹_›
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
h₁ : ∀ (x y : R), r x y → Relation.EqvGen (Rel r) x y
h₂ : ∀ (x : R), Relation.EqvGen (Rel r) x x
h₃ : ∀ {x y : R}, RingConGen.Rel r x y → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y x
h₄ :
  ∀ {x y z : R},
    RingConGen.Rel r x y →
      RingConGen.Rel r y z → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) x z
⊢ Relation.EqvGen (Rel r) x₁ x₂
have h₅ : ∀ {w x y z : R},
  RingConGen.Rel r w x →
    RingConGen.Rel r y z →
      Relation.EqvGen (Rel r) w x → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) (w + y) (x + z)
Tactic: induction h with
    | of => exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)
    | refl => exact (RingQuot.ringCon r).refl _
    | symm => exact (RingQuot.ringCon r).symm ‹_›
    | trans => exact (RingQuot.ringCon r).trans ‹_› ‹_›
    | add => exact (RingQuot.ringCon r).add ‹_› ‹_›
    | mul => exact (RingQuot.ringCon r).mul ‹_› ‹_›
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
h₁ : ∀ (x y : R), r x y → Relation.EqvGen (Rel r) x y
h₂ : ∀ (x : R), Relation.EqvGen (Rel r) x x
h₃ : ∀ {x y : R}, RingConGen.Rel r x y → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y x
h₄ :
  ∀ {x y z : R},
    RingConGen.Rel r x y →
      RingConGen.Rel r y z → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) x z
h₅ :
  ∀ {w x y z : R},
    RingConGen.Rel r w x →
      RingConGen.Rel r y z →
        Relation.EqvGen (Rel r) w x → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) (w + y) (x + z)
⊢ Relation.EqvGen (Rel r) x₁ x₂
have h₆ : ∀ {w x y z : R},
  RingConGen.Rel r w x →
    RingConGen.Rel r y z →
      Relation.EqvGen (Rel r) w x → Relation.EqvGen (Rel r) y z → Relation.EqvGen (Rel r) (w * y) (x * z)
Tactic: induction h with
    | of => exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)
    | refl => exact (RingQuot.ringCon r).refl _
    | symm => exact (RingQuot.ringCon r).symm ‹_›
    | trans => exact (RingQuot.ringCon r).trans ‹_› ‹_›
    | add => exact (RingQuot.ringCon r).add ‹_› ‹_›
    | mul => exact (RingQuot.ringCon r).mul ‹_› ‹_›
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
x : RingQuot r
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
⊢ Quot.mk (Rel r) (HPow.hPow (β := ℕ) a 0) = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
have zero : Quot.mk (Rel r) 1 = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
x : RingQuot r
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
zero : Quot.mk (Rel r) 1 = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
⊢ Quot.mk (Rel r) (HPow.hPow (β := ℕ) a 0) = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
have zero₁ : Quot.mk (Rel r) 1 = Quot.mk (Rel r) 1
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
x : RingQuot r
n : ℕ
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
⊢ Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)
have zero : Quot.mk (Rel r) (HPow.hPow (β := ℕ) a 0) = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
Tactic: induction n with
      | zero => rw [pow_zero, pow_zero]
      | succ n ih =>
        simpa +instances [pow_succ, (· * ·), instMul, Quot.map₂_mk, mk.injEq] using
          congr_arg₂ (fun x y ↦ (⟨x⟩ : RingQuot r) * ⟨y⟩) ih (Quot.sound h)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
x : RingQuot r
n : ℕ
a_1 : Quot (Rel r)
a b : R
h : Rel r a b
zero : Quot.mk (Rel r) (HPow.hPow (β := ℕ) a 0) = Quot.mk (Rel r) (HPow.hPow (β := ℕ) b 0)
⊢ Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)
have succ : ∀ (n : ℕ) (ih : Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)),
  Quot.mk (Rel r) (a ^ (n + 1)) = Quot.mk (Rel r) (b ^ (n + 1))
Tactic: induction n with
      | zero => rw [pow_zero, pow_zero]
      | succ n ih =>
        simpa +instances [pow_succ, (· * ·), instMul, Quot.map₂_mk, mk.injEq] using
          congr_arg₂ (fun x y ↦ (⟨x⟩ : RingQuot r) * ⟨y⟩) ih (Quot.sound h)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
⊢ Function.Surjective (α := R) (β := RingQuot r) (⇑(mkRingHom r) : (a : R) → RingQuot r)
have simp : Function.Surjective (β := RingQuot r) fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x)
Tactic: simp only [mkRingHom_def, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ f = g
have a : ∀ (x : RingQuot r), Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) x : T) ((g : (a : RingQuot r) → T) x : T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ Eq.{uT + 1} (α := T) ((f : (a : RingQuot r) → T) x : T) ((g : (a : RingQuot r) → T) x : T)
have 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)
Tactic: rcases mkRingHom_surjective r x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 + c) : T) ((f : (a : R) → T) (b_1 + c) : T)
have 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)
Tactic: rw [map_add, map_add, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 + c) : T) ((f : (a : R) → T) (b_1 + c) : T)
have 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)
Tactic: rw [map_add, map_add, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 + c) : T) ((f : (a : R) → T) (b_1 + c) : T)
have 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)
Tactic: rw [map_add, map_add, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * c) : T) ((f : (a : R) → T) (b_1 * c) : T)
have 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)
Tactic: rw [map_mul, map_mul, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * c) : T) ((f : (a : R) → T) (b_1 * c) : T)
have 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)
Tactic: rw [map_mul, map_mul, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * c) : T) ((f : (a : R) → T) (b_1 * c) : T)
have 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)
Tactic: rw [map_mul, map_mul, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * b_1) : T) ((f : (a : R) → T) (a_1 * c) : T)
have 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)
Tactic: rw [map_mul, map_mul, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * b_1) : T) ((f : (a : R) → T) (a_1 * c) : T)
have 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)
Tactic: rw [map_mul, map_mul, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) (a_1 * b_1) : T) ((f : (a : R) → T) (a_1 * c) : T)
have 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)
Tactic: rw [map_mul, map_mul, r']
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) a : T) ((f : (a : R) → T) b : T)
have 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)
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']
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) a : T) ((f : (a : R) → T) b : T)
have 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)
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']
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq.{uT + 1} (α := T) ((f : (a : R) → T) a : T) ((f : (a : R) → T) b : T)
have 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)
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']
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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) }
⊢ (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
have 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)) sorry :
                    { 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) sorry)
                  f)) :
            R →+* T) :
          (a : R) → T)
        x :
      T)
    (((↑f : R →+* T) : (a : R) → T) x : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ (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
have simp : { toFun := fun (x : RingQuot r) ↦ Quot.lift (r := Rel r) (⇑(F.comp (mkRingHom r)) : (a : R) → T) sorry (x.toQuot (r := r)),
    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry } =
  F
Tactic: simp only [preLift_def]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ {
      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
have 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) sorry (x.toQuot (r := r)),
              map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry }
            (mkRingHom r) :
          (a : R) → T)
        x :
      T)
    ((F.comp (mkRingHom r) : (a : R) → T) x : T)
Tactic: ext