Theorem: LO.FirstOrder.UTerm.bv_substLast (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
have : x < (bv t).pred ∨ x = (bv t).pred ∨ x > (bv t).pred := Nat.lt_trichotomy _ _
State after:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
this : x < t.bv.pred ∨ x = t.bv.pred ∨ x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n

State before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
this : x < t.bv.pred ∨ x = t.bv.pred ∨ x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
rcases this with (lt | rfl | lt)
State after:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n

case inr.inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
hx : t.bv.pred < t.bv
⊢ (if t.bv.pred < t.bv.pred then bvar t.bv.pred else if t.bv.pred = t.bv.pred then u else bvar t.bv.pred.pred).bv ≤ n

case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n

State before:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
have : x < n := by simpa using lt_of_lt_of_le lt (Nat.pred_le_pred ht)
State after:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n

State before:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
simp only [lt, ↓reduceIte, bv_bvar, ge_iff_le]
State after:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ x + 1 ≤ n

State before:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ x + 1 ≤ n
Tactic:
exact this
State after:
no goals

State before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
⊢ x < n
Tactic:
simpa using lt_of_lt_of_le lt (Nat.pred_le_pred ht)
State after:
no goals

State before:
case inr.inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
hx : t.bv.pred < t.bv
⊢ (if t.bv.pred < t.bv.pred then bvar t.bv.pred else if t.bv.pred = t.bv.pred then u else bvar t.bv.pred.pred).bv ≤ n
Tactic:
simp [hu]
State after:
no goals

State before:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
simp [Nat.lt_asymm lt, Nat.ne_of_gt lt]
State after:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n

State before:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n
Tactic:
have : x ≤ t.bv.pred := Nat.le_pred_of_lt hx
State after:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
this : x ≤ t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n

State before:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
this : x ≤ t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n
Tactic:
exact False.elim (Nat.not_le_of_lt lt this)
State after:
no goals

State before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
⊢ ∀ (x : μ), (fvar x).bv ≤ n
Tactic:
simp[bv]
State after:
no goals