Theorem: FOL.NV.isTautoPrime_imp_isTautoPrime_substPrime (FOL/NV/Margaris/Prop.lean)

State before:
P : Formula
h1 : P.IsTautoPrime
σ : Formula → Formula
⊢ (substPrime σ P).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime] at h1
State after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ (substPrime σ P).IsTautoPrime

State before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ (substPrime σ P).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
State after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (substPrime σ P)

State before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (substPrime σ P)
Tactic:
intro V
State after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ P)

State before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ P)
Tactic:
simp only [evalPrime_substPrime_eq_evalPrime_evalPrime P σ V]
State after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime (fun H => decide (evalPrime V (σ H))) P

State before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime (fun H => decide (evalPrime V (σ H))) P
Tactic:
apply h1
State after:
no goals