awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (i : Fin 0), x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) i) = default i
⊢ 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

Tactic:
funext i
-- 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
i : Fin 0
⊢ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) i) = default i

Tactic:
i.elim0

Premises used: Fin.elim0
-- 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
i : Fin 0
⊢ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{v' + 1} (β ≃ Fin x)) ⋯) i) = default i

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- 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
v' : Fin 0 → M
rw : Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v
⊢ Realize (Formula.iAlls β φ) v v' ↔ ∀ (i : β → M), φ.Realize (M := M) fun (a : α ⊕ β) ↦ Sum.elim v i a

Tactic:
rw [← Formula.realize_iAlls, iff_iff_eq]

Premises used: iff_iff_eq, FirstOrder.Language.Formula.realize_iAlls
-- 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
v' : Fin 0 → M
e__xs : v' = default
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v

Tactic:
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
v' : Fin 0 → M
⊢ v' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
simp :
  (∃ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                      (a : γ) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x)) ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)
⊢ Formula.Realize
      (exs (n := Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯ + 0)
        (relabel
          (fun (a : α ⊕ γ) ↦
            Sum.map id
              (⇑(Classical.choice ⋯ :
                    γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                (a : γ) → Fin (Classical.choose ⋯))
              a)
          φ))
      v ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Tactic:
simp only [Nat.add_zero, realize_exs, 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_exs, 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 u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
⊢ (∃ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                      (a : γ) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x)) ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Tactic:
Equiv.exists_congr ?_ ?_

Premises used: Equiv.exists_congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
refine_1 : (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M) ≃ (γ → M)
refine_2 :
  ∀ (a : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                      (a : γ) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ a (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x)) ↔
      φ.Realize
        (Sum.elim v
          (({
                toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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 := ⋯ :
                (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M) ≃ (γ → M) } :
              (a : Fin (Classical.choose ⋯) → M) → γ → M)
            a))
⊢ (∃ (xs : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                      (a : γ) → Fin (Classical.choose ⋯))
                    x)))
            x)
        fun (x : Fin 0) ↦ xs (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x)) ↔
    ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Tactic:
refine Equiv.exists_congr ?_ ?_

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

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 u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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.{u_3 + 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.{u_3 + 1} (γ ≃ Fin x)) ⋯)) :
                    (a : γ) → Fin (Classical.choose ⋯))
                  x_2)))
          x_1)
      fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x_1)) =
    Realize φ
      (Sum.elim v
        (({
              toFun := fun (v : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 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 := ⋯ :
              (Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M) ≃ (γ → M) } :
            (a : Fin (Classical.choose ⋯) → M) → γ → M)
          x))
      default

Tactic:
congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M
refine_2 :
  ∀ (i : Fin 0), x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) i) = default i
⊢ Eq.{w + 1} (α := Fin 0 → M)
    (fun (x_1 : Fin 0) ↦ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) x_1))
    default

Tactic:
funext i
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M
i : Fin 0
⊢ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) i) = default i

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{max 1 (u_3 + 1)} (γ ≃ Fin x)) ⋯) := Classical.choice ⋯
x : Fin (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) → M
i : Fin 0
⊢ x (natAdd (Classical.choose (p := fun (x : ℕ) ↦ Nonempty.{u_3 + 1} (γ ≃ Fin x)) ⋯) i) = default i

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
rw : Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v
⊢ Realize (Formula.iExs γ φ) v v' ↔ ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Tactic:
rw [← Formula.realize_iExs, iff_iff_eq]

Premises used: iff_iff_eq, FirstOrder.Language.Formula.realize_iExs
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
e__xs : v' = default
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v

Tactic:
congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
γ : Type u_3
inst_1 : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
v : α ⊕ Fin n_1 → M
⊢ Formula.Realize.{u, v, w, u'} (L := L) (toFormula falsum) v ↔
    Realize.{u, v, w, u'} (L := L) falsum (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
v : α ⊕ Fin n_1 → M
⊢ (equal t₁ t₂).toFormula.Realize v ↔ (equal t₁ t₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
simp [BoundedFormula.Realize]

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
v : α ⊕ Fin n_1 → M
⊢ (rel R ts).toFormula.Realize v ↔ (rel R ts).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
simp [BoundedFormula.Realize]

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (v : α ⊕ Fin n_1 → M), f₁.toFormula.Realize v ↔ f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n_1 → M), f₂.toFormula.Realize v ↔ f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
imp : Formula.Realize (f₁.toFormula ⟹ f₂.toFormula) v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₁ : (f₁.toFormula ⟹ f₂.toFormula).Realize v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₂ : Realize f₁.toFormula v default → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₃ : f₁.toFormula.Realize v → Realize f₂.toFormula v default ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₄ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → Realize f₂.toFormula v default ↔
    (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₅ : f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.toFormula.Realize v ↔ (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₆ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) ↔
    (f₁ ⟹ f₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp₇ imp₈ :
  f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) ↔
    f₁.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → f₂.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ (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]

Premises used: FirstOrder.Language.BoundedFormula.toFormula, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
all :
  (∀ (a : M),
      Realize (l := Nat.succ 0)
        (relabel
          (Sum.elim (Sum.inl ∘ Sum.inl)
            (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
          f.toFormula)
        v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)) ↔
    ∀ (a : M), f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
⊢ (∀' f).toFormula.Realize v ↔ (∀' f).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

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

Premises used: FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.toFormula, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
⊢ (∀ (a : M),
      Realize (l := Nat.succ 0)
        (relabel
          (Sum.elim (Sum.inl ∘ Sum.inl)
            (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
          f.toFormula)
        v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)) ↔
    ∀ (a : M), f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)

Tactic:
forall_congr' fun a => ?_

Premises used: forall_congr'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
all :
  ∀ (a : M),
    Realize (l := Nat.succ 0)
        (relabel
          (Sum.elim (Sum.inl ∘ Sum.inl)
            (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
          f.toFormula)
        v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a) ↔
      f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)
⊢ (∀ (a : M),
      Realize (l := Nat.succ 0)
        (relabel
          (Sum.elim (Sum.inl ∘ Sum.inl)
            (Sum.map Sum.inr id ∘ (⇑(_root_.Equiv.symm finSumFinEquiv) : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1)))
          f.toFormula)
        v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)) ↔
    ∀ (a : M), f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin n_1.succ) ↦ M) (v ∘ Sum.inr) a)

Tactic:
refine forall_congr' fun a => ?_

Premises used: forall_congr'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (v : α ⊕ Fin (n_1 + 1) → M), f.toFormula.Realize v ↔ f.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n_1 → M
a : M
⊢ f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize
      (Function.comp (β := α ⊕ Fin (n_1 + 1))
        (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) Sum.inl)
      (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a) ∘ Sum.inr)

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