awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L'.Structure M
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
    realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ {xs : Fin n_1 → M}, (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₁).Realize v' xs ↔ f₁.Realize v xs
ih2 : ∀ {xs : Fin n_1 → M}, (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₂).Realize v' xs ↔ f₂.Realize v xs
xs : Fin n_1 → M
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) (f₁ ⟹ f₂)).Realize v' xs ↔ (f₁ ⟹ f₂).Realize v xs

Tactic:
simp [mapTermRel, Realize, ih1, ih2]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L'.Structure M
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
    realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    (mapTermRel.{u, v, u', v', u_4, u_5} (α := α) ft fr (fun (x : ℕ) ↦ id) f).Realize v' xs ↔ f.Realize v xs
xs : Fin n_1 → M
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) (∀' f)).Realize v' xs ↔ (∀' f).Realize v xs

Tactic:
simp only [mapTermRel, Realize, ih, id]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, id, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L'.Structure M
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
v : α → M
v' : β → M
xs : Fin n → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
    realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum) v' xs ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.equal t₁ t₂)).Realize v' xs ↔
      (BoundedFormula.equal t₁ t₂).Realize v xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.rel R ts)).Realize v' xs ↔
      (BoundedFormula.rel R ts).Realize v xs
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : ∀ {xs : Fin n → M}, (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₁).Realize v' xs ↔ f₁.Realize v xs)
    (ih2 : ∀ {xs : Fin n → M}, (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₂).Realize v' xs ↔ f₂.Realize v xs)
    {xs : Fin n → M}, (mapTermRel ft fr (fun (x : ℕ) ↦ id) (f₁ ⟹ f₂)).Realize v' xs ↔ (f₁ ⟹ f₂).Realize v xs
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih :
      ∀ {xs : Fin (n + 1) → M},
        (mapTermRel.{u, v, u', v', u_4, u_5} (α := α) ft fr (fun (x : ℕ) ↦ id) f).Realize v' xs ↔ f.Realize v xs)
    {xs : Fin n → M}, (mapTermRel ft fr (fun (x : ℕ) ↦ id) (∀' f)).Realize v' xs ↔ (∀' f).Realize v xs
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ).Realize v' xs ↔ φ.Realize v xs

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel, Realize, h1]
  | rel => simp [mapTermRel, Realize, h1, h2]
  | imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
  | all _ ih => simp only [mapTermRel, Realize, ih, id]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.mapTermRel, id, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs' : Fin (m + n) → M),
    realize (Sum.elim v xs') (Term.relabel (relabelAux g n) t) =
      realize (Sum.elim (Sum.elim v (xs' ∘ castAdd n) ∘ g) (xs' ∘ natAdd m)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x
hv :
  ∀ (n : ℕ) (xs : Fin (m + n) → M) (x : M),
    Sum.elim v (snoc (α := fun (a : Fin (m + n + 1)) ↦ M) xs x ∘ castAdd (n + 1)) ∘ g = Sum.elim v (xs ∘ castAdd n) ∘ g
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)

Tactic:
apply realize_mapTermRel_add_castLe

Premises used: FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs' : Fin (m + n) → M),
    realize (Sum.elim v xs') (Term.relabel (relabelAux g n) t) =
      realize (Sum.elim (Sum.elim v (xs' ∘ castAdd n) ∘ g) (xs' ∘ natAdd m)) t

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (xs : Fin (m + n) → M) (x : M),
    Sum.elim v (snoc (α := fun (a : Fin (m + n + 1)) ↦ M) xs x ∘ castAdd (n + 1)) ∘ g = Sum.elim v (xs ∘ castAdd n) ∘ g

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n_1 : ℕ
xs : Fin (n_1 + n') → M
hmn : m + n' ≤ n_1 + 1
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) falsum)
      v xs ↔
    Realize.{u, v, w, u'} (L := L) (l := n_1) falsum v
      (xs ∘ fun (i : Fin n_1) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
simp [mapTermRel, Realize]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin (n_1 + n') → M
hmn : m + n' ≤ n_1 + 1
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (equal t₁ t₂))
      v xs ↔
    (equal t₁ t₂).Realize v (xs ∘ fun (i : Fin n_1) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
simp [mapTermRel, Realize, Sum.elim_comp_map]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize, Sum.elim_comp_map
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin (n_1 + n') → M
hmn : m + n' ≤ n_1 + 1
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (rel R ts))
      v xs ↔
    (rel R ts).Realize v (xs ∘ fun (i : Fin n_1) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
simp [mapTermRel, Realize, Sum.elim_comp_map]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize, Sum.elim_comp_map
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {xs : Fin (n_1 + n') → M} (hmn : m + n' ≤ n_1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₁)
        v xs ↔
      f₁.Realize v (xs ∘ fun (i : Fin n_1) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
ih2 :
  ∀ {xs : Fin (n_1 + n') → M} (hmn : m + n' ≤ n_1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₂)
        v xs ↔
      f₂.Realize v (xs ∘ fun (i : Fin n_1) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (n_1 + n') → M
hmn : m + n' ≤ n_1 + 1
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (f₁ ⟹ f₂))
      v xs ↔
    (f₁ ⟹ f₂).Realize v (xs ∘ fun (i : Fin n_1) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
rw : k + (1 + n') = k + n' + 1
rw₁ : k + (n' + 1) = k + n' + 1
rw₂ rw₃ : k + n' + 1 = k + n' + 1
⊢ k + 1 + n' = k + n' + 1

Tactic:
rw [add_assoc, add_comm 1 n', ← add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
⊢ k + 1 + n' = k + n' + 1

Tactic:
have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
all :
  (∀ (x : M),
      f.Realize v
        ((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
          if (↑i : ℕ) < m then castAdd n' i else i.addNat n')) ↔
    ∀ (x : M),
      f.Realize v
        (snoc (α := fun (a : Fin (k + 1)) ↦ M)
          (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n') x)
⊢ Realize.{u, v, w, u'} (L := L)
      (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (∀' f))
      v xs ↔
    (∀' f).Realize v (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize, Nat.le_succ, LE.le.trans, Nat.succ, FirstOrder.Language.BoundedFormula.realize_castLE_of_eq
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
⊢ (∀ (x : M),
      f.Realize v
        ((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
          if (↑i : ℕ) < m then castAdd n' i else i.addNat n')) ↔
    ∀ (x : M),
      f.Realize v
        (snoc (α := fun (a : Fin (k + 1)) ↦ M)
          (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n') x)

Tactic:
forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))

Premises used: Eq.mpr, Fin.lastCases, funext, congr, forall_congr', iff_eq_eq, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
all :
  ∀ (x : M),
    Eq.{w + 1} (α := M)
      (((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
            if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
          (last k) :
        M)
      (snoc (α := fun (a : Fin (k + 1)) ↦ M) (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
          x (last k) :
        M)
all₁ :
  ∀ (x : M) (i : Fin k),
    Eq.{w + 1} (α := M)
      (((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
            if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
          i.castSucc :
        M)
      (snoc (α := fun (a : Fin (k + 1)) ↦ M) (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
          x i.castSucc :
        M)
⊢ (∀ (x : M),
      f.Realize v
        ((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
          if (↑i : ℕ) < m then castAdd n' i else i.addNat n')) ↔
    ∀ (x : M),
      f.Realize v
        (snoc (α := fun (a : Fin (k + 1)) ↦ M)
          (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n') x)

Tactic:
refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))

Premises used: Eq.mpr, Fin.lastCases, funext, congr, forall_congr', iff_eq_eq, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
all :
  snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) =
    x
⊢ Eq.{w + 1} (α := M)
    (((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
          if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
        (last k) :
      M)
    (snoc (α := fun (a : Fin (k + 1)) ↦ M) (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n') x
        (last k) :
      M)

Tactic:
simp only [Function.comp_apply, val_last, snoc_last]

Premises used: Function.comp_apply, Fin.val_last, Fin.snoc_last
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
⊢ snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) =
    x

Tactic:
(congr rfl (Fin.ext ?_)).trans (snoc_last _ _)

Premises used: Fin.ext, congr, Fin.snoc_last, rfl, Eq.trans
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
all : (↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)
⊢ snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) =
    x

Tactic:
refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)

Premises used: Fin.ext, congr, rfl, Eq.trans
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
pos : k < m → (↑(Fin.cast h (castAdd n' (last k))) : ℕ) = (↑(last (k + n')) : ℕ)
neg : ¬k < m → (↑(Fin.cast h ((last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)
⊢ (↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)

Tactic:
split_ifs
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
h_1 : k < m
pos : k = k + n'
⊢ (↑(Fin.cast h (castAdd n' (last k))) : ℕ) = (↑(last (k + n')) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
h_1 : ¬k < m
⊢ (↑(Fin.cast h ((last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
h_1 : k < m
⊢ k = k + n'

Tactic:
lia
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
all :
  snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    xs (if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
⊢ Eq.{w + 1} (α := M)
    (((snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x ∘ Fin.cast h) ∘ fun (i : Fin (k + 1)) ↦
          if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
        i.castSucc :
      M)
    (snoc (α := fun (a : Fin (k + 1)) ↦ M) (xs ∘ fun (i : Fin k) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n') x
        i.castSucc :
      M)

Tactic:
simp only [Function.comp_apply, Fin.snoc_castSucc]

Premises used: Fin.snoc_castSucc, Function.comp_apply