-- Mathlib/Algebra/RingQuot.lean
theorem eqvGen_rel_eq (r : R → R → Prop) : Relation.EqvGen (Rel r) = RingConGen.Rel r

Proof state:
case h.h.a.mp.rel.mul_left
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : RingConGen.Rel r a✝¹ b✝
⊢ RingConGen.Rel r (a✝¹ * c✝) (b✝ * c✝)

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

Result:
no goals

Proof state:
case h.h.a.mp.rel.add_left
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : RingConGen.Rel r a✝¹ b✝
⊢ RingConGen.Rel r (a✝¹ + c✝) (b✝ + c✝)

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

Result:
no goals

Proof state:
case h.h.a.mp.rel
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✝

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

Result:
no goals

Proof state:
case h.h.a.mp.rel.of
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝¹ y✝¹ x✝ y✝ : R
h✝ : r x✝ y✝
⊢ RingConGen.Rel r x✝ y✝

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

Result:
no goals

Proof state:
case h.h.a.mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

Tactic:
intro h

Result:
case h.h.a.mp
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₂

Proof state:
case h.h.a.mpr.add
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ w✝ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r w✝ x✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : Relation.EqvGen (Rel r) w✝ x✝
a_ih✝ : Relation.EqvGen (Rel r) y✝ z✝
⊢ Relation.EqvGen (Rel r) (w✝ + y✝) (x✝ + z✝)

Tactic:
exact (RingQuot.ringCon r).add ‹_› ‹_›

Result:
no goals

Proof state:
case h.h.a
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂

Tactic:
constructor

Result:
case h.h.a.mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

case h.h.a.mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Proof state:
case h.h.a.mpr.mul
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ w✝ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r w✝ x✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : Relation.EqvGen (Rel r) w✝ x✝
a_ih✝ : Relation.EqvGen (Rel r) y✝ z✝
⊢ Relation.EqvGen (Rel r) (w✝ * y✝) (x✝ * z✝)

Tactic:
exact (RingQuot.ringCon r).mul ‹_› ‹_›

Result:
no goals

Proof state:
case h.h.a.mp.trans
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ z✝ : R
a✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a✝ : Relation.EqvGen (Rel r) y✝ z✝
a_ih✝¹ : RingConGen.Rel r x✝ y✝
a_ih✝ : RingConGen.Rel r y✝ z✝
⊢ RingConGen.Rel r x✝ z✝

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

Result:
no goals

Proof state:
case h.h.a.mpr
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₂

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 ‹_› ‹_›

Result:
no goals

Proof state:
case h.h.a.mp.refl
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ : R
⊢ RingConGen.Rel r x✝ x✝

Tactic:
exact RingConGen.Rel.refl _

Result:
no goals

Proof state:
case h.h.a.mpr.trans
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r x✝ y✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a_ih✝ : Relation.EqvGen (Rel r) y✝ z✝
⊢ Relation.EqvGen (Rel r) x✝ z✝

Tactic:
exact (RingQuot.ringCon r).trans ‹_› ‹_›

Result:
no goals

Proof state:
case h.h.a.mp.symm
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : Relation.EqvGen (Rel r) x✝ y✝
a_ih✝ : RingConGen.Rel r x✝ y✝
⊢ RingConGen.Rel r y✝ x✝

Tactic:
exact RingConGen.Rel.symm ‹_›

Result:
no goals

Proof state:
case h.h.a.mpr.symm
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : RingConGen.Rel r x✝ y✝
a_ih✝ : Relation.EqvGen (Rel r) x✝ y✝
⊢ Relation.EqvGen (Rel r) y✝ x✝

Tactic:
exact (RingQuot.ringCon r).symm ‹_›

Result:
no goals

Proof state:
case h.h.a.mpr.of
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : r x✝ y✝
⊢ Relation.EqvGen (Rel r) x✝ y✝

Tactic:
exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)

Result:
no goals

Proof state:
case h.h.a.mpr.refl
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ : R
⊢ Relation.EqvGen (Rel r) x✝ x✝

Tactic:
exact (RingQuot.ringCon r).refl _

Result:
no goals

Proof state:
case h.h.a.mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Tactic:
intro h

Result:
case h.h.a.mpr
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₂

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Relation.EqvGen (Rel r) = RingConGen.Rel r

Tactic:
ext x₁ x₂

Result:
case h.h.a
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂

Proof state:
case h.h.a.mp.rel.mul_right
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : RingConGen.Rel r b✝ c✝
⊢ RingConGen.Rel r (a✝¹ * b✝) (a✝¹ * c✝)

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

Result:
no goals

Proof state:
case h.h.a.mp
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₂

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 ‹_› ‹_›

Result:
no goals