no goals
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
⊢ IsSatisfiable (LHom.onTheory φ T) ↔ IsSatisfiable T
classical
  refine' ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => _⟩
  haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
  exact Model.isSatisfiable (h'.some.defaultExpansion h)
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
h' : IsSatisfiable T
⊢ IsSatisfiable (LHom.onTheory φ T)
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
⊢ IsSatisfiable (LHom.onTheory φ T) ↔ IsSatisfiable T
refine' ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => _⟩
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
h' : IsSatisfiable T
this : Inhabited ↑(Nonempty.some h')
⊢ IsSatisfiable (LHom.onTheory φ T)
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
h' : IsSatisfiable T
⊢ IsSatisfiable (LHom.onTheory φ T)
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
h' : IsSatisfiable T
this : Inhabited ↑(Nonempty.some h')
⊢ IsSatisfiable (LHom.onTheory φ T)
exact Model.isSatisfiable (h'.some.defaultExpansion h)