Theorem: LO.FirstOrder.lMap_models_lMap (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
⊢ Theory.lMap Φ T ⊨[Struc L₂] (Semiformula.lMap Φ) σ
Tactic:
intro s hM
State after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
⊢ s ⊧ (Semiformula.lMap Φ) σ

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
⊢ s ⊧ (Semiformula.lMap Φ) σ
Tactic:
have : (s.struc.lMap Φ).toStruc ⊧ σ :=
  h ⟨fun _ hq => Semiformula.models_lMap.mp <| hM.realize (Set.mem_image_of_mem _ hq)⟩
State after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
this : (Structure.lMap Φ s.struc).toStruc ⊧ σ
⊢ s ⊧ (Semiformula.lMap Φ) σ

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
this : (Structure.lMap Φ s.struc).toStruc ⊧ σ
⊢ s ⊧ (Semiformula.lMap Φ) σ
Tactic:
exact Semiformula.models_lMap.mpr this
State after:
no goals