internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Tactic:
cases h1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E ((sub σ τ phi).imp_ (sub σ τ psi))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E ((sub σ τ phi).imp_ (sub σ τ psi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi →
      Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔
    Holds D I V M E (sub σ τ phi) → Holds D I V M E (sub σ τ psi)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi →
      Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔
    Holds D I V M E (sub σ τ phi) → Holds D I V M E (sub σ τ psi)
Tactic:
congr! 1
Proof state after:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E (sub σ τ phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi)
Theorem: MM0.holds_sub
Proof state before:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)
Tactic:
exact phi_ih V h1_left
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E (sub σ τ phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi)
Tactic:
exact psi_ih V h1_right
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
case intro h2_left h2_right =>
  unfold sub
  simp only [Holds]
  apply forall_congr'
  intro a
  have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
  apply Function.updateITE_comp_right_injective
  apply Instantiation.is_injective
  simp only [← s1]
  exact phi_ih (Function.updateITE V (σ.val x) a) h1
Proof state after:
no goals
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
unfold sub
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (forall_ (↑σ x) (sub σ τ phi))
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (forall_ (↑σ x) (sub σ τ phi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ (∀ (d : D), Holds D I (Function.updateITE (V ∘ ↑σ) x d) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (↑σ x) d) M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ (∀ (d : D), Holds D I (Function.updateITE (V ∘ ↑σ) x d) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (↑σ x) d) M E (sub σ τ phi)
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
      Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
      Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
intro a
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
Proof state after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
apply Function.updateITE_comp_right_injective
Proof state after:
case s1.h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.Injective ↑σ

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Theorem: MM0.holds_sub
Proof state before:
case s1.h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.Injective ↑σ

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
apply Instantiation.is_injective
Proof state after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)