-- Mathlib/ModelTheory/Semantics.lean
theorem _root_.FirstOrder.Language.Formula.realize_iAlls
    [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} : (φ.iAlls β).Realize v ↔
      ∀ (i : β → M), φ.Realize (fun a => Sum.elim v i a)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Tactic:
rw [Formula.iAlls]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (relabel (fun a => Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls.Realize v ↔
    ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Proof state:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose ⋯) → M) ≃ (β → M)

Tactic:
exact ⟨fun v => v ∘ e, fun v => v ∘ e.symm,
  fun _ => by simp [Function.comp_def],
  fun _ => by simp [Function.comp_def]⟩

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x✝ : Fin (Classical.choose ⋯) → M
⊢ (fun v => v ∘ ⇑e.symm) ((fun v => v ∘ ⇑e) x✝) = x✝

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x => Sum.elim (fun x => v x) (fun x => a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x =>
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize fun a_1 =>
        Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } a) a_1

Tactic:
intro x

Result:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (Realize φ (fun x_1 => Sum.elim (fun x => v x) (fun x_2 => x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) x_1) fun x_1 =>
      x (natAdd (Classical.choose ⋯) x_1)) ↔
    φ.Realize fun a =>
      Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x) a

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x✝ : β → M
⊢ (fun v => v ∘ ⇑e) ((fun v => v ∘ ⇑e.symm) x✝) = x✝

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Tactic:
let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin β))

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (relabel (fun a => Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls.Realize v ↔
    ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Tactic:
simp only [Nat.add_zero, realize_alls, realize_relabel, Function.comp_def,
  castAdd_zero, finCongr_refl, OrderIso.refl_apply, Sum.elim_map, id_eq]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (∀ (xs : Fin (Classical.choose ⋯) → M),
      Realize φ (fun x => Sum.elim (fun x => v x) (fun x => xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x =>
        xs (natAdd (Classical.choose ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (∀ (xs : Fin (Classical.choose ⋯) → M),
      Realize φ (fun x => Sum.elim (fun x => v x) (fun x => xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x =>
        xs (natAdd (Classical.choose ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a

Tactic:
refine Equiv.forall_congr ?_ ?_

Result:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose ⋯) → M) ≃ (β → M)

case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x => Sum.elim (fun x => v x) (fun x => a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x =>
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize fun a_1 => Sum.elim v (?refine_1 a) a_1

Proof state:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (Realize φ (fun x_1 => Sum.elim (fun x => v x) (fun x_2 => x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) x_1) fun x_1 =>
      x (natAdd (Classical.choose ⋯) x_1)) ↔
    φ.Realize fun a =>
      Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x) a

Tactic:
rw [Formula.Realize, iff_iff_eq]

Result:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (Realize φ (fun x_1 => Sum.elim (fun x => v x) (fun x_2 => x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) x_1) fun x_1 =>
      x (natAdd (Classical.choose ⋯) x_1)) =
    Realize φ
      (fun a =>
        Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x) a)
      default

Proof state:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (Realize φ (fun x_1 => Sum.elim (fun x => v x) (fun x_2 => x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) x_1) fun x_1 =>
      x (natAdd (Classical.choose ⋯) x_1)) =
    Realize φ
      (fun a =>
        Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x) a)
      default

Tactic:
congr

Result:
case refine_2.e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (fun x_1 => x (natAdd (Classical.choose ⋯) x_1)) = default

Proof state:
case refine_2.e__xs.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
i : Fin 0
⊢ x (natAdd (Classical.choose ⋯) i) = default i

Tactic:
exact i.elim0

Result:
no goals