Theorem: ConnectedLT.subst (Algdata/Init/LawfulLT.lean)

State before:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
⊢ a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ < b₁ → a₂ < b₂
Tactic:
intro ha hb h₁
State after:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₂

State before:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₂
Tactic:
apply ConnectedLT.lt_of_lt_of_not_gt _ hb.left
State after:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₁

State before:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₁
Tactic:
apply ConnectedLT.lt_of_not_gt_of_lt ha.right h₁
State after:
no goals