case zero
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin Nat.zero → M), Realize φ v xs

case succ
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin n → M), Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ Formula.Realize (alls φ) v ↔ ∀ (xs : Fin (Nat.succ n) → M), Realize φ v xs
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin n → M), Realize φ v xs
induction' n with n ih
no goals
case zero
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin Nat.zero → M), Realize φ v xs
exact Unique.forall_iff.symm
case succ
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin n → M), Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∀ (xs : Fin n → M) (x : M), Realize φ v (snoc xs x)) ↔ ∀ (xs : Fin (Nat.succ n) → M), Realize φ v xs
case succ
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin n → M), Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ Formula.Realize (alls φ) v ↔ ∀ (xs : Fin (Nat.succ n) → M), Realize φ v xs
simp only [alls, ih, Realize]
no goals
case succ
L : Language
L' : Language
M : Type w
N : Type ?u.635929
P : Type ?u.635932
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 (alls φ) v ↔ ∀ (xs : Fin n → M), Realize φ v xs
φ : BoundedFormula L α (Nat.succ n)
⊢ (∀ (xs : Fin n → M) (x : M), Realize φ v (snoc xs x)) ↔ ∀ (xs : Fin (Nat.succ n) → M), Realize φ v xs
exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩