Theorem: Weight.BasicInterval.rel (Weights/BasicInterval.lean)

State before:
⊢ base.a₂ * base.b₁ = base.a₁ * base.b₂ + 1
Tactic:
simp
State after:
no goals

State before:
I' : BasicInterval
⊢ (left I').a₂ * (left I').b₁ = (left I').a₁ * (left I').b₂ + 1
Tactic:
simp [add_mul, mul_add, I'.rel, add_assoc]
State after:
no goals

State before:
I' : BasicInterval
⊢ (right I').a₂ * (right I').b₁ = (right I').a₁ * (right I').b₂ + 1
Tactic:
simp [add_mul, mul_add, I'.rel, add_assoc, add_comm]
State after:
no goals