Theorem: LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper (Logic/FirstOrder/Basic/Syntax/Formula.lean)

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : upper p ≤ m
⊢ ¬fvar? p m
Tactic:
simp[upper, Nat.add_one_le_iff, fvar?] at h ⊢
State after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
⊢ m ∉ fvarList p

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
⊢ m ∉ fvarList p
Tactic:
intro hm
State after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ False

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ False
Tactic:
have : m ≤ Finset.sup p.fvarList.toFinset id :=
  Finset.le_sup (s := p.fvarList.toFinset) (b := m) (f := id) (by simpa using hm)
State after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
this : m ≤ (fvarList p).toFinset.sup id
⊢ False

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
this : m ≤ (fvarList p).toFinset.sup id
⊢ False
Tactic:
exact irrefl_of _ _ $ lt_of_lt_of_le h this
State after:
no goals

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ m ∈ (fvarList p).toFinset
Tactic:
simpa using hm
State after:
no goals