-- Mathlib/ModelTheory/Semantics.lean
theorem realize_toFormula (φ : L.BoundedFormula α n) (v : α ⊕ (Fin n) → M) :
    φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Proof state:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

Tactic:
have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))

Result:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔
    f✝.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a) ∘ Sum.inl)
      (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a) ∘ Sum.inr)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

Proof state:
case all.e__v.h.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝),
    Sum.elim v (fun x => snoc default a (castAdd 0 x))
        (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.map Sum.inr id (finSumFinEquiv.symm x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a) (Sum.inr i.castSucc)

Tactic:
simp only [castSucc, Function.comp_apply, Sum.elim_inr,
  finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]

Result:
case all.e__v.h.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝), v (Sum.inr i) = snoc (fun x => v (Sum.inr x)) a (castAdd 1 i)

Proof state:
case all.e__v.h.inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
val✝ : α
⊢ Sum.elim v (fun x => snoc default a (castAdd 0 x))
      (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.map Sum.inr id (finSumFinEquiv.symm x)) (Sum.inl val✝)) =
    Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a) (Sum.inl val✝)

Tactic:
simp

Result:
no goals

Proof state:
case all.e__xs.h
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin 0
⊢ snoc default a (natAdd 1 x) = default x

Tactic:
exact Fin.elim0 x

Result:
no goals

Proof state:
case all.e__v.h
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : α ⊕ Fin (n✝ + 1)
⊢ Sum.elim v (fun x => snoc default a (castAdd 0 x))
      (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.map Sum.inr id (finSumFinEquiv.symm x)) x) =
    Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a) x

Tactic:
rcases x with _ | x

Result:
case all.e__v.h.inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
val✝ : α
⊢ Sum.elim v (fun x => snoc default a (castAdd 0 x))
      (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.map Sum.inr id (finSumFinEquiv.symm x)) (Sum.inl val✝)) =
    Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a) (Sum.inl val✝)

case all.e__v.h.inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ Sum.elim v (fun x => snoc default a (castAdd 0 x))
      (Sum.elim (fun x => Sum.inl (Sum.inl x)) (fun x => Sum.map Sum.inr id (finSumFinEquiv.symm x)) (Sum.inr x)) =
    Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a) (Sum.inr x)