case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
cases' h.2 φ with hφ hφn
no goals
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
exact iff_of_true (hφ.realize_sentence M) hφ
no goals
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
exact
  iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M))
    ((h.models_not_iff φ).1 hφn)