awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ).Realize v' xs ↔ φ.Realize v xs
have falsum : ∀ {n : ℕ} {xs : Fin n → M},
  Realize (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) falsum) v' xs ↔ Realize.{u, v, w, u'} (L := L) falsum 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]
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ).Realize v' xs ↔ φ.Realize v xs
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
  (mapTermRel ft fr (fun (x : ℕ) ↦ id) (equal t₁ t₂)).Realize v' xs ↔ (equal t₁ t₂).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]
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ).Realize v' xs ↔ φ.Realize v xs
have 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) (rel R ts)).Realize v' xs ↔ (rel R ts).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]
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ).Realize v' xs ↔ φ.Realize v xs
have 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
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]
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ).Realize v' xs ↔ φ.Realize v xs
have 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
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]
Cleared hypotheses: φ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)
have 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
Tactic: apply realize_mapTermRel_add_castLe
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)
have h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x
Tactic: apply realize_mapTermRel_add_castLe
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)
have 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
Tactic: apply realize_mapTermRel_add_castLe
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
have rw : k + (1 + n') = k + n' + 1
Tactic: rw [add_assoc, add_comm 1 n', ← add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ k + 1 + n' = k + n' + 1
have rw₁ : k + (n' + 1) = k + n' + 1
Tactic: rw [add_assoc, add_comm 1 n', ← add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ k + 1 + n' = k + n' + 1
have rw₂ : k + n' + 1 = k + n' + 1
Tactic: rw [add_assoc, add_comm 1 n', ← add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
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
⊢ 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')
have h : 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]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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')
have 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)
Tactic: simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.succ.le_succ)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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)
have 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)
Tactic: refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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)
⊢ (∀ (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)
have 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)
Tactic: refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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)
have 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
Tactic: simp only [Function.comp_apply, val_last, snoc_last]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
have all : (↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)
Tactic: refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ (↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)
have pos : k < m → (↑(Fin.cast h (castAdd n' (last k))) : ℕ) = (↑(last (k + n')) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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')) : ℕ)
⊢ (↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)
have neg : ¬k < m → (↑(Fin.cast h ((last k).addNat n')) : ℕ) = (↑(last (k + n')) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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 (castAdd n' (last k))) : ℕ) = (↑(last (k + n')) : ℕ)
have pos : k = k + n'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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
⊢ 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)
have 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')
Tactic: simp only [Function.comp_apply, Fin.snoc_castSucc]