L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : lift (#↑s) ≤ lift (#M)
this : Inhabited M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : lift (#↑s) ≤ lift (#M)
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this : Inhabited M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : lift (#↑s) ≤ lift (#M)
this : Inhabited M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
rw [Cardinal.lift_mk_le'] at h
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this : Inhabited M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
letI : (constantsOn α).Structure M := constantsOn.structure (Function.extend (↑) h.some default)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝¹ : Inhabited M
this✝ : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
this : M ⊨ LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
have : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s := by
  refine' ((LHom.onTheory_model _ _).2 inferInstance).union _
  rw [model_distinctConstantsTheory]
  refine' fun a as b bs ab => _
  rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
  exact
    h.some.injective
      ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
        (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))
no goals
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝¹ : Inhabited M
this✝ : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
this : M ⊨ LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
exact Model.isSatisfiable M
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ M ⊨ distinctConstantsTheory L s
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ M ⊨ LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s
refine' ((LHom.onTheory_model _ _).2 inferInstance).union _
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ Set.InjOn (fun i => ↑(Language.con L i)) s
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ M ⊨ distinctConstantsTheory L s
rw [model_distinctConstantsTheory]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(Language.con L i)) a = (fun i => ↑(Language.con L i)) b
⊢ a = b
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ Set.InjOn (fun i => ↑(Language.con L i)) s
refine' fun a as b bs ab => _
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(Language.con L i)) a = (fun i => ↑(Language.con L i)) b
⊢ { val := a, property := as } = { val := b, property := bs }
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(Language.con L i)) a = (fun i => ↑(Language.con L i)) b
⊢ a = b
rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
no goals
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(Language.con L i)) a = (fun i => ↑(Language.con L i)) b
⊢ { val := a, property := as } = { val := b, property := bs }
exact
  h.some.injective
    ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
      (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))