Theorem: freshVarForm_is_fresh (Pdl/Fresh.lean)

State before:
φ : Formula
⊢ freshVarForm φ ∉ voc φ
Tactic:
have := freshVarForm_is_larger φ
State after:
φ : Formula
this : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ voc φ

State before:
φ : Formula
this : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ voc φ
Tactic:
simp [freshVarForm, voc, vocabOfFormula] at *
State after:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ vocabOfFormula φ

State before:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ vocabOfFormula φ
Tactic:
by_contra hyp
State after:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
hyp : freshVarForm φ ∈ vocabOfFormula φ
⊢ False

State before:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
hyp : freshVarForm φ ∈ vocabOfFormula φ
⊢ False
Tactic:
specialize this (freshVarForm φ)
State after:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
⊢ False

State before:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
⊢ False
Tactic:
have := Nat.lt_irrefl (freshVarForm φ)
State after:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this✝ : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
this : ¬freshVarForm φ < freshVarForm φ
⊢ False

State before:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this✝ : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
this : ¬freshVarForm φ < freshVarForm φ
⊢ False
Tactic:
tauto
State after:
no goals