awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α n)
      (mapTermRel.{u, v, u', u', u, v} (L := L) (L' := L) (α := α) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id)
          (fun (x : ℕ) ↦ id) fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum :
        L.BoundedFormula α n)
      (BoundedFormula.falsum : L.BoundedFormula α n)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
        (BoundedFormula.equal t₁ t₂) =
      BoundedFormula.equal t₁ t₂
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
        (BoundedFormula.rel R ts) =
      BoundedFormula.rel R ts
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ = φ
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 :
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) f₁ =
      f₁)
  (ih2 :
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) f₂ =
      f₂),
  mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
      (f₁.imp f₂) =
    f₁.imp f₂
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α n)
      (mapTermRel.{u, v, u', u', u, v} (L := L) (L' := L) (α := α) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id)
          (fun (x : ℕ) ↦ id) fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum :
        L.BoundedFormula α n)
      (BoundedFormula.falsum : L.BoundedFormula α n)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
        (BoundedFormula.equal t₁ t₂) =
      BoundedFormula.equal t₁ t₂
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
        (BoundedFormula.rel R ts) =
      BoundedFormula.rel R ts
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) f₁ =
        f₁)
    (ih2 :
      mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) f₂ =
        f₂),
    mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
        (f₁.imp f₂) =
      f₁.imp f₂
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ = φ
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 : mapTermRel (L := L) (α := α) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) f = f),
  mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) f.all =
    f.all
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
⊢ Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)
have h : ∀ (x : α ⊕ Fin m), (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α ⊕ Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x
have h : ∀ (x : α),
  (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)
Tactic: rcases x with x | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α ⊕ Fin m
h :
  ∀ (x : α),
    (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) =
      Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x
have h₁ : ∀ (x : Fin m),
  (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)
Tactic: rcases x with x | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)
have h : Sum.elim v xs
    (Sum.map (β := Fin n ⊕ Fin m) id (⇑finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m))
      ((Equiv.sumAssoc β (Fin n) (Fin m) : (a : (β ⊕ Fin n) ⊕ Fin m) → β ⊕ Fin n ⊕ Fin m) (Sum.inl (g x)))) =
  Sum.elim v (xs ∘ castAdd m) (g x)
Tactic: simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ Sum.elim v xs
      (Sum.map (β := Fin n ⊕ Fin m) id (⇑finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m))
        ((Equiv.sumAssoc β (Fin n) (Fin m) : (a : (β ⊕ Fin n) ⊕ Fin m) → β ⊕ Fin n ⊕ Fin m) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)
have h : ∀ (l : β),
  Sum.elim v xs
      (Sum.map (β := Fin n ⊕ Fin m) id (⇑finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m))
        ((Equiv.sumAssoc β (Fin n) (Fin m) : (a : (β ⊕ Fin n) ⊕ Fin m) → β ⊕ Fin n ⊕ Fin m) (Sum.inl (Sum.inl l)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inl l)
Tactic: rcases g x with l | r
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
h :
  ∀ (l : β),
    Sum.elim v xs
        (Sum.map (β := Fin n ⊕ Fin m) id (⇑finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m))
          ((Equiv.sumAssoc β (Fin n) (Fin m) : (a : (β ⊕ Fin n) ⊕ Fin m) → β ⊕ Fin n ⊕ Fin m) (Sum.inl (Sum.inl l)))) =
      Sum.elim v (xs ∘ castAdd m) (Sum.inl l)
⊢ Sum.elim v xs
      (Sum.map (β := Fin n ⊕ Fin m) id (⇑finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m))
        ((Equiv.sumAssoc β (Fin n) (Fin m) : (a : (β ⊕ Fin n) ⊕ Fin m) → β ⊕ Fin n ⊕ Fin m) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)
have h₁ : ∀ (r : Fin n),
  Sum.elim v xs
      (Sum.map (β := Fin n ⊕ Fin m) id (⇑finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m))
        ((Equiv.sumAssoc β (Fin n) (Fin m) : (a : (β ⊕ Fin n) ⊕ Fin m) → β ⊕ Fin n ⊕ Fin m) (Sum.inl (Sum.inr r)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inr r)
Tactic: rcases g x with l | r
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
α : Type u'
n k : ℕ
⊢ Eq.{u' + 1} (α := α ⊕ Fin k → α ⊕ Fin (n + k)) (relabelAux Sum.inl k) (Sum.map id (natAdd n))
have h : ∀ (x : α ⊕ Fin k), relabelAux Sum.inl k x = Sum.map id (natAdd n) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
α : Type u'
n k : ℕ
x : α ⊕ Fin k
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x
have h : ∀ (val : α), relabelAux Sum.inl k (Sum.inl val) = Sum.map id (natAdd n) (Sum.inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
α : Type u'
n k : ℕ
x : α ⊕ Fin k
h : ∀ (val : α), relabelAux Sum.inl k (Sum.inl val) = Sum.map id (natAdd n) (Sum.inl val)
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x
have h₁ : ∀ (val : Fin k),
  Eq.{u' + 1} (α := α ⊕ Fin (n + k)) (relabelAux Sum.inl k (Sum.inr val)) (Sum.map id (natAdd n) (Sum.inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ relabel Sum.inl φ = castLE ⋯ φ
have simp : Eq (α := L.BoundedFormula α (0 + n))
  (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
    (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) φ)
  (castLE sorry φ)
Tactic: simp only [relabel, relabelAux_sumInl]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ Eq (α := L.BoundedFormula α (0 + n_1))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (rel R ts))
    (castLE ⋯ (rel R ts))
have rel : Eq (α := Fin l → Term.{u, v, u'} L (α ⊕ Fin (0 + n_1)))
  (fun (i : Fin l) ↦ Term.relabel (Sum.map id (Fin.cast sorry)) (ts i)) (Term.relabel (Sum.map id (Fin.cast sorry)) ∘ ts)
Tactic: simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
    (castLE ⋯ φ)
have falsum : ∀ {n : ℕ},
  Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (L := L) (α := α)
      (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun (x : ℕ) ↦ id)
      (fun (x : ℕ) ↦ castLE sorry) falsum)
    (castLE sorry falsum)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
  | rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
  | imp _ _ ih1 ih2 => simp_all [mapTermRel]
  | all _ ih3 => simp_all [mapTermRel]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (L := L) (α := α)
        (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun (x : ℕ) ↦ id)
        (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
      (castLE ⋯ BoundedFormula.falsum)
⊢ Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
    (castLE ⋯ φ)
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
  Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) (equal t₁ t₂))
    (castLE sorry (equal t₁ t₂))
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
  | rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
  | imp _ _ ih1 ih2 => simp_all [mapTermRel]
  | all _ ih3 => simp_all [mapTermRel]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (L := L) (α := α)
        (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun (x : ℕ) ↦ id)
        (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
      (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.equal t₁ t₂))
      (castLE ⋯ (BoundedFormula.equal t₁ t₂))
⊢ Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
    (castLE ⋯ φ)
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
  Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) (rel R ts))
    (castLE sorry (rel R ts))
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
  | rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
  | imp _ _ ih1 ih2 => simp_all [mapTermRel]
  | all _ ih3 => simp_all [mapTermRel]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (L := L) (α := α)
        (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun (x : ℕ) ↦ id)
        (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
      (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.equal t₁ t₂))
      (castLE ⋯ (BoundedFormula.equal t₁ t₂))
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.rel R ts))
      (castLE ⋯ (BoundedFormula.rel R ts))
⊢ Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
    (castLE ⋯ φ)
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 :
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) f₁)
      (castLE sorry f₁))
  (ih2 :
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) f₂)
      (castLE sorry f₂)),
  Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) (f₁.imp f₂))
    (castLE sorry (f₁.imp f₂))
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
  | rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
  | imp _ _ ih1 ih2 => simp_all [mapTermRel]
  | all _ ih3 => simp_all [mapTermRel]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (L := L) (α := α)
        (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun (x : ℕ) ↦ id)
        (fun (x : ℕ) ↦ castLE ⋯) BoundedFormula.falsum)
      (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.equal t₁ t₂))
      (castLE ⋯ (BoundedFormula.equal t₁ t₂))
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (BoundedFormula.rel R ts))
      (castLE ⋯ (BoundedFormula.rel R ts))
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      Eq (α := L.BoundedFormula α (0 + n))
        (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₁)
        (castLE ⋯ f₁))
    (ih2 :
      Eq (α := L.BoundedFormula α (0 + n))
        (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f₂)
        (castLE ⋯ f₂)),
    Eq (α := L.BoundedFormula α (0 + n))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) (f₁.imp f₂))
      (castLE ⋯ (f₁.imp f₂))
⊢ Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)
    (castLE ⋯ φ)
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 :
    Eq (α := L.BoundedFormula α (0 + (n + 1)))
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
        (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) f)
      (castLE sorry f)),
  Eq (α := L.BoundedFormula α (0 + n))
    (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (Sum.map id (natAdd 0)) t)
      (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE sorry) f.all)
    (castLE sorry f.all)
Tactic: induction φ with
  | falsum => rfl
  | equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
  | rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
  | imp _ _ ih1 ih2 => simp_all [mapTermRel]
  | all _ ih3 => simp_all [mapTermRel]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
⊢ Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (LHom.id L).onBoundedFormula id
have h : ∀ (f : L.BoundedFormula α n), (LHom.id L).onBoundedFormula f = id f
Tactic: ext f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
have h : ((LHom.id L).onTerm t₁).bdEqual ((LHom.id L).onTerm t₂) = id (equal t₁ t₂)
Tactic: rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
h : ((LHom.id L).onTerm t₁).bdEqual ((LHom.id L).onTerm t₂) = id (equal t₁ t₂)
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
have h₁ : (id t₁).bdEqual (id t₂) = id (equal t₁ t₂)
Tactic: rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
h : ((LHom.id L).onTerm t₁).bdEqual ((LHom.id L).onTerm t₂) = id (equal t₁ t₂)
h₁ : (id t₁).bdEqual (id t₂) = id (equal t₁ t₂)
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
have h₂ : t₁.bdEqual (id t₂) = id (equal t₁ t₂)
Tactic: rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
h : ((LHom.id L).onTerm t₁).bdEqual ((LHom.id L).onTerm t₂) = id (equal t₁ t₂)
h₁ : (id t₁).bdEqual (id t₂) = id (equal t₁ t₂)
h₂ : t₁.bdEqual (id t₂) = id (equal t₁ t₂)
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
have h₃ : t₁.bdEqual t₂ = id (equal t₁ t₂)
Tactic: rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
h : ((LHom.id L).onTerm t₁).bdEqual ((LHom.id L).onTerm t₂) = id (equal t₁ t₂)
h₁ : (id t₁).bdEqual (id t₂) = id (equal t₁ t₂)
h₂ : t₁.bdEqual (id t₂) = id (equal t₁ t₂)
h₃ : t₁.bdEqual t₂ = id (equal t₁ t₂)
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
have h₄ : t₁.bdEqual t₂ = equal t₁ t₂
Tactic: rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
h : ((LHom.id L).onTerm t₁).bdEqual ((LHom.id L).onTerm t₂) = id (equal t₁ t₂)
h₁ : (id t₁).bdEqual (id t₂) = id (equal t₁ t₂)
h₂ : t₁.bdEqual (id t₂) = id (equal t₁ t₂)
h₃ : t₁.bdEqual t₂ = id (equal t₁ t₂)
h₄ : t₁.bdEqual t₂ = equal t₁ t₂
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
have h₅ : equal t₁ t₂ = equal t₁ t₂
Tactic: rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ (LHom.id L).onBoundedFormula (rel R ts) = id (rel R ts)
have h : ((LHom.id L).onRelation R).boundedFormula (id ∘ ts) = id (rel R ts)
Tactic: rw [onBoundedFormula, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁
ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
have h : ((LHom.id L).onBoundedFormula f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
Tactic: rw [onBoundedFormula, ih1, ih2, id, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁
ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂
h : ((LHom.id L).onBoundedFormula f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
have h₁ : (id f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
Tactic: rw [onBoundedFormula, ih1, ih2, id, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁
ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂
h : ((LHom.id L).onBoundedFormula f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₁ : (id f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
have h₂ : (id f₁).imp (id f₂) = id (f₁.imp f₂)
Tactic: rw [onBoundedFormula, ih1, ih2, id, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁
ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂
h : ((LHom.id L).onBoundedFormula f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₁ : (id f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₂ : (id f₁).imp (id f₂) = id (f₁.imp f₂)
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
have h₃ : f₁.imp (id f₂) = id (f₁.imp f₂)
Tactic: rw [onBoundedFormula, ih1, ih2, id, id, id]