internlm/Lean-Github huggingface dataset:
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ phi.not_.metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
Proof state after:
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ phi.metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ phi.metaVarSet = ∅
Tactic:
exact phi_ih vs h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
⊢ (phi.imp_ psi).metaVarSet = ∅
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ (phi.imp_ psi).metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ (phi.imp_ psi).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
Proof state after:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ phi.metaVarSet ∪ psi.metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ phi.metaVarSet ∪ psi.metaVarSet = ∅
Tactic:
cases h1
Proof state after:
case intro
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ phi.metaVarSet ∪ psi.metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ phi.metaVarSet ∪ psi.metaVarSet = ∅
Tactic:
case intro h1_left h1_right =>
  simp only [phi_ih vs h1_left]
  simp only [psi_ih vs h1_right]
  simp
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ phi.metaVarSet ∪ psi.metaVarSet = ∅
Tactic:
simp only [phi_ih vs h1_left]
Proof state after:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ ∅ ∪ psi.metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ ∅ ∪ psi.metaVarSet = ∅
Tactic:
simp only [psi_ih vs h1_right]
Proof state after:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ ∅ ∪ ∅ = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ ∅ ∪ ∅ = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ x phi)
⊢ (forall_ x phi).metaVarSet = ∅
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ (forall_ x phi).metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ (forall_ x phi).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
Proof state after:
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ phi.metaVarSet = ∅
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ phi.metaVarSet = ∅
Tactic:
exact phi_ih (x :: vs) h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_var_set_is_empty
Proof state before:
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
⊢ (def_ X xs).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
apply Exists.elim σ.2
Proof state after:
σ : Instantiation
⊢ ∀ (a : VarName → VarName), ↑σ ∘ a = id ∧ a ∘ ↑σ = id → ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
⊢ ∀ (a : VarName → VarName), ↑σ ∘ a = id ∧ a ∘ ↑σ = id → ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
intro σ' a1
Proof state after:
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
cases a1
Proof state after:
case intro
σ : Instantiation
σ' : VarName → VarName
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
apply Exists.intro σ_inv
Proof state after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
constructor
Proof state after:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id

case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ_inv ∘ ↑σ = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ∃ σ'_1, σ' ∘ σ'_1 = id ∧ σ'_1 ∘ σ' = id
Tactic:
apply Exists.intro σ.1
Proof state after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id ∧ ↑σ ∘ σ' = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id ∧ ↑σ ∘ σ' = id
Tactic:
constructor
Proof state after:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id

case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ↑σ ∘ σ' = id
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id
Tactic:
exact a1_right
Proof state after:
no goals
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ↑σ ∘ σ' = id
Tactic:
exact a1_left
Proof state after:
no goals
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id
Tactic:
exact a1_left
Proof state after:
no goals
Theorem: MM0.Instantiation.has_left_right_inverse
Proof state before:
case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ_inv ∘ ↑σ = id
Tactic:
exact a1_right
Proof state after:
no goals
Theorem: MM0.Instantiation.is_injective
Proof state before:
σ : Instantiation
⊢ Function.Injective ↑σ
Tactic:
obtain ⟨σ', a1⟩ := σ.2
Proof state after:
case intro
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Function.Injective ↑σ
Theorem: MM0.Instantiation.is_injective
Proof state before:
case intro
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Function.Injective ↑σ
Tactic:
cases a1
Proof state after:
case intro.intro
σ : Instantiation
σ' : VarName → VarName
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Function.Injective ↑σ
Theorem: MM0.Instantiation.is_injective
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Injective ↑σ
Tactic:
case intro a1_left a1_right =>
  have s1 : Function.LeftInverse σ' σ.1 := congr_fun a1_right
  exact Function.LeftInverse.injective s1
Proof state after:
no goals
Theorem: MM0.Instantiation.is_injective
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Injective ↑σ
Tactic:
have s1 : Function.LeftInverse σ' σ.1 := congr_fun a1_right
Proof state after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.LeftInverse σ' ↑σ
⊢ Function.Injective ↑σ
Theorem: MM0.Instantiation.is_injective
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.LeftInverse σ' ↑σ
⊢ Function.Injective ↑σ
Tactic:
exact Function.LeftInverse.injective s1
Proof state after:
no goals
Theorem: MM0.Instantiation.is_surjective
Proof state before:
σ : Instantiation
⊢ Function.Surjective ↑σ
Tactic:
obtain ⟨σ', a1⟩ := σ.2
Proof state after:
case intro
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Theorem: MM0.Instantiation.is_surjective
Proof state before:
case intro
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Tactic:
cases a1
Proof state after:
case intro.intro
σ : Instantiation
σ' : VarName → VarName
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Theorem: MM0.Instantiation.is_surjective
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Tactic:
case intro a1_left a1_right =>
  have s1 : Function.RightInverse σ' σ.1 := congr_fun a1_left
  exact Function.RightInverse.surjective s1
Proof state after:
no goals
Theorem: MM0.Instantiation.is_surjective
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Tactic:
have s1 : Function.RightInverse σ' σ.1 := congr_fun a1_left
Proof state after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.RightInverse σ' ↑σ
⊢ Function.Surjective ↑σ
Theorem: MM0.Instantiation.is_surjective
Proof state before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.RightInverse σ' ↑σ
⊢ Function.Surjective ↑σ
Tactic:
exact Function.RightInverse.surjective s1
Proof state after:
no goals
Theorem: MM0.Instantiation.is_bijective
Proof state before:
σ : Instantiation
⊢ Function.Bijective ↑σ
Tactic:
unfold Function.Bijective
Proof state after:
σ : Instantiation
⊢ Function.Injective ↑σ ∧ Function.Surjective ↑σ
Theorem: MM0.Instantiation.is_bijective
Proof state before:
σ : Instantiation
⊢ Function.Injective ↑σ ∧ Function.Surjective ↑σ
Tactic:
constructor
Proof state after:
case left
σ : Instantiation
⊢ Function.Injective ↑σ

case right
σ : Instantiation
⊢ Function.Surjective ↑σ
Theorem: MM0.Instantiation.is_bijective
Proof state before:
case left
σ : Instantiation
⊢ Function.Injective ↑σ
Tactic:
exact Instantiation.is_injective σ
Proof state after:
no goals
Theorem: MM0.Instantiation.is_bijective
Proof state before:
case right
σ : Instantiation
⊢ Function.Surjective ↑σ
Tactic:
exact Instantiation.is_surjective σ
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
F : Formula
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ F) = sub (σ.comp σ') meta_var_ F
Tactic:
induction F
Proof 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✝)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ true_) = sub (σ.comp σ') meta_var_ true_
Tactic:
case true_ =>
  rfl
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
X : MetaVarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (meta_var_ X)) = sub (σ.comp σ') meta_var_ (meta_var_ X)
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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]
Proof state after:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑(σ.comp σ')) xs)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
x y : VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (eq_ x y)) = sub (σ.comp σ') meta_var_ (eq_ x y)
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
⊢ sub σ meta_var_ (sub σ' meta_var_ true_) = sub (σ.comp σ') meta_var_ true_
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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]
Proof 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_
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof 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_
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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]
Proof 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)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof 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
Proof 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)