[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
hx : ∀ (k : ℕ), k < Nat.zero → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero ≤ y Nat.zero
[PROOFSTEP]
exact h₀
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) ≤ y (Nat.succ n)
[PROOFSTEP]
refine' (hx _ n.lt_succ_self).trans ((hf $ ihn _ _).trans (hy _ n.lt_succ_self))
[GOAL]
case succ.refine'_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
case succ.refine'_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
[PROOFSTEP]
exact fun k hk => hx _ (hk.trans n.lt_succ_self)
[GOAL]
case succ.refine'_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
[PROOFSTEP]
exact fun k hk => hy _ (hk.trans n.lt_succ_self)
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn : 0 < n
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn✝ : 0 < n
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
hn : 0 < Nat.zero
hx : ∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero < y Nat.zero
[PROOFSTEP]
exact hn.false.elim
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < Nat.succ n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) < y (Nat.succ n)
[PROOFSTEP]
suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans $ hy n n.lt_succ_self)
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < Nat.succ n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
[PROOFSTEP]
cases n with
| zero => exact h₀
| succ n =>
  refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le <;> exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < Nat.succ n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
[PROOFSTEP]
cases n with
| zero => exact h₀
| succ n =>
  refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le <;> exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ.zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn✝ : 0 < n
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
ihn :
  0 < Nat.zero →
    (∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)) → x Nat.zero < y Nat.zero
hn : 0 < Nat.succ Nat.zero
hx : ∀ (k : ℕ), k < Nat.succ Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero ≤ y Nat.zero
[PROOFSTEP]

| zero => exact h₀
[GOAL]
case succ.zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn✝ : 0 < n
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
ihn :
  0 < Nat.zero →
    (∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)) → x Nat.zero < y Nat.zero
hn : 0 < Nat.succ Nat.zero
hx : ∀ (k : ℕ), k < Nat.succ Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero ≤ y Nat.zero
[PROOFSTEP]
exact h₀
[GOAL]
case succ.succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) ≤ y (Nat.succ n)
[PROOFSTEP]

| succ n =>
  refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le <;> exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ.succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) ≤ y (Nat.succ n)
[PROOFSTEP]
refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le
[GOAL]
case succ.succ.refine'_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < Nat.succ n
⊢ k < Nat.succ (Nat.succ n)
[PROOFSTEP]
exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ.succ.refine'_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < Nat.succ n
⊢ k < Nat.succ (Nat.succ n)
[PROOFSTEP]
exact hk.trans n.succ.lt_succ_self
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero < y Nat.zero
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n✝ : ℕ
hx : ∀ (k : ℕ), k < Nat.succ n✝ → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n✝ → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n✝) < y (Nat.succ n✝)
[PROOFSTEP]
exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x
[PROOFSTEP]
apply hf.seq_le_seq n
[GOAL]
case h₀
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
[PROOFSTEP]
intros
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)
[PROOFSTEP]
intros
[GOAL]
case hy
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x
[PROOFSTEP]
intros
[GOAL]
case h₀
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
[PROOFSTEP]
simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ (h ∘ g^[k✝ + 1]) x ≤ f ((h ∘ g^[k✝]) x)
[PROOFSTEP]
simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
[GOAL]
case hy
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ f ((f^[k✝] ∘ h) x) ≤ (f^[k✝ + 1] ∘ h) x
[PROOFSTEP]
simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
[PROOFSTEP]
case hx => exact H _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
[PROOFSTEP]
case hx => exact H _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
[PROOFSTEP]
exact H _
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
⊢ id ≤ f^[n]
[PROOFSTEP]
simpa only [iterate_id] using monotone_id.iterate_le_of_le h n
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)
[PROOFSTEP]
exact h _
[GOAL]
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x
[PROOFSTEP]
apply hf.seq_le_seq n
[GOAL]
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x
[PROOFSTEP]
rfl
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
[PROOFSTEP]
intros
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
[PROOFSTEP]
intros
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) ≤ g^[k✝ + 1] x
[PROOFSTEP]
simp [h.iterate_right _ _, hg.iterate _ hx]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x
[PROOFSTEP]
apply hf.seq_pos_lt_seq_of_le_of_lt hn
[GOAL]
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x
[PROOFSTEP]
rfl
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
[PROOFSTEP]
intros
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
[PROOFSTEP]
intros
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) < g^[k✝ + 1] x
[PROOFSTEP]
simp [h.iterate_right _ _, hg.iterate _ hx]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
rcases lt_trichotomy (f x) (g x) with (H | H | H)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
simp only [*, iterate_pos_lt_of_map_lt]
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x
[PROOFSTEP]
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt' hg hf hn)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x
[PROOFSTEP]
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x = g^[n] x ↔ f x = g x
[PROOFSTEP]
simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn, h.symm.iterate_pos_le_iff_map_le' hg hf hn]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x
[PROOFSTEP]
rw [iterate_succ_apply]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)
[PROOFSTEP]
exact hf.iterate n hx
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x
[PROOFSTEP]
rw [iterate_succ_apply]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)
[PROOFSTEP]
exact hf.iterate n hx


[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
[PROOFSTEP]
rw [SupIrred, not_and_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (IsMin a ∨ Exists fun ⦃b⦄ => Exists fun ⦃c⦄ => b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
[PROOFSTEP]
rw [exists₂_congr]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
[PROOFSTEP]
simp (config := { contextual := true }) [@eq_comm _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
[PROOFSTEP]
rw [SupPrime, not_and_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (IsMin a ∨ Exists fun ⦃b⦄ => Exists fun ⦃c⦄ => a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔
    IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
b c : α
ha : b ⊔ c = a
⊢ b = a ∨ c = a
[PROOFSTEP]
simpa [← ha] using h ha.ge
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
⊢ a ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred ⊥
⊢ False
[PROOFSTEP]
exact not_supIrred_bot ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime ⊥
⊢ False
[PROOFSTEP]
exact not_supPrime_bot ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : sup s f = a
⊢ ∃ i, i ∈ s ∧ f i = a
[PROOFSTEP]
classical
induction' s using Finset.induction with i s _ ih
· simpa [ha.ne_bot] using h.symm
simp only [exists_prop, exists_mem_insert] at ih ⊢
rw [sup_insert] at h
exact (ha.2 h).imp_right ih
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : sup s f = a
⊢ ∃ i, i ∈ s ∧ f i = a
[PROOFSTEP]
induction' s using Finset.induction with i s _ ih
[GOAL]
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s f = a
h : sup ∅ f = a
⊢ ∃ i, i ∈ ∅ ∧ f i = a
[PROOFSTEP]
simpa [ha.ne_bot] using h.symm
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s✝ f = a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : sup s f = a → ∃ i, i ∈ s ∧ f i = a
h : sup (insert i s) f = a
⊢ ∃ i_1, i_1 ∈ insert i s ∧ f i_1 = a
[PROOFSTEP]
simp only [exists_prop, exists_mem_insert] at ih ⊢
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s✝ f = a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : sup s f = a → ∃ i, i ∈ s ∧ f i = a
h : sup (insert i s) f = a
⊢ f i = a ∨ ∃ x, x ∈ s ∧ f x = a
[PROOFSTEP]
rw [sup_insert] at h
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s✝ f = a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : sup s f = a → ∃ i, i ∈ s ∧ f i = a
h : f i ⊔ sup s f = a
⊢ f i = a ∨ ∃ x, x ∈ s ∧ f x = a
[PROOFSTEP]
exact (ha.2 h).imp_right ih
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup s f ↔ ∃ i, i ∈ s ∧ a ≤ f i
[PROOFSTEP]
classical
induction' s using Finset.induction with i s _ ih
· simp [ha.ne_bot]
· simp only [exists_prop, exists_mem_insert, sup_insert, ha.le_sup, ih]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup s f ↔ ∃ i, i ∈ s ∧ a ≤ f i
[PROOFSTEP]
induction' s using Finset.induction with i s _ ih
[GOAL]
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup ∅ f ↔ ∃ i, i ∈ ∅ ∧ a ≤ f i
[PROOFSTEP]
simp [ha.ne_bot]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupPrime a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : a ≤ sup s f ↔ ∃ i, i ∈ s ∧ a ≤ f i
⊢ a ≤ sup (insert i s) f ↔ ∃ i_1, i_1 ∈ insert i s ∧ a ≤ f i_1
[PROOFSTEP]
simp only [exists_prop, exists_mem_insert, sup_insert, ha.le_sup, ih]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
classical
apply WellFoundedLT.induction a _
clear a
rintro a ih
by_cases ha : SupIrred a
· exact ⟨{ a }, by simp [ha]⟩
rw [not_supIrred] at ha
obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
· exact ⟨∅, by simp [ha.eq_bot]⟩
obtain ⟨s, rfl, hs⟩ := ih _ hb
obtain ⟨t, rfl, ht⟩ := ih _ hc
exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
apply WellFoundedLT.induction a _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
⊢ ∀ (x : α),
    (∀ (y : α), y < x → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) →
      ∃ s, sup s id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
clear a
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
⊢ ∀ (x : α),
    (∀ (y : α), y < x → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) →
      ∃ s, sup s id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
rintro a ih
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
by_cases ha : SupIrred a
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
exact ⟨{ a }, by simp [ha]⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ sup {a} id = a ∧ ∀ ⦃b : α⦄, b ∈ {a} → SupIrred b
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
rw [not_supIrred] at ha
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
[GOAL]
case neg.inl
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
exact ⟨∅, by simp [ha.eq_bot]⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ sup ∅ id = a ∧ ∀ ⦃b : α⦄, b ∈ ∅ → SupIrred b
[PROOFSTEP]
simp [ha.eq_bot]
[GOAL]
case neg.inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b✝ c✝ : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
b c : α
ih : ∀ (y : α), y < b ⊔ c → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : b < b ⊔ c
hc : c < b ⊔ c
⊢ ∃ s, sup s id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
obtain ⟨s, rfl, hs⟩ := ih _ hb
[GOAL]
case neg.inr.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b c✝ : α
inst✝¹ : OrderBot α
s✝ : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
c : α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ih : ∀ (y : α), y < sup s id ⊔ c → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : sup s id < sup s id ⊔ c
hc : c < sup s id ⊔ c
⊢ ∃ s_1, sup s_1 id = sup s id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
[PROOFSTEP]
obtain ⟨t, rfl, ht⟩ := ih _ hc
[GOAL]
case neg.inr.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b c : α
inst✝¹ : OrderBot α
s✝ : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
t : Finset α
ht : ∀ ⦃b : α⦄, b ∈ t → SupIrred b
ih : ∀ (y : α), y < sup s id ⊔ sup t id → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : sup s id < sup s id ⊔ sup t id
hc : sup t id < sup s id ⊔ sup t id
⊢ ∃ s_1, sup s_1 id = sup s id ⊔ sup t id ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
[PROOFSTEP]
exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeInf α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
b c : α
ha : b ⊓ c = a
⊢ b = a ∨ c = a
[PROOFSTEP]
simpa [← ha] using h ha.le
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
a b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfIrred a
⊢ a ≠ ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfIrred ⊤
⊢ False
[PROOFSTEP]
exact not_infIrred_top ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
a b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfPrime a
⊢ a ≠ ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfPrime ⊤
⊢ False
[PROOFSTEP]
exact not_infPrime_top ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
[PROOFSTEP]
simp_rw [← inf_eq_left, inf_sup_left]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
[PROOFSTEP]
exact @h _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
[PROOFSTEP]
simp_rw [← sup_eq_left, sup_inf_left]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
[PROOFSTEP]
exact @h _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a x✝¹ x✝ : α
⊢ x✝¹ ⊔ x✝ = a → x✝¹ = a ∨ x✝ = a
[PROOFSTEP]
simpa only [sup_eq_max, max_eq_iff] using Or.imp And.left And.left
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = a → x✝¹ = a ∨ x✝ = a
[PROOFSTEP]
simpa only [inf_eq_min, min_eq_iff] using Or.imp And.left And.left


[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
⊢ IsSatisfiable (LHom.onTheory φ T) ↔ IsSatisfiable T
[PROOFSTEP]
classical
refine' ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => _⟩
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
exact Model.isSatisfiable (h'.some.defaultExpansion h)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
⊢ IsSatisfiable (LHom.onTheory φ T) ↔ IsSatisfiable T
[PROOFSTEP]
refine' ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => _⟩
[GOAL]
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)
[PROOFSTEP]
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
[GOAL]
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)
[PROOFSTEP]
exact Model.isSatisfiable (h'.some.defaultExpansion h)
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
⊢ IsSatisfiable T
[PROOFSTEP]
classical
set M : Finset T → Type max u v := fun T0 : Finset T =>
  (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
have h' : M' ⊨ T := by
  refine' ⟨fun φ hφ => _⟩
  rw [Ultraproduct.sentence_realize]
  refine'
    Filter.Eventually.filter_mono (Ultrafilter.of_le _)
      (Filter.eventually_atTop.2
        ⟨{⟨φ, hφ⟩}, fun s h' => Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T)) _⟩)
  simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe, Subtype.exists,
    Subtype.coe_mk, exists_and_right, exists_eq_right]
  exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
exact ⟨ModelType.of T M'⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
⊢ IsSatisfiable T
[PROOFSTEP]
set M : Finset T → Type max u v := fun T0 : Finset T =>
  (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
⊢ IsSatisfiable T
[PROOFSTEP]
let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
⊢ IsSatisfiable T
[PROOFSTEP]
have h' : M' ⊨ T := by
  refine' ⟨fun φ hφ => _⟩
  rw [Ultraproduct.sentence_realize]
  refine'
    Filter.Eventually.filter_mono (Ultrafilter.of_le _)
      (Filter.eventually_atTop.2
        ⟨{⟨φ, hφ⟩}, fun s h' => Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T)) _⟩)
  simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe, Subtype.exists,
    Subtype.coe_mk, exists_and_right, exists_eq_right]
  exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
⊢ M' ⊨ T
[PROOFSTEP]
refine' ⟨fun φ hφ => _⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
⊢ M' ⊨ φ
[PROOFSTEP]
rw [Ultraproduct.sentence_realize]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
⊢ ∀ᶠ (a : Finset ↑T) in ↑(Ultrafilter.of Filter.atTop), M a ⊨ φ
[PROOFSTEP]
refine'
  Filter.Eventually.filter_mono (Ultrafilter.of_le _)
    (Filter.eventually_atTop.2
      ⟨{⟨φ, hφ⟩}, fun s h' => Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T)) _⟩)
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {{ val := φ, property := hφ }}
⊢ φ ∈ ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) s)
[PROOFSTEP]
simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe, Subtype.exists,
  Subtype.coe_mk, exists_and_right, exists_eq_right]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {{ val := φ, property := hφ }}
⊢ ∃ x, { val := φ, property := (_ : φ ∈ T) } ∈ s
[PROOFSTEP]
exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
h' : M' ⊨ T
⊢ IsSatisfiable T
[PROOFSTEP]
exact ⟨ModelType.of T M'⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (i : ι), IsSatisfiable (T i)
[PROOFSTEP]
refine' ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => _⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
[PROOFSTEP]
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ ⋃ (i : ι), T i → IsSatisfiable ↑T0
[PROOFSTEP]
intro T0 hT0
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑T0
[PROOFSTEP]
obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
i : ι
hi : ↑T0 ⊆ T i
⊢ IsSatisfiable ↑T0
[PROOFSTEP]
exact (h' i).mono hi
[GOAL]
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)
[PROOFSTEP]
haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
[GOAL]
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)
[PROOFSTEP]
rw [Cardinal.lift_mk_le'] at h
[GOAL]
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)
[PROOFSTEP]
letI : (constantsOn α).Structure M := constantsOn.structure (Function.extend (↑) h.some default)
[GOAL]
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)
[PROOFSTEP]
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⟩)))
[GOAL]
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
[PROOFSTEP]
refine' ((LHom.onTheory_model _ _).2 inferInstance).union _
[GOAL]
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
[PROOFSTEP]
rw [model_distinctConstantsTheory]
[GOAL]
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
[PROOFSTEP]
refine' fun a as b bs ab => _
[GOAL]
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
[PROOFSTEP]
rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
[GOAL]
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 }
[PROOFSTEP]
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⟩)))
[GOAL]
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)
[PROOFSTEP]
exact Model.isSatisfiable M
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
classical
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
·
  exact fun t =>
    isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
      ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans (aleph0_le_lift.2 (aleph0_le_mk M)))
· apply Monotone.directed_le
  refine' monotone_const.union (monotone_distinctConstantsTheory.comp _)
  simp only [Finset.coe_map, Function.Embedding.coe_subtype]
  exact
    Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s)) Set.monotone_image fun _ _ =>
      Finset.coe_subset.2
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∀ (i : Finset ↑s),
    IsSatisfiable
      (LHom.onTheory (lhomWithConstants L α) T ∪
        distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i))
[PROOFSTEP]
exact fun t =>
  isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
    ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans (aleph0_le_lift.2 (aleph0_le_mk M)))
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
apply Monotone.directed_le
[GOAL]
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
refine' monotone_const.union (monotone_distinctConstantsTheory.comp _)
[GOAL]
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
simp only [Finset.coe_map, Function.Embedding.coe_subtype]
[GOAL]
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => (fun a => ↑a) '' ↑i
[PROOFSTEP]
exact
  Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s)) Set.monotone_image fun _ _ =>
    Finset.coe_subset.2
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∃ N, lift κ ≤ #↑N
[PROOFSTEP]
obtain ⟨N⟩ := isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ ∃ N, lift κ ≤ #↑N
[PROOFSTEP]
refine' ⟨(N.is_model.mono (Set.subset_union_left _ _)).bundled.reduct _, _⟩
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ lift κ ≤
    #↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T)))
[PROOFSTEP]
haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono (Set.subset_union_right _ _)
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤
    #↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T)))
[PROOFSTEP]
rw [ModelType.reduct_Carrier, coe_of]
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤ #↑N
[PROOFSTEP]
refine' _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) _
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift #(Quotient.out κ) ≤ #↑N
[PROOFSTEP]
rw [← mk_univ]
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift #↑Set.univ ≤ #↑N
[PROOFSTEP]
refine' (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 _)
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (lift #↑N) ≤ lift #↑N
[PROOFSTEP]
rw [lift_lift]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
[PROOFSTEP]
classical
refine' ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _), fun h => _⟩
rw [isSatisfiable_iff_isFinitelySatisfiable]
intro s hs
rw [Set.iUnion_eq_iUnion_finset] at hs
obtain ⟨t, ht⟩ :=
  Directed.exists_mem_subset_of_finset_subset_biUnion
    (by
      exact
        Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
          Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩)
    hs
exact (h t).mono ht
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
[PROOFSTEP]
refine' ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _), fun h => _⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
[PROOFSTEP]
rw [isSatisfiable_iff_isFinitelySatisfiable]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsFinitelySatisfiable (⋃ (i : ι), T i)
[PROOFSTEP]
intro s hs
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑s
[PROOFSTEP]
rw [Set.iUnion_eq_iUnion_finset] at hs
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
[PROOFSTEP]
obtain ⟨t, ht⟩ :=
  Directed.exists_mem_subset_of_finset_subset_biUnion
    (by
      exact
        Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
          Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩)
    hs
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), T i_1
[PROOFSTEP]
exact
  Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
    Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
[PROOFSTEP]
exact (h t).mono ht
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
⊢ lift #↑∅ ≤ lift κ
[PROOFSTEP]
simp
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
[PROOFSTEP]
have : Small.{w} S := by
  rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
  exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
⊢ Small.{w, w'} { x // x ∈ S }
[PROOFSTEP]
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
⊢ Small.{w, w'} { x // x ∈ S }
[PROOFSTEP]
exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
this : Small.{w, w'} { x // x ∈ S }
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
[PROOFSTEP]
refine'
  ⟨(equivShrink S).bundledInduced L, ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
    lift_inj.1 (_root_.trans _ hS)⟩
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
this : Small.{w, w'} { x // x ∈ S }
⊢ lift #↑(Equiv.bundledInduced L (equivShrink { x // x ∈ S })) = lift #{ x // x ∈ S }
[PROOFSTEP]
simp only [Equiv.bundledInduced_α, lift_mk_shrink']
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N0, hN0⟩ := (L.elementaryDiagram M).exists_large_model_of_infinite_model κ M
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, ⟨NN0⟩, hN⟩ :=
  exists_elementaryEmbedding_card_eq_of_le (L[[M]]) N0 κ
    (aleph0_le_lift.1 ((aleph0_le_lift.2 (aleph0_le_mk M)).trans h2))
    (by
      simp only [card_withConstants, lift_add, lift_lift]
      rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
      rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
      exact ⟨h2, h1⟩)
    (hN0.trans (by rw [← lift_umax', lift_id]))
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift (card (L[[M]])) ≤ lift κ
[PROOFSTEP]
simp only [card_withConstants, lift_add, lift_lift]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift (card L) + lift #M ≤ lift κ
[PROOFSTEP]
rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift #M ≤ lift κ ∧ lift (card L) ≤ lift κ
[PROOFSTEP]
rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift #M ≤ lift κ ∧ lift (card L) ≤ lift κ
[PROOFSTEP]
exact ⟨h2, h1⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ #↑N0 ≤ lift #↑N0
[PROOFSTEP]
rw [← lift_umax', lift_id]
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
letI := (lhomWithConstants L M).reduct N
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : Structure L ↑N := LHom.reduct (lhomWithConstants L M) ↑N
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
haveI h : N ⊨ L.elementaryDiagram M := (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : Structure L ↑N := LHom.reduct (lhomWithConstants L M) ↑N
h : ↑N ⊨ elementaryDiagram L M
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
refine' ⟨Bundled.of N, ⟨_⟩, hN⟩
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : Structure L ↑N := LHom.reduct (lhomWithConstants L M) ↑N
h : ↑N ⊨ elementaryDiagram L M
⊢ M ↪ₑ[L] ↑(Bundled.of ↑N)
[PROOFSTEP]
apply ElementaryEmbedding.ofModelsElementaryDiagram L M N
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M)
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ ≤ lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inl h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
  exact ⟨N, Or.inl hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inl h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
  exact ⟨N, Or.inl hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift #M
N : Bundled (Structure L)
hN1 : Nonempty (↑N ↪ₑ[L] M)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, Or.inl hN1, hN2⟩
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inr h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
  exact ⟨N, Or.inr hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inr h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
  exact ⟨N, Or.inr hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift #M
N : Bundled (Structure L)
hN1 : Nonempty (M ↪ₑ[L] ↑N)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, Or.inr hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2
[GOAL]
case intro.intro.inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : #↑N = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩
[GOAL]
case intro.intro.inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
cases h with
| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
cases h with
| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ
[PROOFSTEP]

| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
haveI := MI
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI this : Infinite ↑M
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
[GOAL]
case intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : ModelType T
MI this : Infinite ↑M
N : Bundled (Structure L)
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift (card L) ≤ lift #↑N
⊢ ∃ N_1, #↑N_1 = #↑N
[PROOFSTEP]
haveI : Nonempty N := hN.nonempty
[GOAL]
case intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : ModelType T
MI this✝ : Infinite ↑M
N : Bundled (Structure L)
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift (card L) ≤ lift #↑N
this : Nonempty ↑N
⊢ ∃ N_1, #↑N_1 = #↑N
[PROOFSTEP]
exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ T ⊨ᵇ φ ↔ ¬IsSatisfiable (T ∪ {Formula.not φ})
[PROOFSTEP]
rw [models_sentence_iff, IsSatisfiable]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (M : ModelType T), ↑M ⊨ φ) ↔ ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
[PROOFSTEP]
refine'
  ⟨fun h1 h2 =>
    (Sentence.realize_not _).1
      (realize_sentence_of_mem (T ∪ {Formula.not φ}) (Set.subset_union_right _ _ (Set.mem_singleton _)))
      (h1 (h2.some.subtheoryModel (Set.subset_union_left _ _))),
    fun h M => _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
M : ModelType T
⊢ ↑M ⊨ φ
[PROOFSTEP]
contrapose! h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ¬↑M ⊨ φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
[PROOFSTEP]
rw [← Sentence.realize_not] at h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
[PROOFSTEP]
refine'
  ⟨{  Carrier := M
      is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => _⟩ }⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ
[PROOFSTEP]
rw [Set.mem_singleton_iff.1 h']
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ
[PROOFSTEP]
exact h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
[PROOFSTEP]
rw [models_iff_not_satisfiable] at h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬IsSatisfiable (T ∪ {Formula.not φ})
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
[PROOFSTEP]
contrapose! h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ IsSatisfiable (T ∪ {Formula.not φ})
[PROOFSTEP]
have : M ⊨ T ∪ {Formula.not φ} :=
  by
  simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp, Sentence.realize_not]
  rw [← model_iff]
  exact ⟨h, inferInstance⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}
[PROOFSTEP]
simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp, Sentence.realize_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ (a : Sentence L), a ∈ T → M ⊨ a
[PROOFSTEP]
rw [← model_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T
[PROOFSTEP]
exact ⟨h, inferInstance⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ IsSatisfiable (T ∪ {Formula.not φ})
[PROOFSTEP]
exact Model.isSatisfiable M
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ
[PROOFSTEP]
simp only [models_iff_not_satisfiable]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ ¬IsSatisfiable (T ∪ {Formula.not φ}) ↔ ∃ T0, ↑T0 ⊆ T ∧ ¬IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
rw [← not_iff_not, not_not, isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ¬∃ T0, ↑T0 ⊆ T ∧ ¬IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
push_neg
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
letI := Classical.decEq (Sentence L)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) →
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
intro h T0 hT0
[GOAL]
case mp
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T
⊢ IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
simpa using
  h (T0 ∪ {Formula.not φ})
    (by
      simp only [Finset.coe_union, Finset.coe_singleton]
      exact Set.union_subset_union hT0 (Set.Subset.refl _))
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T
⊢ ↑(T0 ∪ {Formula.not φ}) ⊆ T ∪ {Formula.not φ}
[PROOFSTEP]
simp only [Finset.coe_union, Finset.coe_singleton]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T
⊢ ↑T0 ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}
[PROOFSTEP]
exact Set.union_subset_union hT0 (Set.Subset.refl _)
[GOAL]
case mpr
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})) →
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
[PROOFSTEP]
intro h T0 hT0
[GOAL]
case mpr
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ IsSatisfiable ↑T0
[PROOFSTEP]
exact IsSatisfiable.mono (h (T0.erase (Formula.not φ)) (by simpa using hT0)) (by simp)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑(Finset.erase T0 (Formula.not φ)) ⊆ T
[PROOFSTEP]
simpa using hT0
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑T0 ⊆ ↑(Finset.erase T0 (Formula.not φ)) ∪ {Formula.not φ}
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
[PROOFSTEP]
cases' h.2 φ with hφ hφn
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
[PROOFSTEP]
simp only [hφ, not_true, iff_false_iff]
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ
[PROOFSTEP]
rw [models_sentence_iff, not_forall]
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ
[PROOFSTEP]
refine' ⟨h.1.some, _⟩
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ Formula.not φ
[PROOFSTEP]
simp only [Sentence.realize_not, Classical.not_not]
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ φ
[PROOFSTEP]
exact models_sentence_iff.1 hφ _
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
[PROOFSTEP]
simp only [hφn, true_iff_iff]
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ ¬T ⊨ᵇ φ
[PROOFSTEP]
intro hφ
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False
[PROOFSTEP]
rw [models_sentence_iff] at *
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : ∀ (M : ModelType T), ↑M ⊨ Formula.not φ
hφ : ∀ (M : ModelType T), ↑M ⊨ φ
⊢ False
[PROOFSTEP]
exact hφn h.1.some (hφ _)
[GOAL]
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 ⊨ᵇ φ
[PROOFSTEP]
cases' h.2 φ with hφ hφn
[GOAL]
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 ⊨ᵇ φ
[PROOFSTEP]
exact iff_of_true (hφ.realize_sentence M) hφ
[GOAL]
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 ⊨ᵇ φ
[PROOFSTEP]
exact iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M)) ((h.models_not_iff φ).1 hφn)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ φ ∈ T
[PROOFSTEP]
refine' (h.mem_or_not_mem φ).resolve_right fun con => _
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False
[PROOFSTEP]
rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : ¬IsSatisfiable T
con : Formula.not φ ∈ T
⊢ False
[PROOFSTEP]
exact hφ h.1
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : BoundedFormula L α n
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ φ) v xs
[PROOFSTEP]
rw [BoundedFormula.realize_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (ψ ⇔ φ) v xs
[PROOFSTEP]
rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ ψ) v xs
[PROOFSTEP]
exact h M v xs
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
[PROOFSTEP]
have h1' := h1 M v xs
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
[PROOFSTEP]
have h2' := h2 M v xs
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
h2' : BoundedFormula.Realize (ψ ⇔ θ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
[PROOFSTEP]
rw [BoundedFormula.realize_iff] at *
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize ψ v xs
h2' : BoundedFormula.Realize ψ v xs ↔ BoundedFormula.Realize θ v xs
⊢ BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize θ v xs
[PROOFSTEP]
exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ SemanticallyEquivalent T (∀'φ) (∀'ψ)
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_all]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    (∀ (a : ↑M), BoundedFormula.Realize φ v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), BoundedFormula.Realize ψ v (Fin.snoc xs a)
[PROOFSTEP]
exact fun M v xs => forall_congr' fun a => h.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ SemanticallyEquivalent T (∃'φ) (∃'ψ)
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_ex]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    (∃ a, BoundedFormula.Realize φ v (Fin.snoc xs a)) ↔ ∃ a, BoundedFormula.Realize ψ v (Fin.snoc xs a)
[PROOFSTEP]
exact fun M v xs => exists_congr fun a => h.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
⊢ SemanticallyEquivalent T (∼φ) ∼ψ
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M), ¬BoundedFormula.Realize φ v xs ↔ ¬BoundedFormula.Realize ψ v xs
[PROOFSTEP]
exact fun M v xs => not_congr h.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ SemanticallyEquivalent T (φ ⟹ φ') (ψ ⟹ ψ')
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_imp]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    BoundedFormula.Realize φ v xs → BoundedFormula.Realize φ' v xs ↔
      BoundedFormula.Realize ψ v xs → BoundedFormula.Realize ψ' v xs
[PROOFSTEP]
exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w
inst✝ : Structure L M
φ : Sentence L
⊢ φ ∈ completeTheory L M ∨ Formula.not φ ∈ completeTheory L M
[PROOFSTEP]
simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ ∼∼φ) v xs
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⟹ ψ ⇔ ∼φ ⊔ ψ) v xs
[PROOFSTEP]
simp [imp_iff_not_or]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⊔ ψ ⇔ ∼(∼φ ⊓ ∼ψ)) v xs
[PROOFSTEP]
simp [imp_iff_not_or]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⊓ ψ ⇔ ∼(∼φ ⊔ ∼ψ)) v xs
[PROOFSTEP]
simp [and_iff_not_or_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ✝ ψ : BoundedFormula L α n
φ : BoundedFormula L α (n + 1)
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (∀'φ ⇔ ∼(∃'∼φ)) v xs
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ✝ ψ : BoundedFormula L α n
φ : BoundedFormula L α (n + 1)
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (∃'φ ⇔ ∼(∀'∼φ)) v xs
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ ∀'liftAt 1 n φ) v xs
[PROOFSTEP]
skip
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ ∀'liftAt 1 n φ) v xs
[PROOFSTEP]
rw [realize_iff, realize_all_liftAt_one_self]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : BoundedFormula L α n
M : Theory.ModelType ∅
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ toPrenex φ) v xs
[PROOFSTEP]
rw [realize_iff, realize_toPrenex]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ P φ
[PROOFSTEP]
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
h' : ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
⊢ P φ
[PROOFSTEP]
exact (hse φ.semanticallyEquivalent_toPrenex).2 (h' φ.toPrenex_isPrenex)
[GOAL]
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
[PROOFSTEP]
intro m φ hφ
[GOAL]
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
hφ : IsPrenex φ
⊢ P φ
[PROOFSTEP]
induction' hφ with _ _ hφ _ _ _ hφ _ _ _ hφ
[GOAL]
case h'.of_isQF
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
⊢ P φ✝
[PROOFSTEP]
exact hqf hφ
[GOAL]
case h'.all
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∀'φ✝)
[PROOFSTEP]
exact hall hφ
[GOAL]
case h'.ex
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∃'φ✝)
[PROOFSTEP]
exact hex hφ
[GOAL]
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
[PROOFSTEP]
obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
[PROOFSTEP]
rw [Theory.models_sentence_iff, Theory.models_sentence_iff]
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
⊢ (∀ (M : Theory.ModelType T), ↑M ⊨ φ) ∨ ∀ (M : Theory.ModelType T), ↑M ⊨ Formula.not φ
[PROOFSTEP]
by_contra con
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
con : ¬((∀ (M : Theory.ModelType T), ↑M ⊨ φ) ∨ ∀ (M : Theory.ModelType T), ↑M ⊨ Formula.not φ)
⊢ False
[PROOFSTEP]
push_neg at con
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
con : (∃ M, ¬↑M ⊨ φ) ∧ ∃ M, ¬↑M ⊨ Formula.not φ
⊢ False
[PROOFSTEP]
obtain ⟨⟨MF, hMF⟩, MT, hMT⟩ := con
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ¬↑MT ⊨ Formula.not φ
⊢ False
[PROOFSTEP]
rw [Sentence.realize_not, Classical.not_not] at hMT
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
⊢ False
[PROOFSTEP]
refine' hMF _
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
⊢ ↑MF ⊨ φ
[PROOFSTEP]
haveI := hT MT
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this : Infinite ↑MT
⊢ ↑MF ⊨ φ
[PROOFSTEP]
haveI := hT MF
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
⊢ ↑MF ⊨ φ
[PROOFSTEP]
obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2
[GOAL]
case intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled (Structure L)
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
⊢ ↑MF ⊨ φ
[PROOFSTEP]
obtain ⟨NF, MNF, hNF⟩ := exists_elementarilyEquivalent_card_eq L MF κ h1 h2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled (Structure L)
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
NF : Bundled (Structure L)
MNF : ↑MF ≅[L] ↑NF
hNF : #↑NF = κ
⊢ ↑MF ⊨ φ
[PROOFSTEP]
obtain ⟨TF⟩ := h (MNT.toModel T) (MNF.toModel T) hNT hNF
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled (Structure L)
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
NF : Bundled (Structure L)
MNF : ↑MF ≅[L] ↑NF
hNF : #↑NF = κ
TF : ↑(ElementarilyEquivalent.toModel T MNT) ≃[L] ↑(ElementarilyEquivalent.toModel T MNF)
⊢ ↑MF ⊨ φ
[PROOFSTEP]
exact ((MNT.realize_sentence φ).trans ((TF.realize_sentence φ).trans (MNF.realize_sentence φ).symm)).1 hMT
[GOAL]
L : Language
κ : Cardinal.{w}
T✝ : Theory L
T : Theory Language.empty
M N : Theory.ModelType T
hM : #↑M = κ
hN : #↑N = κ
⊢ Nonempty (↑M ≃[Language.empty] ↑N)
[PROOFSTEP]
rw [empty.nonempty_equiv_iff, hM, hN]
[GOAL]
L : Language
κ : Cardinal.{w}
T : Theory L
⊢ lift (card Language.empty) ≤ lift ℵ₀
[PROOFSTEP]
simp