case zero
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
φ✝ : BoundedFormula L α n
v : α → M
φ : BoundedFormula L α Nat.zero
⊢ Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs

case succ
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
φ : BoundedFormula L α n
v : α → M
⊢ Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
induction' n with n ih
no goals
case zero
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
φ✝ : BoundedFormula L α n
v : α → M
φ : BoundedFormula L α Nat.zero
⊢ Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
exact Unique.exists_iff.symm
case succ
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∃ xs a, Realize φ v (snoc xs a)) ↔ ∃ xs, Realize φ v xs
case succ
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
simp only [BoundedFormula.exs, ih, realize_ex]
case succ.mp
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∃ xs a, Realize φ v (snoc xs a)) → ∃ xs, Realize φ v xs

case succ.mpr
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∃ xs, Realize φ v xs) → ∃ xs a, Realize φ v (snoc xs a)
case succ
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∃ xs a, Realize φ v (snoc xs a)) ↔ ∃ xs, Realize φ v xs
constructor
case succ.mp.intro.intro
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
xs : Fin n → M
x : M
h : Realize φ v (snoc xs x)
⊢ ∃ xs, Realize φ v xs
case succ.mp
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∃ xs a, Realize φ v (snoc xs a)) → ∃ xs, Realize φ v xs
rintro ⟨xs, x, h⟩
no goals
case succ.mp.intro.intro
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
xs : Fin n → M
x : M
h : Realize φ v (snoc xs x)
⊢ ∃ xs, Realize φ v xs
exact ⟨_, h⟩
case succ.mpr.intro
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
xs : Fin (Nat.succ n) → M
h : Realize φ v xs
⊢ ∃ xs a, Realize φ v (snoc xs a)
case succ.mpr
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∃ xs, Realize φ v xs) → ∃ xs a, Realize φ v (snoc xs a)
rintro ⟨xs, h⟩
case succ.mpr.intro
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
xs : Fin (Nat.succ n) → M
h : Realize φ v (snoc (init xs) (xs (last n)))
⊢ ∃ xs a, Realize φ v (snoc xs a)
case succ.mpr.intro
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
xs : Fin (Nat.succ n) → M
h : Realize φ v xs
⊢ ∃ xs a, Realize φ v (snoc xs a)
rw [← Fin.snoc_init_self xs] at h
no goals
case succ.mpr.intro
L : Language
L' : Language
M : Type w
N : Type ?u.637329
P : Type ?u.637332
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n✝ : ℕ
T : Theory L
φ✝ : BoundedFormula L α n✝
v : α → M
n : ℕ
ih : ∀ {φ : BoundedFormula L α n}, Formula.Realize (exs φ) v ↔ ∃ xs, Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
xs : Fin (Nat.succ n) → M
h : Realize φ v (snoc (init xs) (xs (last n)))
⊢ ∃ xs a, Realize φ v (snoc xs a)
exact ⟨_, _, h⟩