awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a b x c d x_1 y z : R
h_1 : Relation.EqvGen (Rel r) x_1 y
h_2 : 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:
exact h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- 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
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)
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)
⊢ Relation.EqvGen (Rel r) (x * c) (x * d)

Tactic:
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'

Premises used: Relation.EqvGen.refl, symm, refl
-- 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
a b x y : R
h : 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:
(hxy hcd.symm).symm

Premises used: Relation.EqvGen.symm
-- 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
a b x y : R
h : 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:
exact (hxy hcd.symm).symm

Premises used: Relation.EqvGen.symm
-- 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
a b x y z : R
h_1 : Relation.EqvGen (Rel r) x y
h_2 : 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:
(h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)

Premises used: Relation.EqvGen.trans, Relation.EqvGen.refl
-- 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
a b x y z : R
h_1 : Relation.EqvGen (Rel r) x y
h_2 : 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:
exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)

Premises used: Relation.EqvGen.trans, Relation.EqvGen.refl
-- 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
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)
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)
⊢ Relation.EqvGen (Rel r) (a * c) (b * 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 _)

Premises used: Relation.EqvGen.refl, symm, refl
-- 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
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)

Tactic:
(Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_

Premises used: Relation.EqvGen.trans, Relation.EqvGen.rel, RingQuot.Rel.add_left
-- 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
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : Relation.EqvGen (Rel r) (y + c) (y + d)
⊢ Relation.EqvGen (Rel r) (x + c) (y + d)

Tactic:
refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_

Premises used: Relation.EqvGen.trans, Relation.EqvGen.rel, RingQuot.Rel.add_left
-- 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
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
hcd : Rel r x_1 y_1
⊢ Relation.EqvGen (Rel r) (y + x_1) (y + y_1)

Tactic:
Relation.EqvGen.rel _ _ hcd.add_right

Premises used: RingQuot.Rel.add_right, Relation.EqvGen.rel
-- 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
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
hcd : Rel r x_1 y_1
⊢ Relation.EqvGen (Rel r) (y + x_1) (y + y_1)

Tactic:
exact Relation.EqvGen.rel _ _ hcd.add_right

Premises used: RingQuot.Rel.add_right, Relation.EqvGen.rel
-- 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
a b x y : R
hab : Rel r x y
c d x_1 : R
⊢ Relation.EqvGen (Rel r) (y + x_1) (y + x_1)

Tactic:
Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- 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
a b x y : R
hab : Rel r x y
c d x_1 : R
⊢ Relation.EqvGen (Rel r) (y + x_1) (y + x_1)

Tactic:
exact Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- 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
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h : Relation.EqvGen (Rel r) (y + x_1) (y + y_1)
⊢ Relation.EqvGen (Rel r) (y + y_1) (y + x_1)

Tactic:
h.symm _ _

Premises used: Relation.EqvGen.symm
-- 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
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h : Relation.EqvGen (Rel r) (y + x_1) (y + y_1)
⊢ Relation.EqvGen (Rel r) (y + y_1) (y + x_1)

Tactic:
exact h.symm _ _

Premises used: Relation.EqvGen.symm
-- 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
a b x y : R
hab : Rel r x y
c d x_1 y_1 z : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h_2 : Relation.EqvGen (Rel r) y_1 z
h : Relation.EqvGen (Rel r) (y + x_1) (y + y_1)
h' : Relation.EqvGen (Rel r) (y + y_1) (y + z)
⊢ Relation.EqvGen (Rel r) (y + x_1) (y + z)

Tactic:
h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- 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
a b x y : R
hab : Rel r x y
c d x_1 y_1 z : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h_2 : Relation.EqvGen (Rel r) y_1 z
h : Relation.EqvGen (Rel r) (y + x_1) (y + y_1)
h' : Relation.EqvGen (Rel r) (y + y_1) (y + z)
⊢ Relation.EqvGen (Rel r) (y + x_1) (y + z)

Tactic:
exact h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- 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
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)
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)
⊢ Relation.EqvGen (Rel r) (y + c) (y + d)

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'

Premises used: Relation.EqvGen.refl, symm, refl
-- 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
a b x c d x_1 y : R
hcd : Rel r x_1 y
⊢ Relation.EqvGen (Rel r) (x + x_1) (x + y)

Tactic:
Relation.EqvGen.rel _ _ hcd.add_right

Premises used: RingQuot.Rel.add_right, Relation.EqvGen.rel
-- 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
a b x c d x_1 y : R
hcd : Rel r x_1 y
⊢ Relation.EqvGen (Rel r) (x + x_1) (x + y)

Tactic:
exact Relation.EqvGen.rel _ _ hcd.add_right

Premises used: RingQuot.Rel.add_right, Relation.EqvGen.rel
-- 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
a b x c d x_1 : R
⊢ Relation.EqvGen (Rel r) (x + x_1) (x + x_1)

Tactic:
Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- 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
a b x c d x_1 : R
⊢ Relation.EqvGen (Rel r) (x + x_1) (x + x_1)

Tactic:
exact Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- 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
a b x c d x_1 y : R
h_1 : 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:
h.symm _ _

Premises used: Relation.EqvGen.symm
-- 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
a b x c d x_1 y : R
h_1 : 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:
exact h.symm _ _

Premises used: Relation.EqvGen.symm
-- 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
a b x c d x_1 y z : R
h_1 : Relation.EqvGen (Rel r) x_1 y
h_2 : 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:
h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- 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
a b x c d x_1 y z : R
h_1 : Relation.EqvGen (Rel r) x_1 y
h_2 : 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:
exact h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- 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
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)
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)
⊢ Relation.EqvGen (Rel r) (x + c) (x + d)

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'

Premises used: Relation.EqvGen.refl, symm, refl
-- 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
a b x y : R
h : 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:
(hxy hcd.symm).symm

Premises used: Relation.EqvGen.symm
-- 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
a b x y : R
h : 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:
exact (hxy hcd.symm).symm

Premises used: Relation.EqvGen.symm
-- 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
a b x y z : R
h_1 : Relation.EqvGen (Rel r) x y
h_2 : 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:
(h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)

Premises used: Relation.EqvGen.trans, Relation.EqvGen.refl
-- 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
a b x y z : R
h_1 : Relation.EqvGen (Rel r) x y
h_2 : 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:
exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)

Premises used: Relation.EqvGen.trans, Relation.EqvGen.refl
-- 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
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)
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)
⊢ Relation.EqvGen (Rel r) (a + c) (b + 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 _)

Premises used: Relation.EqvGen.refl, symm, refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
h : ∀ (x₁ x₂ : R), Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂
⊢ Relation.EqvGen (Rel r) = RingConGen.Rel r

Tactic:
ext x₁ x₂
-- Module: Mathlib.Algebra.RingQuot
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₂
h₁ : RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂
⊢ Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂

Tactic:
constructor
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y x_1 y_1 : R
h : r x_1 y_1
⊢ RingConGen.Rel r x_1 y_1

Tactic:
RingConGen.Rel.of _ _ ‹_›

Premises used: RingConGen.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y x_1 y_1 : R
h : r x_1 y_1
⊢ RingConGen.Rel r x_1 y_1

Tactic:
exact RingConGen.Rel.of _ _ ‹_›

Premises used: RingConGen.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y a b c : R
h_1 : Rel r a b
h : RingConGen.Rel r a b
⊢ RingConGen.Rel r (a + c) (b + c)

Tactic:
h.add (RingConGen.Rel.refl _)

Premises used: RingConGen.Rel.refl, RingConGen.Rel.add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y a b c : R
h_1 : Rel r a b
h : RingConGen.Rel r a b
⊢ RingConGen.Rel r (a + c) (b + c)

Tactic:
exact h.add (RingConGen.Rel.refl _)

Premises used: RingConGen.Rel.refl, RingConGen.Rel.add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y a b c : R
h_1 : Rel r a b
h : RingConGen.Rel r a b
⊢ RingConGen.Rel r (a * c) (b * c)

Tactic:
h.mul (RingConGen.Rel.refl _)

Premises used: RingConGen.Rel.mul, RingConGen.Rel.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y a b c : R
h_1 : Rel r a b
h : RingConGen.Rel r a b
⊢ RingConGen.Rel r (a * c) (b * c)

Tactic:
exact h.mul (RingConGen.Rel.refl _)

Premises used: RingConGen.Rel.mul, RingConGen.Rel.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y a b c : R
h_1 : Rel r b c
h : RingConGen.Rel r b c
⊢ RingConGen.Rel r (a * b) (a * c)

Tactic:
(RingConGen.Rel.refl _).mul h

Premises used: RingConGen.Rel.mul, RingConGen.Rel.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y a b c : R
h_1 : Rel r b c
h : RingConGen.Rel r b c
⊢ RingConGen.Rel r (a * b) (a * c)

Tactic:
exact (RingConGen.Rel.refl _).mul h

Premises used: RingConGen.Rel.mul, RingConGen.Rel.refl
-- Module: Mathlib.Algebra.RingQuot
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)
h₄ : ∀ ⦃a b c : R⦄, Rel r b c → ∀ (h : RingConGen.Rel r b c), RingConGen.Rel r (a * b) (a * c)
⊢ 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

Premises used: RingConGen.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x : R
⊢ RingConGen.Rel r x x

Tactic:
RingConGen.Rel.refl _

Premises used: RingConGen.Rel.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x : R
⊢ RingConGen.Rel r x x

Tactic:
exact RingConGen.Rel.refl _

Premises used: RingConGen.Rel.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : Relation.EqvGen (Rel r) x y
a_ih : RingConGen.Rel r x y
⊢ RingConGen.Rel r y x

Tactic:
RingConGen.Rel.symm ‹_›

Premises used: RingConGen.Rel.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
x₁ x₂ x y : R
h : Relation.EqvGen (Rel r) x y
a_ih : RingConGen.Rel r x y
⊢ RingConGen.Rel r y x

Tactic:
exact RingConGen.Rel.symm ‹_›

Premises used: RingConGen.Rel.symm