-- 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
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ (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:
rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]

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 (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ Realize f✝.toFormula
      (Sum.elim v (snoc default a ∘ castAdd 0) ∘
        Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm))
      (snoc default a ∘ natAdd 1) =
    Realize f✝.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) default

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
⊢ (∀'f✝).toFormula.Realize v ↔ (∀'f✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
rw [toFormula, Formula.Realize, realize_all, realize_all]

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),
      (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
        (snoc default a)) ↔
    ∀ (a : M), f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

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)) ↔
    ∀ (a : M), f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

Tactic:
refine forall_congr' fun 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
⊢ (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
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)
⊢ (Realize f✝.toFormula
      (fun x =>
        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))
      fun x => snoc default a (natAdd 1 x)) =
    Realize f✝.toFormula (Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a)) default

Tactic:
congr with x

Result:
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

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

Proof state:
case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).toFormula.Realize v ↔ (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
  realize_imp]

Result:
no goals

Proof state:
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)

Tactic:
refine Fin.lastCases ?_ ?_ x

Result:
case all.e__v.h.inr.refine_1
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 (last n✝))) =
    Sum.elim (fun x => v (Sum.inl x)) (snoc (fun x => v (Sum.inr x)) a) (Sum.inr (last n✝))

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)