Theorem: LO.FirstOrder.Completeness.SearchTree.rank_of_lt (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
τ₁ τ₂ : SearchTree T Γ
h : Lt T Γ τ₂ τ₁
⊢ τ₂.rank = τ₁.rank + 1
Tactic:
cases h
State after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ rank ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ = rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩ + 1

State before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ rank ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ = rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩ + 1
Tactic:
simp
State after:
no goals