awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T T' : L.Theory
h : ∀ φ ∈ T, M ⊨ φ
h' : ∀ φ ∈ T', M ⊨ φ
⊢ ∀ (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ

Tactic:
fun φ hφ => hφ.elim (h _) (h' _)

Premises used: Or.elim
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T T' : L.Theory
h : ∀ φ ∈ T, M ⊨ φ
h' : ∀ φ ∈ T', M ⊨ φ
⊢ ∀ (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ

Tactic:
exact fun φ hφ => hφ.elim (h _) (h' _)
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T T' : L.Theory
⊢ M ⊨ T ∪ T' ↔ M ⊨ T ∧ M ⊨ T'

Tactic:
⟨fun h => ⟨h.mono Set.subset_union_left, h.mono Set.subset_union_right⟩, fun h =>
    h.1.union h.2⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, FirstOrder.Language.Theory.Model.mono, FirstOrder.Language.Theory.Model.union
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
⊢ Model.{u, v, w} (L := L) M {φ} ↔ M ⊨ φ

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
φ : L.Sentence
rw : M ⊨ {φ} ∪ T ↔ M ⊨ φ ∧ M ⊨ T
rw₁ : Model.{u, v, w} (L := L) M {φ} ∧ M ⊨ T ↔ M ⊨ φ ∧ M ⊨ T
rw₂ rw₃ : M ⊨ φ ∧ M ⊨ T ↔ M ⊨ φ ∧ M ⊨ T
⊢ M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T

Tactic:
rw [Set.insert_eq, model_union_iff, model_singleton_iff]

Premises used: Set.insert_eq, FirstOrder.Language.Theory.model_union_iff, FirstOrder.Language.Theory.model_singleton_iff
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
⊢ M ⊨ T ↔ T ⊆ L.completeTheory M

Tactic:
T.model_iff

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.completeTheory, Set.Mem, setOf, FirstOrder.Language.Theory.model_iff, Set.Subset, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
MT : M ⊨ T
⊢ T ⊆ L.completeTheory M

Tactic:
model_iff_subset_completeTheory.1 MT

Premises used: FirstOrder.Language.Theory.model_iff_subset_completeTheory, Iff.mp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
T : L.Theory
⊢ M ⊨ L.completeTheory M

Tactic:
Theory.model_iff_subset_completeTheory.2 subset_rfl

Premises used: Iff.mpr, FirstOrder.Language.Theory.model_iff_subset_completeTheory, subset_rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
⊢ N ⊨ φ ↔ M ⊨ φ

Tactic:
⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩

Premises used: FirstOrder.Language.completeTheory, Iff.intro, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
refine : ∀ (h : N ⊨ φ), M ⊨ φ
⊢ N ⊨ φ ↔ M ⊨ φ

Tactic:
refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
h : N ⊨ φ
contrapose : ∀ (h : ¬M ⊨ φ), ¬N ⊨ φ
⊢ M ⊨ φ

Tactic:
contrapose h
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
h : ¬M ⊨ φ
⊢ M ⊨ Formula.not φ

Tactic:
rw [← Sentence.realize_not] at *

Premises used: FirstOrder.Language.Sentence.realize_not
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ

Tactic:
(L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)

Premises used: Iff.mpr, FirstOrder.Language.completeTheory, FirstOrder.Language.mem_completeTheory, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : N ⊨ L.completeTheory M
φ : L.Sentence
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ

Tactic:
exact (L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)

Premises used: Iff.mpr, FirstOrder.Language.completeTheory, FirstOrder.Language.mem_completeTheory, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs

Tactic:
Unique.forall_iff.symm

Premises used: FirstOrder.Language.BoundedFormula.alls, Unique.forall_iff, Iff.symm, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs

Tactic:
exact Unique.forall_iff.symm

Premises used: Unique.forall_iff, Iff.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
succ :
  (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc (α := fun (a : Fin (n + 1)) ↦ M) xs x)) ↔
    ∀ (xs : Fin (n + 1) → M), φ.Realize v xs
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
simp only [alls, ih, Realize]

Premises used: FirstOrder.Language.BoundedFormula.alls, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc (α := fun (a : Fin (n + 1)) ↦ M) xs x)) ↔
    ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩

Premises used: Eq.rec, Fin.snoc, Fin.init, Fin.snoc_init_self, Fin.last, Iff.intro
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc (α := fun (a : Fin (n + 1)) ↦ M) xs x)) ↔
    ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
zero : ∀ {φ : L.BoundedFormula α 0}, φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs
succ :
  ∀ (n : ℕ) (ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs)
    {φ : L.BoundedFormula α (n + 1)}, φ.alls.Realize v ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs

Tactic:
induction n with
  | zero => exact Unique.forall_iff.symm
  | succ n ih =>
    simp only [alls, ih, Realize]
    exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩

Premises used: FirstOrder.Language.BoundedFormula.alls, Fin.succ, FirstOrder.Language.BoundedFormula.Realize, Unique.forall_iff, Iff.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin 0 → M), φ.Realize v xs

Tactic:
Unique.exists_iff.symm

Premises used: FirstOrder.Language.BoundedFormula.exs, Unique.exists_iff, Iff.symm, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin 0 → M), φ.Realize v xs

Tactic:
exact Unique.exists_iff.symm

Premises used: Unique.exists_iff, Iff.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
succ :
  (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) ↔
    ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
simp only [BoundedFormula.exs, ih, realize_ex]

Premises used: FirstOrder.Language.BoundedFormula.realize_ex, FirstOrder.Language.BoundedFormula.exs
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
succ :
  (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
    ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
succ₁ :
  (∃ (xs : Fin (n + 1) → M), φ.Realize v xs) →
    ∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
⊢ (∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) ↔
    ∃ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin n → M
x : M
h : φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs x)
⊢ ∃ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin n → M
x : M
h : φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs x)
⊢ ∃ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v xs
⊢ φ.Realize v (snoc (α := fun (i : Fin (n + 1)) ↦ M) (init (α := fun (i : Fin (n + 1)) ↦ M) xs) (xs (last n)))

Tactic:
rw [← Fin.snoc_init_self xs] at h

Premises used: Fin.snoc_init_self
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v (snoc (α := fun (i : Fin (n + 1)) ↦ M) (init (α := fun (i : Fin (n + 1)) ↦ M) xs) (xs (last n)))
⊢ ∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
⟨_, _, h⟩

Premises used: Exists.intro
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n_1 : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
xs : Fin (n + 1) → M
h : φ.Realize v (snoc (α := fun (i : Fin (n + 1)) ↦ M) (init (α := fun (i : Fin (n + 1)) ↦ M) xs) (xs (last n)))
⊢ ∃ (xs : Fin n → M) (a : M), φ.Realize v (snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
exact ⟨_, _, h⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
zero : ∀ {φ : L.BoundedFormula α 0}, φ.exs.Realize v ↔ ∃ (xs : Fin 0 → M), φ.Realize v xs
succ :
  ∀ (n : ℕ) (ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs)
    {φ : L.BoundedFormula α (n + 1)}, φ.exs.Realize v ↔ ∃ (xs : Fin (n + 1) → M), φ.Realize v xs
⊢ φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs

Tactic:
induction n with
  | zero => exact Unique.exists_iff.symm
  | succ n ih =>
    simp only [BoundedFormula.exs, ih, realize_ex]
    constructor
    · rintro ⟨xs, x, h⟩
      exact ⟨_, h⟩
    · rintro ⟨xs, h⟩
      rw [← Fin.snoc_init_self xs] at h
      exact ⟨_, _, h⟩

Premises used: FirstOrder.Language.BoundedFormula.realize_ex, Fin.succ, FirstOrder.Language.BoundedFormula.exs, Unique.exists_iff, Iff.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
simp :
  (∀ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ β) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : β) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                      (a : β) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a
⊢ Formula.Realize
      (alls (n := Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯ + 0)
        (relabel
          (fun (a : α ⊕ β) ↦
            Sum.map id
              (⇑(Classical.choice ⋯ : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                (a : β) → Fin (Classical.choose ⋯))
              a)
          φ))
      v ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a

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

Premises used: Fin.castAdd_zero, FirstOrder.Language.BoundedFormula.realize_relabel, Function.comp_def, FirstOrder.Language.BoundedFormula.realize_alls, Nat.add_zero, id_eq, Sum.elim_map
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ (∀ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ β) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : β) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                      (a : β) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a

Tactic:
Equiv.forall_congr ?_ ?_

Premises used: Equiv.forall_congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
refine_1 : (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ≃ (β → M)
refine_2 :
  ∀ (a : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M),
    (Realize (M := M) φ
        (fun (x : α ⊕ β) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : β) ↦
              a
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                      (a : β) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ a (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x)) ↔
      φ.Realize (M := M) fun (a_1 : α ⊕ β) ↦
        Sum.elim v
          (({
                toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
                  v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)),
                invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β), left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Fin (Classical.choose ⋯) → M) → β → M)
            a)
          a_1
⊢ (∀ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M),
      Realize (M := M) φ
        (fun (x : α ⊕ β) ↦
          Sum.elim (fun (x : α) ↦ v x)
            (fun (x : β) ↦
              xs
                (Fin.cast ⋯
                  (((Classical.choice ⋯ :
                        β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                      (a : β) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x)) ↔
    ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a

Tactic:
refine Equiv.forall_congr ?_ ?_

Premises used: Equiv.forall_congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M
⊢ (fun (v : β → M) ↦
        (v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β) :
          Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M))
      ((fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
          (v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)) : β → M))
        x) =
    x

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : β → M
⊢ (fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
        (v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)) : β → M))
      ((fun (v : β → M) ↦
          (v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β) :
            Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M))
        x) =
    x

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → 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]⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M
refine_2 :
  (Realize (M := M) φ
      (fun (x_1 : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x_2 : β) ↦
            x
              (Fin.cast ⋯
                (((Classical.choice ⋯ :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                    (a : β) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) =
    Realize (M := M) φ
      (fun (a : α ⊕ β) ↦
        Sum.elim v
          (({
                toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
                  v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)),
                invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β), left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Fin (Classical.choose ⋯) → M) → β → M)
            x)
          a)
      default
⊢ (Realize (M := M) φ
      (fun (x_1 : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x_2 : β) ↦
            x
              (Fin.cast ⋯
                (((Classical.choice ⋯ :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                    (a : β) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) ↔
    φ.Realize (M := M) fun (a : α ⊕ β) ↦
      Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
                v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)),
              invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Fin (Classical.choose ⋯) → M) → β → M)
          x)
        a

Tactic:
rw [Formula.Realize, iff_iff_eq]

Premises used: iff_iff_eq, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (v' + 1)} (β ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M
refine_2 :
  Eq.{w + 1} (α := Fin 0 → M)
    (fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) default
⊢ (Realize (M := M) φ
      (fun (x_1 : α ⊕ β) ↦
        Sum.elim (fun (x : α) ↦ v x)
          (fun (x_2 : β) ↦
            x
              (Fin.cast ⋯
                (((Classical.choice ⋯ :
                      β ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯)) :
                    (a : β) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) x_1)) =
    Realize (M := M) φ
      (fun (a : α ⊕ β) ↦
        Sum.elim v
          (({
                toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) → M) ↦
                  v ∘ (⇑e : (a : β) → Fin (Classical.choose ⋯)),
                invFun := fun (v : β → M) ↦ v ∘ (⇑e.symm : (a : Fin (Classical.choose ⋯)) → β), left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Fin (Classical.choose ⋯) → M) → β → M)
            x)
          a)
      default

Tactic:
congr