awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
rel :
  ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d)
refl : ∀ (x : R) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (x * d)
symm :
  ∀ (x y : R),
    Relation.EqvGen (Rel r) x y →
      ∀ (hxy : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d)) {c d : R}
        (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (y * c) (x * d)
⊢ Relation.EqvGen (Rel r) (a * c) (b * d)
have trans : ∀ (x y z : R),
  Relation.EqvGen (Rel r) x y →
    Relation.EqvGen (Rel r) y z →
      ∀ (h : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d))
        (h' : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (y * c) (z * d)) {c d : R}
        (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (z * d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- 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
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x + c) (y + d)
have rel : Relation.EqvGen (Rel r) (y + c) (y + d)
Tactic: refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
-- 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
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (y + c) (y + d)
have rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y + x) (y + y_1)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y + x) (y + y_1)
⊢ Relation.EqvGen (Rel r) (y + c) (y + d)
have rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y + x) (y + x)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y + x) (y + y_1)
rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y + x) (y + x)
⊢ Relation.EqvGen (Rel r) (y + c) (y + d)
have rel₂ : ∀ (x y_1 : R),
  Relation.EqvGen (Rel r) x y_1 →
    ∀ (h : Relation.EqvGen (Rel r) (y + x) (y + y_1)), Relation.EqvGen (Rel r) (y + y_1) (y + x)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y + x) (y + y_1)
rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y + x) (y + x)
rel₂ :
  ∀ (x y_1 : R),
    Relation.EqvGen (Rel r) x y_1 →
      ∀ (h : Relation.EqvGen (Rel r) (y + x) (y + y_1)), Relation.EqvGen (Rel r) (y + y_1) (y + x)
⊢ Relation.EqvGen (Rel r) (y + c) (y + d)
have rel₃ : ∀ (x y_1 z : R),
  Relation.EqvGen (Rel r) x y_1 →
    Relation.EqvGen (Rel r) y_1 z →
      ∀ (h : Relation.EqvGen (Rel r) (y + x) (y + y_1)) (h' : Relation.EqvGen (Rel r) (y + y_1) (y + z)),
        Relation.EqvGen (Rel r) (y + x) (y + z)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x + c) (x + d)
have refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x + x_1) (x + y)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x + x_1) (x + y)
⊢ Relation.EqvGen (Rel r) (x + c) (x + d)
have refl₁ : ∀ (x_1 : R), Relation.EqvGen (Rel r) (x + x_1) (x + x_1)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x + x_1) (x + y)
refl₁ : ∀ (x_1 : R), Relation.EqvGen (Rel r) (x + x_1) (x + x_1)
⊢ Relation.EqvGen (Rel r) (x + c) (x + d)
have refl₂ : ∀ (x_1 y : R),
  Relation.EqvGen (Rel r) x_1 y →
    ∀ (h : Relation.EqvGen (Rel r) (x + x_1) (x + y)), Relation.EqvGen (Rel r) (x + y) (x + x_1)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x + x_1) (x + y)
refl₁ : ∀ (x_1 : R), Relation.EqvGen (Rel r) (x + x_1) (x + x_1)
refl₂ :
  ∀ (x_1 y : R),
    Relation.EqvGen (Rel r) x_1 y →
      ∀ (h : Relation.EqvGen (Rel r) (x + x_1) (x + y)), Relation.EqvGen (Rel r) (x + y) (x + x_1)
⊢ Relation.EqvGen (Rel r) (x + c) (x + d)
have refl₃ : ∀ (x_1 y z : R),
  Relation.EqvGen (Rel r) x_1 y →
    Relation.EqvGen (Rel r) y z →
      ∀ (h : Relation.EqvGen (Rel r) (x + x_1) (x + y)) (h' : Relation.EqvGen (Rel r) (x + y) (x + z)),
        Relation.EqvGen (Rel r) (x + x_1) (x + z)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- 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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (a + c) (b + d)
have rel : ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- 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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
rel :
  ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d)
⊢ Relation.EqvGen (Rel r) (a + c) (b + d)
have refl : ∀ (x : R) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (x + d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- 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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
rel :
  ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d)
refl : ∀ (x : R) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (x + d)
⊢ Relation.EqvGen (Rel r) (a + c) (b + d)
have symm : ∀ (x y : R),
  Relation.EqvGen (Rel r) x y →
    ∀ (hxy : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d)) {c d : R}
      (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (y + c) (x + d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- 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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
rel :
  ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d)
refl : ∀ (x : R) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (x + d)
symm :
  ∀ (x y : R),
    Relation.EqvGen (Rel r) x y →
      ∀ (hxy : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d)) {c d : R}
        (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (y + c) (x + d)
⊢ Relation.EqvGen (Rel r) (a + c) (b + d)
have trans : ∀ (x y z : R),
  Relation.EqvGen (Rel r) x y →
    Relation.EqvGen (Rel r) y z →
      ∀ (h : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (y + d))
        (h' : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (y + c) (z + d)) {c d : R}
        (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x + c) (z + d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
⊢ Relation.EqvGen (Rel r) = RingConGen.Rel r
have h : ∀ (x₁ x₂ : R), Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂
Tactic: ext x₁ x₂
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂
have h : Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂
⊢ Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂
have h₁ : RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : Rel r x y
⊢ RingConGen.Rel r x y
have h₁ : ∀ ⦃x y : R⦄, r x y → RingConGen.Rel r x y
Tactic: induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
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₂ x y : R
h : Rel r x y
h₁ : ∀ ⦃x y : R⦄, r x y → RingConGen.Rel r x y
⊢ RingConGen.Rel r x y
have h₂ : ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : RingConGen.Rel r a b), RingConGen.Rel r (a + c) (b + c)
Tactic: induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
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₂ x y : R
h : Rel r x y
h₁ : ∀ ⦃x y : R⦄, r x y → RingConGen.Rel r x y
h₂ : ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : RingConGen.Rel r a b), RingConGen.Rel r (a + c) (b + c)
⊢ RingConGen.Rel r x y
have h₃ : ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : RingConGen.Rel r a b), RingConGen.Rel r (a * c) (b * c)
Tactic: induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
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₂ x y : R
h : Rel r x y
h₁ : ∀ ⦃x y : R⦄, r x y → RingConGen.Rel r x y
h₂ : ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : RingConGen.Rel r a b), RingConGen.Rel r (a + c) (b + c)
h₃ : ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : RingConGen.Rel r a b), RingConGen.Rel r (a * c) (b * c)
⊢ RingConGen.Rel r x y
have h₄ : ∀ ⦃a b c : R⦄, Rel r b c → ∀ (h : RingConGen.Rel r b c), RingConGen.Rel r (a * b) (a * c)
Tactic: induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
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 : Relation.EqvGen (Rel r) x₁ x₂
⊢ RingConGen.Rel r x₁ x₂
have h₁ : ∀ (x y : R) (h : Rel r x y), RingConGen.Rel r x y
Tactic: induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›
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 : Relation.EqvGen (Rel r) x₁ x₂
h₁ : ∀ (x y : R) (h : Rel r x y), RingConGen.Rel r x y
⊢ RingConGen.Rel r x₁ x₂
have h₂ : ∀ (x : R), RingConGen.Rel r x x
Tactic: induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›
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 : Relation.EqvGen (Rel r) x₁ x₂
h₁ : ∀ (x y : R) (h : Rel r x y), RingConGen.Rel r x y
h₂ : ∀ (x : R), RingConGen.Rel r x x
⊢ RingConGen.Rel r x₁ x₂
have h₃ : ∀ (x y : R), Relation.EqvGen (Rel r) x y → RingConGen.Rel r x y → RingConGen.Rel r y x
Tactic: induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›
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 : Relation.EqvGen (Rel r) x₁ x₂
h₁ : ∀ (x y : R) (h : Rel r x y), RingConGen.Rel r x y
h₂ : ∀ (x : R), RingConGen.Rel r x x
h₃ : ∀ (x y : R), Relation.EqvGen (Rel r) x y → RingConGen.Rel r x y → RingConGen.Rel r y x
⊢ RingConGen.Rel r x₁ x₂
have h₄ : ∀ (x y z : R),
  Relation.EqvGen (Rel r) x y →
    Relation.EqvGen (Rel r) y z → RingConGen.Rel r x y → RingConGen.Rel r y z → RingConGen.Rel r x z
Tactic: induction h with
    | rel _ _ h => induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h
    | refl => exact RingConGen.Rel.refl _
    | symm => exact RingConGen.Rel.symm ‹_›
    | trans => exact RingConGen.Rel.trans ‹_› ‹_›
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₂
⊢ Relation.EqvGen (Rel r) x₁ x₂
have h₁ : ∀ (x y : R), r x y → Relation.EqvGen (Rel r) x y
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
⊢ Relation.EqvGen (Rel r) x₁ x₂
have h₂ : ∀ (x : R), Relation.EqvGen (Rel r) x x
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
⊢ Relation.EqvGen (Rel r) x₁ x₂
have h₃ : ∀ {x y : R}, RingConGen.Rel r x y → Relation.EqvGen (Rel r) x y → Relation.EqvGen (Rel r) y x
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