Theorem: LO.FirstOrder.lMap_models_lMap_iff (Logic/FirstOrder/Completeness/SubLanguage.lean)

State before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ ↔ T ⊨ σ
Tactic:
constructor
State after:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ → T ⊨ σ

case mpr
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ T ⊨ σ → Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ

State before:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ → T ⊨ σ
Tactic:
intro h s₁ hs₁
State after:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ s₁ ⊧ σ

State before:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ s₁ ⊧ σ
Tactic:
exact (Structure.extendStructure.models_lMap Φ injf injr s₁.struc σ).mp $ h
  (by simp[Semantics.realizeSet_iff, Theory.lMap, Semantics.models]
      intro σ hσ; exact (Structure.extendStructure.models_lMap (Φ := Φ) injf injr s₁.struc σ).mpr (hs₁.realize hσ))
State after:
no goals

State before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ (Structure.extendStructure Φ s₁.struc).toStruc ∈ Semantics.models (SmallStruc L₂) (Theory.lMap Φ T)
Tactic:
simp[Semantics.realizeSet_iff, Theory.lMap, Semantics.models]
State after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ ∀ a ∈ T, (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) a

State before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ ∀ a ∈ T, (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) a
Tactic:
intro σ hσ
State after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ✝ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ✝
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) σ

State before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ✝ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ✝
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) σ
Tactic:
exact (Structure.extendStructure.models_lMap (Φ := Φ) injf injr s₁.struc σ).mpr (hs₁.realize hσ)
State after:
no goals

State before:
case mpr
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ T ⊨ σ → Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
Tactic:
exact lMap_models_lMap
State after:
no goals