-- Mathlib/ModelTheory/Semantics.lean
theorem realize_all_liftAt_one_self {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M}
    {xs : Fin n → M} : (φ.liftAt 1 n).all.Realize v xs ↔ φ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (∀'liftAt 1 n φ).Realize v xs ↔ φ.Realize v xs

Tactic:
inhabit M

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ (∀'liftAt 1 n φ).Realize v xs ↔ φ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ (∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)) ↔ φ.Realize v xs

Tactic:
refine ⟨fun h => ?_, fun h a => ?_⟩

Result:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)
⊢ φ.Realize v xs

case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : φ.Realize v xs
a : M
⊢ φ.Realize v (snoc xs a ∘ castSucc)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ (∀'liftAt 1 n φ).Realize v xs ↔ φ.Realize v xs

Tactic:
simp only [realize_all, realize_liftAt_one_self]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ (∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)) ↔ φ.Realize v xs

Proof state:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : φ.Realize v xs
a : M
⊢ φ.Realize v (snoc xs a ∘ castSucc)

Tactic:
refine (congr rfl (funext fun i => ?_)).mp h

Result:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : φ.Realize v xs
a : M
i : Fin n
⊢ xs i = (snoc xs a ∘ castSucc) i

Proof state:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)
⊢ φ.Realize v xs

Tactic:
refine (congr rfl (funext fun i => ?_)).mp (h default)

Result:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)
i : Fin n
⊢ (snoc xs default ∘ castSucc) i = xs i

Proof state:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : φ.Realize v xs
a : M
i : Fin n
⊢ xs i = (snoc xs a ∘ castSucc) i

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)
i : Fin n
⊢ (snoc xs default ∘ castSucc) i = xs i

Tactic:
simp

Result:
no goals