case h.h.a
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
⊢ EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
⊢ EqvGen (Rel r) = RingConGen.Rel r
ext x₁ x₂
case h.h.a.mp
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
⊢ EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

case h.h.a.mpr
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → EqvGen (Rel r) x₁ x₂
case h.h.a
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
⊢ EqvGen (Rel r) x₁ x₂ ↔ RingConGen.Rel r x₁ x₂
constructor
case h.h.a.mp
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
h : EqvGen (Rel r) x₁ x₂
⊢ RingConGen.Rel r x₁ x₂
case h.h.a.mp
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
⊢ EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂
intro h
no goals
case h.h.a.mp
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
h : EqvGen (Rel r) x₁ x₂
⊢ RingConGen.Rel r x₁ x₂
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 ‹_› ‹_›
no goals
case h.h.a.mp.rel
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
h : Rel r x✝ y✝
⊢ RingConGen.Rel r x✝ y✝
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
no goals
case h.h.a.mp.rel.of
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝¹ y✝¹ x✝ y✝ : R
h✝ : r x✝ y✝
⊢ RingConGen.Rel r x✝ y✝
exact RingConGen.Rel.of _ _ ‹_›
no goals
case h.h.a.mp.rel.add_left
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
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✝)
exact h.add (RingConGen.Rel.refl _)
no goals
case h.h.a.mp.rel.mul_left
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
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✝)
exact h.mul (RingConGen.Rel.refl _)
no goals
case h.h.a.mp.rel.mul_right
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
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✝)
exact (RingConGen.Rel.refl _).mul h
no goals
case h.h.a.mp.refl
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ : R
⊢ RingConGen.Rel r x✝ x✝
exact RingConGen.Rel.refl _
no goals
case h.h.a.mp.symm
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : EqvGen (Rel r) x✝ y✝
a_ih✝ : RingConGen.Rel r x✝ y✝
⊢ RingConGen.Rel r y✝ x✝
exact RingConGen.Rel.symm ‹_›
no goals
case h.h.a.mp.trans
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ y✝ z✝ : R
a✝¹ : EqvGen (Rel r) x✝ y✝
a✝ : EqvGen (Rel r) y✝ z✝
a_ih✝¹ : RingConGen.Rel r x✝ y✝
a_ih✝ : RingConGen.Rel r y✝ z✝
⊢ RingConGen.Rel r x✝ z✝
exact RingConGen.Rel.trans ‹_› ‹_›
case h.h.a.mpr
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
⊢ EqvGen (Rel r) x₁ x₂
case h.h.a.mpr
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → EqvGen (Rel r) x₁ x₂
intro h
no goals
case h.h.a.mpr
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
⊢ EqvGen (Rel r) x₁ x₂
induction h with
| of => exact 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 ‹_› ‹_›
no goals
case h.h.a.mpr.of
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : r x✝ y✝
⊢ EqvGen (Rel r) x✝ y✝
exact EqvGen.rel _ _ (Rel.of ‹_›)
no goals
case h.h.a.mpr.refl
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ : R
⊢ EqvGen (Rel r) x✝ x✝
exact (RingQuot.ringCon r).refl _
no goals
case h.h.a.mpr.symm
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : RingConGen.Rel r x✝ y✝
a_ih✝ : EqvGen (Rel r) x✝ y✝
⊢ EqvGen (Rel r) y✝ x✝
exact (RingQuot.ringCon r).symm ‹_›
no goals
case h.h.a.mpr.trans
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
x₁ x₂ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r x✝ y✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : EqvGen (Rel r) x✝ y✝
a_ih✝ : EqvGen (Rel r) y✝ z✝
⊢ EqvGen (Rel r) x✝ z✝
exact (RingQuot.ringCon r).trans ‹_› ‹_›
no goals
case h.h.a.mpr.add
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
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✝¹ : EqvGen (Rel r) w✝ x✝
a_ih✝ : EqvGen (Rel r) y✝ z✝
⊢ EqvGen (Rel r) (w✝ + y✝) (x✝ + z✝)
exact (RingQuot.ringCon r).add ‹_› ‹_›
no goals
case h.h.a.mpr.mul
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
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✝¹ : EqvGen (Rel r) w✝ x✝
a_ih✝ : EqvGen (Rel r) y✝ z✝
⊢ EqvGen (Rel r) (w✝ * y✝) (x✝ * z✝)
exact (RingQuot.ringCon r).mul ‹_› ‹_›