awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
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
ft' : (n : ℕ) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n) → Term.{u_2, u_3, u_1} L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (equal t₁ t₂)) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) (equal t₁ t₂)

Tactic:
simp [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
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
ft' : (n : ℕ) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n) → Term.{u_2, u_3, u_1} L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (rel R ts)) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) (rel R ts)

Tactic:
simp [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
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
ft' : (n : ℕ) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n) → Term.{u_2, u_3, u_1} L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₁) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) f₁
ih2 :
  mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) f₂) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) f₂
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (f₁.imp f₂)) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) (f₁.imp f₂)

Tactic:
simp [mapTermRel, ih1, ih2]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
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
ft' : (n : ℕ) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n) → Term.{u_2, u_3, u_1} L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  mapTermRel.{u_4, u_5, v', u_1, u_2, u_3} (α := β) ft' fr' (fun (x : ℕ) ↦ id)
      (mapTermRel.{u, v, u', v', u_4, u_5} (α := α) ft fr (fun (x : ℕ) ↦ id) f) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (α := α) (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x)
      (fun (x : ℕ) ↦ id) f
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) f.all) =
    mapTermRel.{u, v, u', u_1, u_2, u_3} (L' := L'') (β := γ) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ ft' x ∘ ft x)
      (fun (x : ℕ) ↦ fr' x ∘ fr x) (fun (x : ℕ) ↦ id) f.all

Tactic:
simp [mapTermRel, ih3]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
⊢ Eq (α := L.BoundedFormula α n_1)
    (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_1) falsum :
      L.BoundedFormula α n_1)
    (falsum : L.BoundedFormula α n_1)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
      (equal t₁ t₂) =
    equal t₁ t₂

Tactic:
simp [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id)
      (rel R ts) =
    rel R ts

Tactic:
simp [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
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:
simp [mapTermRel, ih1, ih2]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 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:
simp [mapTermRel, ih3]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
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₂
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
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ = φ

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n_1 : ℕ
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) ≃ Term.{u_2, u_3, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → _root_.Equiv.{v + 1, u_3 + 1} (L.Relations n) (L'.Relations n)
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel.{u_2, u_3, v', u', u, v} (L := L') (L' := L) (α := β) (β := α) (g := fun (n : ℕ) ↦ n)
      (fun (n : ℕ) ↦ (⇑(ft n).symm : (a : L'.Term (β ⊕ Fin n)) → L.Term (α ⊕ Fin n)))
      (fun (n : ℕ) ↦ (⇑(fr n).symm : (a : L'.Relations n) → L.Relations n)) fun (x : ℕ) ↦ id (n := n)
      (mapTermRel.{u, v, u', v', u_2, u_3} (L' := L') (β := β) (g := fun (n : ℕ) ↦ n)
          (fun (n : ℕ) ↦ (⇑(ft n) : (a : L.Term (α ⊕ Fin n)) → L'.Term (β ⊕ Fin n)))
          (fun (n : ℕ) ↦ (⇑(fr n) : (a : L.Relations n) → L'.Relations n)) (fun (x : ℕ) ↦ id) φ :
        L'.BoundedFormula β n) =
    φ

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n_1 : ℕ
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) ≃ Term.{u_2, u_3, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → _root_.Equiv.{v + 1, u_3 + 1} (L.Relations n) (L'.Relations n)
n : ℕ
φ : L'.BoundedFormula β n
⊢ mapTermRel.{u, v, u', v', u_2, u_3} (L := L) (L' := L') (α := α) (β := β) (g := fun (n : ℕ) ↦ n)
      (fun (n : ℕ) ↦ (⇑(ft n) : (a : L.Term (α ⊕ Fin n)) → L'.Term (β ⊕ Fin n)))
      (fun (n : ℕ) ↦ (⇑(fr n) : (a : L.Relations n) → L'.Relations n)) fun (x : ℕ) ↦ id (n := n)
      (mapTermRel.{u_2, u_3, v', u', u, v} (L' := L) (β := α) (g := fun (n : ℕ) ↦ n)
          (fun (n : ℕ) ↦ (⇑(ft n).symm : (a : L'.Term (β ⊕ Fin n)) → L.Term (α ⊕ Fin n)))
          (fun (n : ℕ) ↦ (⇑(fr n).symm : (a : L'.Relations n) → L.Relations n)) (fun (x : ℕ) ↦ id) φ :
        L.BoundedFormula α n) =
    φ

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
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
⊢ Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Syntax
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)
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)
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x

Tactic:
rcases x with x | x
-- Module: Mathlib.ModelTheory.Syntax
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
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)
⊢ (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:
simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]

Premises used: Sum.map_inl, FirstOrder.Language.BoundedFormula.relabelAux, Sum.elim_inl, Function.comp_apply
-- Module: Mathlib.ModelTheory.Syntax
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)
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)
⊢ 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:
rcases g x with l | r
-- Module: Mathlib.ModelTheory.Syntax
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
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:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
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:
simp
-- Module: Mathlib.ModelTheory.Syntax
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) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)

Tactic:
simp [BoundedFormula.relabelAux]

Premises used: FirstOrder.Language.BoundedFormula.relabelAux
-- Module: Mathlib.ModelTheory.Syntax
Goal:
α : Type u'
n k : ℕ
h : ∀ (x : α ⊕ Fin k), relabelAux Sum.inl k x = Sum.map id (natAdd n) x
⊢ Eq.{u' + 1} (α := α ⊕ Fin k → α ⊕ Fin (n + k)) (relabelAux Sum.inl k) (Sum.map id (natAdd n))

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Syntax
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)
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))
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x

Tactic:
cases x
-- Module: Mathlib.ModelTheory.Syntax
Goal:
α : Type u'
n k : ℕ
val : α
⊢ relabelAux Sum.inl k (Sum.inl val) = Sum.map id (natAdd n) (Sum.inl val)

Tactic:
simp [relabelAux]

Premises used: FirstOrder.Language.BoundedFormula.relabelAux
-- Module: Mathlib.ModelTheory.Syntax
Goal:
α : Type u'
n k : ℕ
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:
simp [relabelAux]

Premises used: FirstOrder.Language.BoundedFormula.relabelAux
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
⊢ Eq (α := L.BoundedFormula β (n + k)) (relabel g falsum) falsum

Tactic:
rfl

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.relabel, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
⊢ Eq (α := L.BoundedFormula β (n + k)) (relabel g ⊥) ⊥

Tactic:
rfl

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.relabel, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ ψ : L.BoundedFormula α k
⊢ relabel g (φ.imp ψ) = (relabel g φ).imp (relabel g ψ)

Tactic:
rfl

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.relabel, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α k
⊢ relabel g φ.not = (relabel g φ).not

Tactic:
simp [BoundedFormula.not]

Premises used: FirstOrder.Language.BoundedFormula.not
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ Eq (α := L.BoundedFormula β (n + k))
    (all
      (castLE ⋯
        (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (relabelAux g x) t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) φ)))
    (all
      (mapTermRel (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.relabel (relabelAux g x) t) (fun (x : ℕ) ↦ id)
        (fun (x : ℕ) ↦ castLE ⋯) φ))

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ relabel g φ.ex = (relabel g φ).ex

Tactic:
simp [BoundedFormula.ex]

Premises used: FirstOrder.Language.BoundedFormula.ex
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
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 ⋯) φ)
    (castLE ⋯ φ)
⊢ relabel Sum.inl φ = castLE ⋯ φ

Tactic:
simp only [relabel, relabelAux_sumInl]

Premises used: FirstOrder.Language.BoundedFormula.relabelAux_sumInl, FirstOrder.Language.BoundedFormula.relabel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
⊢ Eq (α := L.BoundedFormula α (0 + n_1))
    (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 ⋯) falsum)
    (castLE ⋯ falsum)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
t₁ t₂ : 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 ⋯) (equal t₁ t₂))
    (castLE ⋯ (equal t₁ t₂))

Tactic:
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, Fin.castLE_of_eq, Fin.natAdd_zero
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
rel :
  Eq (α := Fin l → Term.{u, v, u'} L (α ⊕ Fin (0 + n_1)))
    (fun (i : Fin l) ↦ Term.relabel (Sum.map id (Fin.cast ⋯)) (ts i)) (Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts)
⊢ 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 ⋯) (BoundedFormula.rel R ts))
    (castLE ⋯ (BoundedFormula.rel R ts))

Tactic:
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, Fin.castLE_of_eq, Fin.natAdd_zero
-- Module: Mathlib.ModelTheory.Syntax
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 (α := Fin l → Term.{u, v, u'} L (α ⊕ Fin (0 + n_1)))
    (fun (i : Fin l) ↦ Term.relabel (Sum.map id (Fin.cast ⋯)) (ts i)) (Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  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 ⋯) f₁)
    (castLE ⋯ f₁)
ih2 :
  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 ⋯) f₂)
    (castLE ⋯ f₂)
⊢ 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 ⋯) (f₁.imp f₂))
    (castLE ⋯ (f₁.imp f₂))

Tactic:
simp_all [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 :
  Eq (α := L.BoundedFormula α (0 + (n_1 + 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 ⋯) f)
    (castLE ⋯ f)
⊢ 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 ⋯) f.all)
    (castLE ⋯ f.all)

Tactic:
simp_all [mapTermRel]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n : ℕ
h : ∀ (f : L.BoundedFormula α n), (LHom.id L).onBoundedFormula f = id f
⊢ Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (LHom.id L).onBoundedFormula id

Tactic:
ext f
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
⊢ Eq (α := L.BoundedFormula α n_1) ((LHom.id L).onBoundedFormula falsum) (id falsum)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
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₂
h₅ h₆ : equal t₁ t₂ = equal t₁ t₂
⊢ (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)

Tactic:
rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]

Premises used: FirstOrder.Language.Term.bdEqual, id, FirstOrder.Language.LHom.onBoundedFormula, FirstOrder.Language.LHom.id_onTerm
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
h : ((LHom.id L).onRelation R).boundedFormula (id ∘ ts) = id (rel R ts)
⊢ (LHom.id L).onBoundedFormula (rel R ts) = id (rel R ts)

Tactic:
rw [onBoundedFormula, LHom.id_onTerm]

Premises used: FirstOrder.Language.LHom.onBoundedFormula, FirstOrder.Language.LHom.id_onTerm
-- Module: Mathlib.ModelTheory.Syntax
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).onRelation R).boundedFormula (id ∘ ts) = id (rel R ts)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
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₂)
h₃ : f₁.imp (id f₂) = id (f₁.imp f₂)
h₄ : f₁.imp f₂ = id (f₁.imp f₂)
h₅ h₆ : f₁.imp f₂ = f₁.imp f₂
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)

Tactic:
rw [onBoundedFormula, ih1, ih2, id, id, id]

Premises used: id, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : (LHom.id L).onBoundedFormula f = id f
h : ((LHom.id L).onBoundedFormula f).all = id f.all
h₁ : (id f).all = id f.all
h₂ : f.all = id f.all
h₃ h₄ : f.all = f.all
⊢ (LHom.id L).onBoundedFormula f.all = id f.all

Tactic:
rw [onBoundedFormula, ih3, id, id]

Premises used: id, FirstOrder.Language.LHom.onBoundedFormula