-- Mathlib/Algebra/Star/RingQuot.lean
theorem Rel.star (hr : ∀ a b, r a b → r (star a) (star b))
    ⦃a b : R⦄ (h : Rel r a b) : Rel r (star a) (star b)

Proof state:
case mul_right
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star (a✝¹ * b✝)) (Star.star (a✝¹ * c✝))

Tactic:
rw [star_mul, star_mul]

Result:
case mul_right
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star b✝ * Star.star a✝¹) (Star.star c✝ * Star.star a✝¹)

Proof state:
case mul_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star c✝ * Star.star a✝¹) (Star.star c✝ * Star.star b✝)

Tactic:
exact Rel.mul_right h

Result:
no goals

Proof state:
case add_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star a✝¹ + Star.star c✝) (Star.star b✝ + Star.star c✝)

Tactic:
exact Rel.add_left h

Result:
no goals

Proof state:
case mul_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star (a✝¹ * c✝)) (Star.star (b✝ * c✝))

Tactic:
rw [star_mul, star_mul]

Result:
case mul_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star c✝ * Star.star a✝¹) (Star.star c✝ * Star.star b✝)

Proof state:
case of
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b x✝ y✝ : R
h : r x✝ y✝
⊢ Rel r (Star.star x✝) (Star.star y✝)

Tactic:
exact Rel.of (hr _ _ h)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b : R
h : Rel r a b
⊢ Rel r (Star.star a) (Star.star b)

Tactic:
induction h with
| of h          => exact Rel.of (hr _ _ h)
| add_left _ h  => rw [star_add, star_add]
                   exact Rel.add_left h
| mul_left _ h  => rw [star_mul, star_mul]
                   exact Rel.mul_right h
| mul_right _ h => rw [star_mul, star_mul]
                   exact Rel.mul_left h

Result:
no goals

Proof state:
case add_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star (a✝¹ + c✝)) (Star.star (b✝ + c✝))

Tactic:
rw [star_add, star_add]

Result:
case add_left
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
h : Rel r (Star.star a✝¹) (Star.star b✝)
⊢ Rel r (Star.star a✝¹ + Star.star c✝) (Star.star b✝ + Star.star c✝)

Proof state:
case mul_right
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star b✝ * Star.star a✝¹) (Star.star c✝ * Star.star a✝¹)

Tactic:
exact Rel.mul_left h

Result:
no goals