awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
all :
  Realize f.toFormula
      (Function.comp (β := (α ⊕ Fin n_1) ⊕ Fin 1)
        (Sum.elim v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a ∘ castAdd 0))
        (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))))
      (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 1 0)) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)
        (natAdd 1)) =
    Realize f.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) default
⊢ 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)

Tactic:
rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]

Premises used: iff_iff_eq, FirstOrder.Language.BoundedFormula.realize_relabel, 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
all :
  (Realize.{u, v, w, u'} (M := M) f.toFormula
      (fun (x : α ⊕ Fin (n_1 + 1)) ↦
        Sum.elim v
          (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
          (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
            (fun (x : Fin (n_1 + 1)) ↦
              Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
            x))
      fun (x : Fin 0) ↦ snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x)) =
    Realize.{u, v, w, u'} (M := M) f.toFormula
      (Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a))
      default
⊢ Realize f.toFormula
      (Function.comp (β := (α ⊕ Fin n_1) ⊕ Fin 1)
        (Sum.elim v (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a ∘ castAdd 0))
        (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))))
      (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 1 0)) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a)
        (natAdd 1)) =
    Realize f.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) default

Tactic:
simp only [Function.comp_def]

Premises used: Function.comp_def
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
all :
  ∀ (x : α ⊕ Fin (n_1 + 1)),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          x) =
      Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) x
all₁ :
  ∀ (x : Fin 0),
    Eq.{w + 1} (α := M) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x) : M) (default x : M)
⊢ (Realize.{u, v, w, u'} (M := M) f.toFormula
      (fun (x : α ⊕ Fin (n_1 + 1)) ↦
        Sum.elim v
          (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
          (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
            (fun (x : Fin (n_1 + 1)) ↦
              Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
            x))
      fun (x : Fin 0) ↦ snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x)) =
    Realize.{u, v, w, u'} (M := M) f.toFormula
      (Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a))
      default

Tactic:
congr with x
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : α ⊕ Fin (n_1 + 1)
all :
  ∀ (val : α),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          (Sum.inl val)) =
      Sum.elim (β := Fin (n_1 + 1)) (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inl val)
all₁ :
  ∀ (x : Fin (n_1 + 1)),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          (Sum.inr x)) =
      Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr x)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        x) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) x

Tactic:
rcases x with _ | x
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
val : α
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inl val)) =
    Sum.elim (β := Fin (n_1 + 1)) (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inl val)

Tactic:
simp
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr x)) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr x)

Tactic:
Fin.lastCases ?_ ?_ x

Premises used: Fin.lastCases
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
all :
  Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr (last n_1))) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr (last n_1))
all₁ :
  ∀ (i : Fin n_1),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr x)) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr x)

Tactic:
refine Fin.lastCases ?_ ?_ x
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
⊢ Sum.elim v
      (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
      (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
        (fun (x : Fin (n_1 + 1)) ↦
          Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
        (Sum.inr (last n_1))) =
    Sum.elim (fun (x : α) ↦ v (Sum.inl x))
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr (last n_1))

Tactic:
simp [Fin.snoc]

Premises used: Fin.snoc
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
all :
  ∀ (i : Fin n_1),
    v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a (castAdd 1 i)
⊢ ∀ (i : Fin n_1),
    Sum.elim v
        (fun (x : Fin 1) ↦ snoc.{w + 1} (α := fun (a : Fin (Nat.succ 0)) ↦ M) (default : Fin 0 → M) a (castAdd 0 x))
        (Sum.elim (fun (x : α) ↦ Sum.inl (Sum.inl x))
          (fun (x : Fin (n_1 + 1)) ↦
            Sum.map Sum.inr id ((_root_.Equiv.symm finSumFinEquiv : (a : Fin (n_1 + 1)) → Fin n_1 ⊕ Fin 1) x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun (x : α) ↦ v (Sum.inl x))
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)

Tactic:
simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]

Premises used: Sum.map_inl, finSumFinEquiv_symm_apply_castAdd, Sum.elim_inr, Sum.elim_inl, Fin.castSucc
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
all :
  ∀ (i : Fin n_1),
    v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a i.castSucc
⊢ ∀ (i : Fin n_1),
    v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a (castAdd 1 i)

Tactic:
rw [← castSucc]

Premises used: Fin.castSucc
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin (n_1 + 1)
⊢ ∀ (i : Fin n_1),
    v (Sum.inr i) = snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (fun (x : Fin n_1) ↦ v (Sum.inr x)) a i.castSucc

Tactic:
simp
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin 0
⊢ Eq.{w + 1} (α := M) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x) : M) (default x : M)

Tactic:
Fin.elim0 x

Premises used: Fin.elim0
-- 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
h :
  f.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)) ↔
    f.Realize (v ∘ Sum.inl) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) (v ∘ Sum.inr) a)
x : Fin 0
⊢ Eq.{w + 1} (α := M) (snoc (α := fun (a : Fin (Nat.succ 0)) ↦ M) default a (natAdd 1 x) : M) (default x : M)

Tactic:
exact Fin.elim0 x

Premises used: Fin.elim0
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α ⊕ Fin n → M
falsum :
  ∀ {n : ℕ} (v : α ⊕ Fin n → M),
    Formula.Realize.{u, v, w, u'} (L := L) (toFormula BoundedFormula.falsum) v ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum (v ∘ Sum.inl) (v ∘ Sum.inr)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.equal t₁ t₂).toFormula.Realize v ↔ (BoundedFormula.equal t₁ t₂).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) (v : α ⊕ Fin n → M),
    (BoundedFormula.rel R ts).toFormula.Realize v ↔ (BoundedFormula.rel R ts).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
imp :
  ∀ {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)
all :
  ∀ {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)
⊢ φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [BoundedFormula.Realize]
  | rel => simp [BoundedFormula.Realize]
  | imp _ _ ih1 ih2 =>
    rw [toFormula, Formula.Realize, realize_imp, ← Formula.Realize, ih1, ← Formula.Realize, ih2,
      realize_imp]
  | all _ ih3 =>
    rw [toFormula, Formula.Realize, realize_all, realize_all]
    refine forall_congr' fun a => ?_
    have h := ih3 (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a))
    simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h
    rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]
    simp only [Function.comp_def]
    congr with x
    · rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp
    · exact Fin.elim0 x

Premises used: FirstOrder.Language.BoundedFormula.imp, Sum.map_inl, Sum.elim_comp_inr, Sum.elim_comp_inl, iff_iff_eq, FirstOrder.Language.BoundedFormula.realize_all, Fin.snoc, finSumFinEquiv_symm_apply_castAdd, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.realize_relabel, Sum.elim_inr, FirstOrder.Language.BoundedFormula.falsum, Function.comp_def, FirstOrder.Language.BoundedFormula.toFormula, forall_congr', Sum.elim_inl, Fin.castSucc, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst_1 : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iSup f).Realize v v' ↔ ∃ (b : β), (f b).Realize v v'

Tactic:
simp only [iSup, realize_foldr_sup, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
    exists_exists_eq_and]

Premises used: Finset.mem_univ, FirstOrder.Language.BoundedFormula.realize_foldr_sup, exists_exists_eq_and, FirstOrder.Language.BoundedFormula.iSup, Finset.mem_toList, List.mem_map, true_and
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst_1 : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iInf f).Realize v v' ↔ ∀ (b : β), (f b).Realize v v'

Tactic:
simp only [iInf, realize_foldr_inf, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
    forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Finset.mem_univ, forall_exists_index, FirstOrder.Language.BoundedFormula.iInf, FirstOrder.Language.BoundedFormula.realize_foldr_inf, Finset.mem_toList, List.mem_map, forall_apply_eq_imp_iff, true_and
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : Finite β
f : β → L.Formula α
v : α → M
⊢ (Formula.iSup f).Realize v ↔ ∃ (b : β), (f b).Realize v

Tactic:
simp [Formula.iSup, Formula.Realize]

Premises used: FirstOrder.Language.Formula.iSup, 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 β
f : β → L.Formula α
v : α → M
⊢ (Formula.iInf f).Realize v ↔ ∀ (b : β), (f b).Realize v

Tactic:
simp [Formula.iInf, Formula.Realize]

Premises used: FirstOrder.Language.Formula.iInf, 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
simp :
  (∃ (i : γ → M),
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize (M := M)
              ((fun (a : (α ⊕ γ) ⊕ γ) ↦ Sum.elim (Sum.elim v i) i_1 a) ∘ fun (a : α ⊕ γ) ↦
                Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (L := L) (M := M)
              (iInf fun (g : γ) ↦ Term.equal (var (Sum.inr g)) (var (Sum.inl (Sum.inr g)))) fun (a : (α ⊕ γ) ⊕ γ) ↦
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ (x : γ → M), φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              (Formula.imp (Formula.relabel (fun (a : α ⊕ γ) ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ)
                (iInf fun (g : γ) ↦ Term.equal (var (Sum.inr g)) (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ (x : γ → M), φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
simp only [Formula.realize_iExs, Formula.realize_inf, Formula.realize_iAlls, Formula.realize_imp,
    Formula.realize_relabel]

Premises used: FirstOrder.Language.Formula.realize_iAlls, FirstOrder.Language.Formula.realize_relabel, FirstOrder.Language.Formula.realize_inf, FirstOrder.Language.Formula.realize_imp, FirstOrder.Language.Formula.realize_iExs