Theorem: FOL.NV.C_18_3 (FOL/NV/Margaris/Fol.lean)

State before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsProof (P_U.iff_ P_V)
Tactic:
apply
  IsDeduct.mp_
    (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ ((Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V)).imp_ (P_U.iff_ P_V))

case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ ((Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V)).imp_ (P_U.iff_ P_V))
Tactic:
apply T_18_2 U V P_U P_V ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList h1
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ ∀ (v : VarName),
    (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U → v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ ∀ (v : VarName),
    (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U → v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Tactic:
intro v a1
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Tactic:
simp
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Tactic:
simp only [isBoundIn_iff_mem_boundVarSet] at a1
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Tactic:
exact a1
State after:
no goals

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))
Tactic:
simp only [Formula.Forall_]
State after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList)

State before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList)
Tactic:
induction ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
State after:
case a.nil
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) [])

case a.cons
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tail✝)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) (head✝ :: tail✝))

State before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) [])
Tactic:
case _ =>
  simp
  exact h2
State after:
no goals

State before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) [])
Tactic:
simp
State after:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (U.iff_ V)

State before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (U.iff_ V)
Tactic:
exact h2
State after:
no goals

State before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) (hd :: tl))
Tactic:
simp
State after:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (forall_ hd (List.foldr forall_ (U.iff_ V) tl))

State before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (forall_ hd (List.foldr forall_ (U.iff_ V) tl))
Tactic:
apply generalization
State after:
case h1
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)

case h2
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ ∀ H ∈ ∅, ¬isFreeIn hd H

State before:
case h1
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
Tactic:
exact ih
State after:
no goals

State before:
case h2
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ ∀ H ∈ ∅, ¬isFreeIn hd H
Tactic:
simp
State after:
no goals