no goals
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
T : Type u₄
inst✝¹ : Semiring T
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)
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
no goals
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝)
exact Rel.of (hr _ _ h)
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝)
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝))
rw [star_add, star_add]
no goals
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝)
exact Rel.add_left h
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝)
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝))
rw [star_mul, star_mul]
no goals
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝)
exact Rel.mul_right h
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝¹)
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝))
rw [star_mul, star_mul]
no goals
case 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
T : Type u₄
inst✝¹ : Semiring T
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✝¹)
exact Rel.mul_left h