awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions n
_ts : Fin n → L[[γ]].Term α
ih : ∀ (a : Fin n), (_ts a).constantsToVars.varsToConstants = _ts a
func :
  ∀ (f : L[[γ]].Functions 0) (_ts : Fin 0 → L[[γ]].Term α)
    (ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a),
    (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
func₁ :
  ∀ (n : ℕ) (f : L[[γ]].Functions (n + 1)) (_ts : Fin (n + 1) → L[[γ]].Term α)
    (ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a),
    (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
⊢ (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts

Tactic:
cases n
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a
func :
  ∀ (val : L.Functions 0),
    (Language.func (Sum.inl val) _ts).constantsToVars.varsToConstants = Language.func (Sum.inl val) _ts
func₁ :
  ∀ (val : (constantsOn γ).Functions 0),
    (Language.func (Sum.inr val) _ts).constantsToVars.varsToConstants = Language.func (Sum.inr val) _ts
⊢ (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts

Tactic:
cases f
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a
val : L.Functions 0
⊢ (func (Sum.inl val) _ts).constantsToVars.varsToConstants = func (Sum.inl val) _ts

Tactic:
simp [constantsToVars, varsToConstants, ih]

Premises used: FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.varsToConstants
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts a).constantsToVars.varsToConstants = _ts a
val : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val) _ts).constantsToVars.varsToConstants = func (Sum.inr val) _ts

Tactic:
simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]

Premises used: FirstOrder.Language.Constants.term, FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.varsToConstants, eq_iff_true_of_subsingleton
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions (n + 1)
_ts : Fin (n + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a
func :
  ∀ (val : L.Functions (n + 1)),
    (Language.func (Sum.inl val) _ts).constantsToVars.varsToConstants = Language.func (Sum.inl val) _ts
func₁ :
  ∀ (f : (constantsOn γ).Functions (n + 1)),
    (Language.func (Sum.inr f) _ts).constantsToVars.varsToConstants = Language.func (Sum.inr f) _ts
⊢ (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts

Tactic:
obtain - | f := f
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
_ts : Fin (n + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a
val : L.Functions (n + 1)
⊢ (func (Sum.inl val) _ts).constantsToVars.varsToConstants = func (Sum.inl val) _ts

Tactic:
simp [constantsToVars, varsToConstants, ih]

Premises used: FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.varsToConstants
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
_ts : Fin (n + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a
f : (constantsOn γ).Functions (n + 1)
⊢ (func (Sum.inr f) _ts).constantsToVars.varsToConstants = func (Sum.inr f) _ts

Tactic:
isEmptyElim f

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
_ts : Fin (n + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n + 1)), (_ts a).constantsToVars.varsToConstants = _ts a
f : (constantsOn γ).Functions (n + 1)
⊢ (func (Sum.inr f) _ts).constantsToVars.varsToConstants = func (Sum.inr f) _ts

Tactic:
exact isEmptyElim f
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L[[γ]].Term α
var : ∀ (a : α), Eq (α := L[[γ]].Term α) (varsToConstants (constantsToVars (Language.var a))) (Language.var a)
func :
  ∀ {n : ℕ} (f : L[[γ]].Functions n) (_ts : Fin n → L[[γ]].Term α)
    (ih : ∀ (a : Fin n), (_ts a).constantsToVars.varsToConstants = _ts a),
    (Language.func f _ts).constantsToVars.varsToConstants = Language.func f _ts
⊢ t.constantsToVars.varsToConstants = t

Tactic:
induction t with
    | var => rfl
    | @func n f _ ih =>
      cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f

Premises used: FirstOrder.Language.Constants.term, FirstOrder.Language.Term.func, FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.var, FirstOrder.Language.Term.varsToConstants, eq_iff_true_of_subsingleton
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
x : γ ⊕ α
var :
  ∀ (val : γ),
    Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var (Sum.inl val))))
      (Language.var (Sum.inl val))
var₁ :
  ∀ (val : α),
    Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var (Sum.inr val))))
      (Language.var (Sum.inr val))
⊢ Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var x))) (Language.var x)

Tactic:
cases x
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
val : γ
⊢ Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (var (Sum.inl val)))) (var (Sum.inl val))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
val : α
⊢ Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (var (Sum.inr val)))) (var (Sum.inr val))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L.Functions n
_ts : Fin n → L.Term (γ ⊕ α)
ih : ∀ (a : Fin n), (_ts a).varsToConstants.constantsToVars = _ts a
func :
  ∀ (f : L.Functions 0) (_ts : Fin 0 → L.Term (γ ⊕ α))
    (ih : ∀ (a : Fin 0), (_ts a).varsToConstants.constantsToVars = _ts a),
    (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts
func₁ :
  ∀ (n : ℕ) (f : L.Functions (n + 1)) (_ts : Fin (n + 1) → L.Term (γ ⊕ α))
    (ih : ∀ (a : Fin (n + 1)), (_ts a).varsToConstants.constantsToVars = _ts a),
    (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts
⊢ (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts

Tactic:
cases n
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts a).varsToConstants.constantsToVars = _ts a
⊢ (func f _ts).varsToConstants.constantsToVars = func f _ts

Tactic:
simp [varsToConstants, constantsToVars, ih]

Premises used: FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.varsToConstants
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L.Functions (n + 1)
_ts : Fin (n + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n + 1)), (_ts a).varsToConstants.constantsToVars = _ts a
⊢ (func f _ts).varsToConstants.constantsToVars = func f _ts

Tactic:
simp [varsToConstants, constantsToVars, ih]

Premises used: FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.varsToConstants
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L.Term (γ ⊕ α)
var : ∀ (x : γ ⊕ α), Eq (α := L.Term (γ ⊕ α)) (constantsToVars (varsToConstants (Language.var x))) (Language.var x)
func :
  ∀ {n : ℕ} (f : L.Functions n) (_ts : Fin n → L.Term (γ ⊕ α))
    (ih : ∀ (a : Fin n), (_ts a).varsToConstants.constantsToVars = _ts a),
    (Language.func f _ts).varsToConstants.constantsToVars = Language.func f _ts
⊢ t.varsToConstants.constantsToVars = t

Tactic:
induction t with
    | var x => cases x <;> rfl
    | @func n f _ ih => cases n <;> · simp [varsToConstants, constantsToVars, ih]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.var, FirstOrder.Language.Term.varsToConstants
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
t : L[[γ]].Term (α ⊕ β)
⊢ Eq (α := L.Term ((γ ⊕ α) ⊕ β))
    ((constantsVarsEquivLeft : (a : L[[γ]].Term (α ⊕ β)) → L.Term ((γ ⊕ α) ⊕ β)) t : L.Term ((γ ⊕ α) ⊕ β))
    (relabel (⇑(Equiv.sumAssoc γ α β).symm : (a : γ ⊕ α ⊕ β) → (γ ⊕ α) ⊕ β) t.constantsToVars : L.Term ((γ ⊕ α) ⊕ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
t : L.Term ((γ ⊕ α) ⊕ β)
⊢ Eq (α := L[[γ]].Term (α ⊕ β))
    ((_root_.Equiv.symm constantsVarsEquivLeft : (a : L.Term ((γ ⊕ α) ⊕ β)) → L[[γ]].Term (α ⊕ β)) t :
      L[[γ]].Term (α ⊕ β))
    (varsToConstants (relabel (⇑(Equiv.sumAssoc γ α β) : (a : (γ ⊕ α) ⊕ β) → γ ⊕ α ⊕ β) t) : L[[γ]].Term (α ⊕ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
t : L.Term α
var : ∀ (a : α), Eq (α := L.Term α) (substFunc (L := L) (Language.var a) fun {n : ℕ} ↦ Functions.term) (Language.var a)
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α),
    (∀ (a : Fin l), ((_ts a).substFunc fun {n : ℕ} ↦ Functions.term) = _ts a) →
      ((Language.func _f _ts).substFunc fun {n : ℕ} ↦ Functions.term) = Language.func _f _ts
⊢ (t.substFunc fun {n : ℕ} ↦ Functions.term) = t

Tactic:
induction t
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
a : α
⊢ Eq (α := L.Term α) (substFunc (L := L) (var a) fun {n : ℕ} ↦ Functions.term) (var a)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
h : ∀ (t : L.Term α), (LHom.id L).onTerm t = id t
⊢ Eq (α := L.Term α → L.Term α) (LHom.id L).onTerm id

Tactic:
ext t
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
a : α
⊢ (LHom.id L).onTerm (var a) = id (var a)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), (LHom.id L).onTerm (_ts a) = id (_ts a)
h : (func ((LHom.id L).onFunction _f) fun (i : Fin l) ↦ id (_ts i)) = id (func _f _ts)
⊢ (LHom.id L).onTerm (func _f _ts) = id (func _f _ts)

Tactic:
simp_rw [onTerm, ih]

Premises used: FirstOrder.Language.LHom.onTerm
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), (LHom.id L).onTerm (_ts a) = id (_ts a)
⊢ (func ((LHom.id L).onFunction _f) fun (i : Fin l) ↦ id (_ts i)) = id (func _f _ts)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
t : L.Term α
h : ∀ (a : α), (LHom.id L).onTerm (var a) = id (var a)
h₁ :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α) (ih : ∀ (a : Fin l), (LHom.id L).onTerm (_ts a) = id (_ts a)),
    (LHom.id L).onTerm (func _f _ts) = id (func _f _ts)
⊢ (LHom.id L).onTerm t = id t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl

Premises used: FirstOrder.Language.LHom.onTerm, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
h : ∀ (t : L.Term α), (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t
⊢ Eq (α := L.Term α → L''.Term α) (φ.comp ψ).onTerm (φ.onTerm ∘ ψ.onTerm)

Tactic:
ext t
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
a : α
⊢ (φ.comp ψ).onTerm (var a) = (φ.onTerm ∘ ψ.onTerm) (var a)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), (φ.comp ψ).onTerm (_ts a) = (φ.onTerm ∘ ψ.onTerm) (_ts a)
h :
  (func ((φ.comp ψ).onFunction _f) fun (i : Fin l) ↦ (φ.onTerm ∘ ψ.onTerm) (_ts i)) =
    (φ.onTerm ∘ ψ.onTerm) (func _f _ts)
⊢ (φ.comp ψ).onTerm (func _f _ts) = (φ.onTerm ∘ ψ.onTerm) (func _f _ts)

Tactic:
simp_rw [onTerm, ih]

Premises used: FirstOrder.Language.LHom.onTerm
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), (φ.comp ψ).onTerm (_ts a) = (φ.onTerm ∘ ψ.onTerm) (_ts a)
⊢ (func ((φ.comp ψ).onFunction _f) fun (i : Fin l) ↦ (φ.onTerm ∘ ψ.onTerm) (_ts i)) =
    (φ.onTerm ∘ ψ.onTerm) (func _f _ts)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
h : ∀ (a : α), (φ.comp ψ).onTerm (var a) = (φ.onTerm ∘ ψ.onTerm) (var a)
h₁ :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
    (ih : ∀ (a : Fin l), (φ.comp ψ).onTerm (_ts a) = (φ.onTerm ∘ ψ.onTerm) (_ts a)),
    (φ.comp ψ).onTerm (func _f _ts) = (φ.onTerm ∘ ψ.onTerm) (func _f _ts)
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl

Premises used: FirstOrder.Language.LHom.onTerm, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
rw : Eq (α := L.Term α → L.Term α) (φ.invLHom.onTerm ∘ φ.toLHom.onTerm) id
rw₁ : Eq (α := L.Term α → L.Term α) (φ.invLHom.comp φ.toLHom).onTerm id
rw₂ : Eq (α := L.Term α → L.Term α) (LHom.id L).onTerm id
rw₃ rw₄ : Eq (α := L.Term α → L.Term α) id id
⊢ Function.LeftInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]

Premises used: FirstOrder.Language.LHom.comp_onTerm, Function.leftInverse_iff_comp, FirstOrder.Language.LHom.id_onTerm, FirstOrder.Language.LEquiv.left_inv
-- Module: Mathlib.ModelTheory.Syntax
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
rw₃ rw₄ : Eq (α := L'.Term α → L'.Term α) id id
⊢ Function.RightInverse (α := L.Term α) φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]

Premises used: FirstOrder.Language.LEquiv.right_inv, Function.rightInverse_iff_comp, FirstOrder.Language.LHom.comp_onTerm, FirstOrder.Language.LHom.id_onTerm
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n _m _n : ℕ
h : _m ≤ _n
f : L.BoundedFormula α (_m + 1)
⊢ _m + 1 ≤ _n + 1

Tactic:
gcongr
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
h : n_1 ≤ n_1
⊢ Eq (α := L.BoundedFormula α n_1) (castLE h falsum) 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 : n_1 ≤ n_1
⊢ castLE h (equal t₁ t₂) = equal t₁ t₂

Tactic:
simp
-- 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 : n_1 ≤ n_1
⊢ castLE h (rel R ts) = rel R ts

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ (h : n_1 ≤ n_1), castLE h f₁ = f₁
ih2 : ∀ (h : n_1 ≤ n_1), castLE h f₂ = f₂
h : n_1 ≤ n_1
⊢ castLE h (f₁.imp f₂) = f₁.imp f₂

Tactic:
simp [ih1, ih2]
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ (h : n_1 + 1 ≤ n_1 + 1), castLE h f = f
h : n_1 ≤ n_1
⊢ castLE h f.all = f.all

Tactic:
simp [ih3]
-- Module: Mathlib.ModelTheory.Syntax
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₂
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
⊢ castLE h φ = φ

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

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
k m n : ℕ
km : k ≤ m
mn : m ≤ n
φ : L.BoundedFormula α k
revert : ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ
⊢ castLE mn (castLE km φ) = castLE ⋯ φ

Tactic:
revert m n
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
k n m n_1 : ℕ
km : n ≤ m
mn : m ≤ n_1
⊢ Eq (α := L.BoundedFormula α n_1) (castLE mn (castLE km falsum)) (castLE ⋯ falsum)

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

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
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 :
  BoundedFormula.rel R (Term.relabel (Sum.map id (Fin.castLE mn) ∘ Sum.map id (Fin.castLE km)) ∘ ts) =
    BoundedFormula.rel R (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts)
⊢ BoundedFormula.rel R (Term.relabel (Sum.map id (Fin.castLE mn)) ∘ Term.relabel (Sum.map id (Fin.castLE km)) ∘ ts) =
    BoundedFormula.rel R (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts)

Tactic:
rw [← Function.comp_assoc, Term.relabel_comp_relabel]

Premises used: FirstOrder.Language.Term.relabel_comp_relabel, Function.comp_assoc
-- Module: Mathlib.ModelTheory.Syntax
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) ∘ Sum.map id (Fin.castLE km)) ∘ ts) =
    rel R (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
k 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₂)

Tactic:
simp [ih1, ih2]
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
k n : ℕ
f : L.BoundedFormula α (n + 1)
ih3 : ∀ {m n_2 : ℕ} (km : n + 1 ≤ m) (mn : m ≤ n_2), castLE mn (castLE km f) = castLE ⋯ f
m n_1 : ℕ
km : n ≤ m
mn : m ≤ n_1
⊢ castLE mn (castLE km f.all) = castLE ⋯ f.all

Tactic:
simp only [castLE, ih3]

Premises used: FirstOrder.Language.BoundedFormula.castLE
-- Module: Mathlib.ModelTheory.Syntax
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₂)
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 ⋯ f) {m n_1 : ℕ} (km : n ≤ m)
    (mn : m ≤ n_1), castLE mn (castLE km f.all) = castLE ⋯ f.all
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ

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]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.Term.relabel_comp_relabel, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel, FirstOrder.Language.BoundedFormula.castLE, Function.comp_assoc
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
k m n : ℕ
km : k ≤ m
mn : m ≤ n
⊢ Eq (α := L.BoundedFormula α k → L.BoundedFormula α n) (castLE mn ∘ castLE km) (castLE ⋯)

Tactic:
funext (castLE_castLE km mn)

Premises used: FirstOrder.Language.BoundedFormula.castLE_castLE, funext
-- Module: Mathlib.ModelTheory.Syntax
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
rw₂ rw₃ : x_1 + (n' + 1) ≤ x_1 + (n' + 1)
⊢ x_1 + 1 + n' ≤ x_1 + n' + 1

Tactic:
rw [add_assoc, add_comm 1, add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- 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 : ℕ
⊢ Eq (α := L''.BoundedFormula γ n_1)
    (mapTermRel ft' fr' fun (x : ℕ) ↦ id (n := n_1) (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n_1) falsum) :
      L''.BoundedFormula γ n_1)
    (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_1) falsum :
      L''.BoundedFormula γ n_1)

Tactic:
rfl