-- Mathlib/ModelTheory/Semantics.lean
theorem _root_.FirstOrder.Language.Formula.realize_iExs
    [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} : (φ.iExs γ).Realize v ↔
      ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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.e__xs.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

Tactic:
rw [Formula.iExs]

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

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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 u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

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 u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

Proof state:
case refine_2.e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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

Tactic:
funext i

Result:
case refine_2.e__xs.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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

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

Tactic:
simp only [Nat.add_zero, realize_exs, 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 u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (∃ xs,
      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, φ.Realize (Sum.elim v i)

Proof state:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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 φ
      (Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x))
      default

Tactic:
congr

Result:
case refine_2.e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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
        (Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } a))

Tactic:
intro x

Result:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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
      (Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x))

Proof state:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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
      (Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x))

Tactic:
rw [Formula.Realize, iff_iff_eq]

Result:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
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 φ
      (Sum.elim v ({ toFun := fun v => v ∘ ⇑e, invFun := fun v => v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } x))
      default