awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.onTerm ∘ φ.invLHom.onTerm) id
rw₁ : Eq (α := L'.Term α → L'.Term α) (φ.toLHom.comp φ.invLHom).onTerm id
rw₂ : Eq (α := L'.Term α → L'.Term α) (LHom.id L').onTerm id
⊢ Function.RightInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm
have rw₃ : Eq (α := L'.Term α → L'.Term α) id id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
h : n ≤ n
φ : L.BoundedFormula α n
⊢ castLE h φ = φ
have falsum : ∀ {n : ℕ} (h : n ≤ n), Eq (α := L.BoundedFormula α n) (castLE h falsum) falsum
Tactic: induction φ with
  | falsum => rfl
  | equal => simp
  | rel => simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => simp [ih3]
Cleared hypotheses: h, φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
h : n ≤ n
φ : L.BoundedFormula α n
falsum : ∀ {n : ℕ} (h : n ≤ n), Eq (α := L.BoundedFormula α n) (castLE h BoundedFormula.falsum) BoundedFormula.falsum
⊢ castLE h φ = φ
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (h : n ≤ n), castLE h (equal t₁ t₂) = equal t₁ t₂
Tactic: induction φ with
  | falsum => rfl
  | equal => simp
  | rel => simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => simp [ih3]
Cleared hypotheses: h, φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
h : n ≤ n
φ : L.BoundedFormula α n
falsum : ∀ {n : ℕ} (h : n ≤ n), Eq (α := L.BoundedFormula α n) (castLE h BoundedFormula.falsum) BoundedFormula.falsum
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (h : n ≤ n),
    castLE h (BoundedFormula.equal t₁ t₂) = BoundedFormula.equal t₁ t₂
⊢ castLE h φ = φ
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) (h : n ≤ n), castLE h (rel R ts) = rel R ts
Tactic: induction φ with
  | falsum => rfl
  | equal => simp
  | rel => simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => simp [ih3]
Cleared hypotheses: h, φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
h : n ≤ n
φ : L.BoundedFormula α n
falsum : ∀ {n : ℕ} (h : n ≤ n), Eq (α := L.BoundedFormula α n) (castLE h BoundedFormula.falsum) BoundedFormula.falsum
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (h : n ≤ n),
    castLE h (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)) (h : n ≤ n),
    castLE h (BoundedFormula.rel R ts) = BoundedFormula.rel R ts
⊢ castLE h φ = φ
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n) (ih1 : ∀ (h : n ≤ n), castLE h f₁ = f₁) (ih2 : ∀ (h : n ≤ n), castLE h f₂ = f₂)
  (h : n ≤ n), castLE h (f₁.imp f₂) = f₁.imp f₂
Tactic: induction φ with
  | falsum => rfl
  | equal => simp
  | rel => simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => simp [ih3]
Cleared hypotheses: h, φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
h : n ≤ n
φ : L.BoundedFormula α n
falsum : ∀ {n : ℕ} (h : n ≤ n), Eq (α := L.BoundedFormula α n) (castLE h BoundedFormula.falsum) BoundedFormula.falsum
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) (h : n ≤ n),
    castLE h (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)) (h : n ≤ n),
    castLE h (BoundedFormula.rel R ts) = BoundedFormula.rel R ts
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n) (ih1 : ∀ (h : n ≤ n), castLE h f₁ = f₁)
    (ih2 : ∀ (h : n ≤ n), castLE h f₂ = f₂) (h : n ≤ n), castLE h (f₁.imp f₂) = f₁.imp f₂
⊢ castLE h φ = φ
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1)) (ih3 : ∀ (h : n + 1 ≤ n + 1), castLE h f = f) (h : n ≤ n),
  castLE h f.all = f.all
Tactic: induction φ with
  | falsum => rfl
  | equal => simp
  | rel => simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => simp [ih3]
Cleared hypotheses: h, φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k m n : ℕ
km : k ≤ m
mn : m ≤ n
φ : L.BoundedFormula α k
⊢ castLE mn (castLE km φ) = castLE ⋯ φ
have revert : ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE sorry φ
Tactic: revert m n
Cleared hypotheses: m, n, km, mn
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k n l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
m n_1 : ℕ
km : n ≤ m
mn : m ≤ n_1
⊢ rel R (Term.relabel (Sum.map id (Fin.castLE mn)) ∘ Term.relabel (Sum.map id (Fin.castLE km)) ∘ ts) =
    rel R (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts)
have rel : rel R (Term.relabel (Sum.map id (Fin.castLE mn) ∘ Sum.map id (Fin.castLE km)) ∘ ts) =
  rel R (Term.relabel (Sum.map id (Fin.castLE sorry)) ∘ ts)
Tactic: rw [← Function.comp_assoc, Term.relabel_comp_relabel]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ
have falsum : ∀ {n m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
  Eq (α := L.BoundedFormula α n_1) (castLE mn (castLE km falsum)) (castLE sorry falsum)
Tactic: induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
falsum :
  ∀ {n m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    Eq (α := L.BoundedFormula α n_1) (castLE mn (castLE km BoundedFormula.falsum)) (castLE ⋯ BoundedFormula.falsum)
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
  castLE mn (castLE km (equal t₁ t₂)) = castLE sorry (equal t₁ t₂)
Tactic: induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
falsum :
  ∀ {n m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    Eq (α := L.BoundedFormula α n_1) (castLE mn (castLE km BoundedFormula.falsum)) (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    castLE mn (castLE km (BoundedFormula.equal t₁ t₂)) = castLE ⋯ (BoundedFormula.equal t₁ t₂)
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
  castLE mn (castLE km (rel R ts)) = castLE sorry (rel R ts)
Tactic: induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
falsum :
  ∀ {n m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    Eq (α := L.BoundedFormula α n_1) (castLE mn (castLE km BoundedFormula.falsum)) (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    castLE mn (castLE km (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)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    castLE mn (castLE km (BoundedFormula.rel R ts)) = castLE ⋯ (BoundedFormula.rel R ts)
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 : ∀ {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1), castLE mn (castLE km f₁) = castLE sorry f₁)
  (ih2 : ∀ {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1), castLE mn (castLE km f₂) = castLE sorry f₂) {m n_1 : ℕ} (km : n ≤ m)
  (mn : m ≤ n_1), castLE mn (castLE km (f₁.imp f₂)) = castLE sorry (f₁.imp f₂)
Tactic: induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
falsum :
  ∀ {n m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    Eq (α := L.BoundedFormula α n_1) (castLE mn (castLE km BoundedFormula.falsum)) (castLE ⋯ BoundedFormula.falsum)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    castLE mn (castLE km (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)) {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1),
    castLE mn (castLE km (BoundedFormula.rel R ts)) = castLE ⋯ (BoundedFormula.rel R ts)
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : ∀ {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1), castLE mn (castLE km f₁) = castLE ⋯ f₁)
    (ih2 : ∀ {m n_1 : ℕ} (km : n ≤ m) (mn : m ≤ n_1), castLE mn (castLE km f₂) = castLE ⋯ f₂) {m n_1 : ℕ} (km : n ≤ m)
    (mn : m ≤ n_1), castLE mn (castLE km (f₁.imp f₂)) = castLE ⋯ (f₁.imp f₂)
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 : ∀ {m n_1 : ℕ} (km : n + 1 ≤ m) (mn : m ≤ n_1), castLE mn (castLE km f) = castLE sorry f) {m n_1 : ℕ} (km : n ≤ m)
  (mn : m ≤ n_1), castLE mn (castLE km f.all) = castLE sorry f.all
Tactic: induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x n' m : ℕ
φ : L.BoundedFormula α x
x_1 : ℕ
⊢ x_1 + 1 + n' ≤ x_1 + n' + 1
have rw : x_1 + (1 + n') ≤ x_1 + n' + 1
Tactic: rw [add_assoc, add_comm 1, add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x n' m : ℕ
φ : L.BoundedFormula α x
x_1 : ℕ
rw : x_1 + (1 + n') ≤ x_1 + n' + 1
⊢ x_1 + 1 + n' ≤ x_1 + n' + 1
have rw₁ : x_1 + (n' + 1) ≤ x_1 + n' + 1
Tactic: rw [add_assoc, add_comm 1, add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x n' m : ℕ
φ : L.BoundedFormula α x
x_1 : ℕ
rw : x_1 + (1 + n') ≤ x_1 + n' + 1
rw₁ : x_1 + (n' + 1) ≤ x_1 + n' + 1
⊢ x_1 + 1 + n' ≤ x_1 + n' + 1
have rw₂ : x_1 + (n' + 1) ≤ x_1 + (n' + 1)
Tactic: rw [add_assoc, add_comm 1, add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
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 : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ) =
    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) φ
have falsum : ∀ {n : ℕ},
  Eq (α := L''.BoundedFormula γ n)
    (mapTermRel ft' fr' fun (x : ℕ) ↦ id (n := n) (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) falsum) :
      L''.BoundedFormula γ n)
    (mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (L' := L'') (α := α) (β := γ) (g := fun (x : ℕ) ↦ x)
        (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x) fun (x : ℕ) ↦ id (n := n) falsum :
      L''.BoundedFormula γ n)
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
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 : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula γ n)
      (mapTermRel ft' fr' fun (x : ℕ) ↦ id (n := n) (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum) :
        L''.BoundedFormula γ n)
      (mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (L' := L'') (α := α) (β := γ) (g := fun (x : ℕ) ↦ x)
          (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x) fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum :
        L''.BoundedFormula γ n)
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ) =
    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) φ
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
  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: 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
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 : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula γ n)
      (mapTermRel ft' fr' fun (x : ℕ) ↦ id (n := n) (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum) :
        L''.BoundedFormula γ n)
      (mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (L' := L'') (α := α) (β := γ) (g := fun (x : ℕ) ↦ x)
          (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x) fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum :
        L''.BoundedFormula γ n)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.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) (BoundedFormula.equal t₁ t₂)
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ) =
    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) φ
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
  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: 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
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 : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula γ n)
      (mapTermRel ft' fr' fun (x : ℕ) ↦ id (n := n) (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum) :
        L''.BoundedFormula γ n)
      (mapTermRel.{u, v, u', u_1, u_2, u_3} (L := L) (L' := L'') (α := α) (β := γ) (g := fun (x : ℕ) ↦ x)
          (fun (x : ℕ) ↦ ft' x ∘ ft x) (fun (x : ℕ) ↦ fr' x ∘ fr x) fun (x : ℕ) ↦ id (n := n) BoundedFormula.falsum :
        L''.BoundedFormula γ n)
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.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) (BoundedFormula.equal t₁ t₂)
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) (BoundedFormula.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) (BoundedFormula.rel R ts)
⊢ mapTermRel ft' fr' (fun (x : ℕ) ↦ id) (mapTermRel ft fr (fun (x : ℕ) ↦ id) φ) =
    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) φ
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (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: 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
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ = φ
have 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) falsum :
      L.BoundedFormula α n)
    (falsum : L.BoundedFormula α n)
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)
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ = φ
have 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)
      (equal t₁ t₂) =
    equal t₁ t₂
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₂
⊢ mapTermRel (L' := L) (β := α) (g := fun (x : ℕ) ↦ x) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ = φ
have 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)
      (rel R ts) =
    rel R ts
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: φ