Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp (FOL/MM0/MM0.lean)

State before:
F : Formula
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ F) = sub (σ.comp σ') meta_var_ F
Tactic:
induction F
State after:
case meta_var_
σ σ' : Instantiation
a✝ : MetaVarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (meta_var_ a✝)) = sub (σ.comp σ') meta_var_ (meta_var_ a✝)

case pred_
σ σ' : Instantiation
a✝¹ : PredName
a✝ : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (pred_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (pred_ a✝¹ a✝)

case eq_
σ σ' : Instantiation
a✝¹ a✝ : VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (eq_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (eq_ a✝¹ a✝)

case true_
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ true_) = sub (σ.comp σ') meta_var_ true_

case not_
σ σ' : Instantiation
a✝ : Formula
a_ih✝ : sub σ meta_var_ (sub σ' meta_var_ a✝) = sub (σ.comp σ') meta_var_ a✝
⊢ sub σ meta_var_ (sub σ' meta_var_ a✝.not_) = sub (σ.comp σ') meta_var_ a✝.not_

case imp_
σ σ' : Instantiation
a✝¹ a✝ : Formula
a_ih✝¹ : sub σ meta_var_ (sub σ' meta_var_ a✝¹) = sub (σ.comp σ') meta_var_ a✝¹
a_ih✝ : sub σ meta_var_ (sub σ' meta_var_ a✝) = sub (σ.comp σ') meta_var_ a✝
⊢ sub σ meta_var_ (sub σ' meta_var_ (a✝¹.imp_ a✝)) = sub (σ.comp σ') meta_var_ (a✝¹.imp_ a✝)

case forall_
σ σ' : Instantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : sub σ meta_var_ (sub σ' meta_var_ a✝) = sub (σ.comp σ') meta_var_ a✝
⊢ sub σ meta_var_ (sub σ' meta_var_ (forall_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (forall_ a✝¹ a✝)

case def_
σ σ' : Instantiation
a✝¹ : DefName
a✝ : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (def_ a✝¹ a✝)) = sub (σ.comp σ') meta_var_ (def_ a✝¹ a✝)

State before:
σ σ' : Instantiation
X : MetaVarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (meta_var_ X)) = sub (σ.comp σ') meta_var_ (meta_var_ X)
Tactic:
case meta_var_ X =>
  rfl
State after:
no goals

State before:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (pred_ X xs)) = sub (σ.comp σ') meta_var_ (pred_ X xs)
Tactic:
case pred_ X xs =>
  simp only [sub]
  unfold Instantiation.comp
  simp
State after:
no goals

State before:
σ σ' : Instantiation
x y : VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (eq_ x y)) = sub (σ.comp σ') meta_var_ (eq_ x y)
Tactic:
case eq_ x y =>
  rfl
State after:
no goals

State before:
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ true_) = sub (σ.comp σ') meta_var_ true_
Tactic:
case true_ =>
  rfl
State after:
no goals

State before:
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ sub σ meta_var_ (sub σ' meta_var_ phi.not_) = sub (σ.comp σ') meta_var_ phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [sub]
  unfold Instantiation.comp
  congr! 1
State after:
no goals

State before:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ sub σ meta_var_ (sub σ' meta_var_ (phi.imp_ psi)) = sub (σ.comp σ') meta_var_ (phi.imp_ psi)
Tactic:
case imp_ phi psi phi_ih psi_ih =>
  simp only [sub]
  unfold Instantiation.comp
  congr! 1
State after:
no goals

State before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ sub σ meta_var_ (sub σ' meta_var_ (forall_ x phi)) = sub (σ.comp σ') meta_var_ (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  simp only [sub]
  unfold Instantiation.comp
  congr! 1
State after:
no goals

State before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (def_ X xs)) = sub (σ.comp σ') meta_var_ (def_ X xs)
Tactic:
case def_ X xs =>
  simp only [sub]
  unfold Instantiation.comp
  simp
State after:
no goals

State before:
σ σ' : Instantiation
X : MetaVarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (meta_var_ X)) = sub (σ.comp σ') meta_var_ (meta_var_ X)
Tactic:
rfl
State after:
no goals

State before:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (pred_ X xs)) = sub (σ.comp σ') meta_var_ (pred_ X xs)
Tactic:
simp only [sub]
State after:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑(σ.comp σ')) xs)

State before:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑(σ.comp σ')) xs)
Tactic:
unfold Instantiation.comp
State after:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)

State before:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)
Tactic:
simp
State after:
no goals

State before:
σ σ' : Instantiation
x y : VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (eq_ x y)) = sub (σ.comp σ') meta_var_ (eq_ x y)
Tactic:
rfl
State after:
no goals

State before:
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ true_) = sub (σ.comp σ') meta_var_ true_
Tactic:
rfl
State after:
no goals

State before:
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ sub σ meta_var_ (sub σ' meta_var_ phi.not_) = sub (σ.comp σ') meta_var_ phi.not_
Tactic:
simp only [sub]
State after:
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).not_ = (sub (σ.comp σ') meta_var_ phi).not_

State before:
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).not_ = (sub (σ.comp σ') meta_var_ phi).not_
Tactic:
unfold Instantiation.comp
State after:
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).not_ = (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).not_

State before:
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).not_ = (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).not_
Tactic:
congr! 1
State after:
no goals

State before:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ sub σ meta_var_ (sub σ' meta_var_ (phi.imp_ psi)) = sub (σ.comp σ') meta_var_ (phi.imp_ psi)
Tactic:
simp only [sub]
State after:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).imp_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub (σ.comp σ') meta_var_ phi).imp_ (sub (σ.comp σ') meta_var_ psi)

State before:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).imp_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub (σ.comp σ') meta_var_ phi).imp_ (sub (σ.comp σ') meta_var_ psi)
Tactic:
unfold Instantiation.comp
State after:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).imp_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).imp_ (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ psi)

State before:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).imp_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).imp_ (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ psi)
Tactic:
congr! 1
State after:
no goals

State before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ sub σ meta_var_ (sub σ' meta_var_ (forall_ x phi)) = sub (σ.comp σ') meta_var_ (forall_ x phi)
Tactic:
simp only [sub]
State after:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑(σ.comp σ') x) (sub (σ.comp σ') meta_var_ phi)

State before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑(σ.comp σ') x) (sub (σ.comp σ') meta_var_ phi)
Tactic:
unfold Instantiation.comp
State after:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑⟨↑σ ∘ ↑σ', ⋯⟩ x) (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi)

State before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑⟨↑σ ∘ ↑σ', ⋯⟩ x) (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi)
Tactic:
congr! 1
State after:
no goals

State before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (def_ X xs)) = sub (σ.comp σ') meta_var_ (def_ X xs)
Tactic:
simp only [sub]
State after:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑(σ.comp σ')) xs)

State before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑(σ.comp σ')) xs)
Tactic:
unfold Instantiation.comp
State after:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)

State before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)
Tactic:
simp
State after:
no goals