Theorem: LO.FirstOrder.satisfiable_lMap (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₁
s : Satisfiable T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
Tactic:
rcases s with ⟨⟨M, i, s⟩, hM⟩
State after:
case intro.mk
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)

State before:
case intro.mk
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
Tactic:
exact ⟨⟨M, i, s.extendStructure Φ⟩, by
  simp[Semantics.realizeSet_iff]
  intro σ hσ
  exact (Structure.extendStructure.models_lMap Φ injf injr s σ).mpr (hM.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₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧* ⇑(Semiformula.lMap Φ) '' T
Tactic:
simp[Semantics.realizeSet_iff]
State after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ ∀ a ∈ T, { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) a

State before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ ∀ a ∈ T, { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (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₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) σ

State before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) σ
Tactic:
exact (Structure.extendStructure.models_lMap Φ injf injr s σ).mpr (hM.realize hσ)
State after:
no goals