[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
t : Term L α
⊢ relabel id t = t
[PROOFSTEP]
induction' t with _ _ _ _ ih
[GOAL]
case var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
_a✝ : α
⊢ relabel id (var _a✝) = var _a✝
[PROOFSTEP]
rfl
[GOAL]
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), relabel id (_ts✝ a) = _ts✝ a
⊢ relabel id (func _f✝ _ts✝) = func _f✝ _ts✝
[PROOFSTEP]
simp [ih]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
f : α → β
g : β → γ
t : Term L α
⊢ relabel g (relabel f t) = relabel (g ∘ f) t
[PROOFSTEP]
induction' t with _ _ _ _ ih
[GOAL]
case var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
f : α → β
g : β → γ
_a✝ : α
⊢ relabel g (relabel f (var _a✝)) = relabel (g ∘ f) (var _a✝)
[PROOFSTEP]
rfl
[GOAL]
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
f : α → β
g : β → γ
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), relabel g (relabel f (_ts✝ a)) = relabel (g ∘ f) (_ts✝ a)
⊢ relabel g (relabel f (func _f✝ _ts✝)) = relabel (g ∘ f) (func _f✝ _ts✝)
[PROOFSTEP]
simp [ih]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
g : α ≃ β
t : Term L α
⊢ relabel (↑g.symm) (relabel (↑g) t) = t
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
g : α ≃ β
t : Term L β
⊢ relabel (↑g) (relabel (↑g.symm) t) = t
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
⊢ Function.LeftInverse varsToConstants constantsToVars
[PROOFSTEP]
intro t
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
t : Term (L[[γ]]) α
⊢ varsToConstants (constantsToVars t) = t
[PROOFSTEP]
induction' t with _ n f _ ih
[GOAL]
case var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
_a✝ : α
⊢ varsToConstants (constantsToVars (var _a✝)) = var _a✝
[PROOFSTEP]
rfl
[GOAL]
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
f : Functions (L[[γ]]) n
_ts✝ : Fin n → Term (L[[γ]]) α
ih : ∀ (a : Fin n), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
⊢ varsToConstants (constantsToVars (func f _ts✝)) = func f _ts✝
[PROOFSTEP]
cases n
[GOAL]
case func.zero
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
f : Functions (L[[γ]]) Nat.zero
_ts✝ : Fin Nat.zero → Term (L[[γ]]) α
ih : ∀ (a : Fin Nat.zero), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
⊢ varsToConstants (constantsToVars (func f _ts✝)) = func f _ts✝
[PROOFSTEP]
cases f
[GOAL]
case func.zero.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
_ts✝ : Fin Nat.zero → Term (L[[γ]]) α
ih : ∀ (a : Fin Nat.zero), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
val✝ : Functions L Nat.zero
⊢ varsToConstants (constantsToVars (func (Sum.inl val✝) _ts✝)) = func (Sum.inl val✝) _ts✝
[PROOFSTEP]
simp [constantsToVars, varsToConstants, ih]
[GOAL]
case func.zero.inr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
_ts✝ : Fin Nat.zero → Term (L[[γ]]) α
ih : ∀ (a : Fin Nat.zero), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
val✝ : Functions (constantsOn γ) Nat.zero
⊢ varsToConstants (constantsToVars (func (Sum.inr val✝) _ts✝)) = func (Sum.inr val✝) _ts✝
[PROOFSTEP]
simp [constantsToVars, varsToConstants, Constants.term]
[GOAL]
case func.succ
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
f : Functions (L[[γ]]) (Nat.succ n✝)
_ts✝ : Fin (Nat.succ n✝) → Term (L[[γ]]) α
ih : ∀ (a : Fin (Nat.succ n✝)), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
⊢ varsToConstants (constantsToVars (func f _ts✝)) = func f _ts✝
[PROOFSTEP]
cases' f with f f
[GOAL]
case func.succ.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
_ts✝ : Fin (Nat.succ n✝) → Term (L[[γ]]) α
ih : ∀ (a : Fin (Nat.succ n✝)), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
f : Functions L (Nat.succ n✝)
⊢ varsToConstants (constantsToVars (func (Sum.inl f) _ts✝)) = func (Sum.inl f) _ts✝
[PROOFSTEP]
simp [constantsToVars, varsToConstants, ih]
[GOAL]
case func.succ.inr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
_ts✝ : Fin (Nat.succ n✝) → Term (L[[γ]]) α
ih : ∀ (a : Fin (Nat.succ n✝)), varsToConstants (constantsToVars (_ts✝ a)) = _ts✝ a
f : Functions (constantsOn γ) (Nat.succ n✝)
⊢ varsToConstants (constantsToVars (func (Sum.inr f) _ts✝)) = func (Sum.inr f) _ts✝
[PROOFSTEP]
exact isEmptyElim f
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
⊢ Function.RightInverse varsToConstants constantsToVars
[PROOFSTEP]
intro t
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
t : Term L (γ ⊕ α)
⊢ constantsToVars (varsToConstants t) = t
[PROOFSTEP]
induction' t with x n f _ ih
[GOAL]
case var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
x : γ ⊕ α
⊢ constantsToVars (varsToConstants (var x)) = var x
[PROOFSTEP]
cases x
[GOAL]
case var.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
val✝ : γ
⊢ constantsToVars (varsToConstants (var (Sum.inl val✝))) = var (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case var.inr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
val✝ : α
⊢ constantsToVars (varsToConstants (var (Sum.inr val✝))) = var (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
f : Functions L n
_ts✝ : Fin n → Term L (γ ⊕ α)
ih : ∀ (a : Fin n), constantsToVars (varsToConstants (_ts✝ a)) = _ts✝ a
⊢ constantsToVars (varsToConstants (func f _ts✝)) = func f _ts✝
[PROOFSTEP]
cases n
[GOAL]
case func.zero
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
f : Functions L Nat.zero
_ts✝ : Fin Nat.zero → Term L (γ ⊕ α)
ih : ∀ (a : Fin Nat.zero), constantsToVars (varsToConstants (_ts✝ a)) = _ts✝ a
⊢ constantsToVars (varsToConstants (func f _ts✝)) = func f _ts✝
[PROOFSTEP]
simp [varsToConstants, constantsToVars, ih]
[GOAL]
case func.succ
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
f : Functions L (Nat.succ n✝)
_ts✝ : Fin (Nat.succ n✝) → Term L (γ ⊕ α)
ih : ∀ (a : Fin (Nat.succ n✝)), constantsToVars (varsToConstants (_ts✝ a)) = _ts✝ a
⊢ constantsToVars (varsToConstants (func f _ts✝)) = func f _ts✝
[PROOFSTEP]
simp [varsToConstants, constantsToVars, ih]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
⊢ onTerm (LHom.id L) = id
[PROOFSTEP]
ext t
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
t : Term L α
⊢ onTerm (LHom.id L) t = id t
[PROOFSTEP]
induction' t with _ _ _ _ ih
[GOAL]
case h.var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
_a✝ : α
⊢ onTerm (LHom.id L) (var _a✝) = id (var _a✝)
[PROOFSTEP]
rfl
[GOAL]
case h.func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (LHom.id L) (_ts✝ a) = id (_ts✝ a)
⊢ onTerm (LHom.id L) (func _f✝ _ts✝) = id (func _f✝ _ts✝)
[PROOFSTEP]
simp_rw [onTerm, ih]
[GOAL]
case h.func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (LHom.id L) (_ts✝ a) = id (_ts✝ a)
⊢ (func (onFunction (LHom.id L) _f✝) fun i => id (_ts✝ i)) = id (func _f✝ _ts✝)
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ onTerm (comp φ ψ) = onTerm φ ∘ onTerm ψ
[PROOFSTEP]
ext t
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : Term L α
⊢ onTerm (comp φ ψ) t = (onTerm φ ∘ onTerm ψ) t
[PROOFSTEP]
induction' t with _ _ _ _ ih
[GOAL]
case h.var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
_a✝ : α
⊢ onTerm (comp φ ψ) (var _a✝) = (onTerm φ ∘ onTerm ψ) (var _a✝)
[PROOFSTEP]
rfl
[GOAL]
case h.func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (comp φ ψ) (_ts✝ a) = (onTerm φ ∘ onTerm ψ) (_ts✝ a)
⊢ onTerm (comp φ ψ) (func _f✝ _ts✝) = (onTerm φ ∘ onTerm ψ) (func _f✝ _ts✝)
[PROOFSTEP]
simp_rw [onTerm, ih]
[GOAL]
case h.func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
ih : ∀ (a : Fin l✝), onTerm (comp φ ψ) (_ts✝ a) = (onTerm φ ∘ onTerm ψ) (_ts✝ a)
⊢ (func (onFunction (comp φ ψ) _f✝) fun i => (onTerm φ ∘ onTerm ψ) (_ts✝ i)) = (onTerm φ ∘ onTerm ψ) (func _f✝ _ts✝)
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
φ : L ≃ᴸ L'
⊢ Function.LeftInverse (LHom.onTerm φ.invLHom) (LHom.onTerm φ.toLHom)
[PROOFSTEP]
rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
φ : L ≃ᴸ L'
⊢ Function.RightInverse (LHom.onTerm φ.invLHom) (LHom.onTerm φ.toLHom)
[PROOFSTEP]
rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ n : ℕ
h : n ≤ n
φ : BoundedFormula L α n
⊢ castLE h φ = φ
[PROOFSTEP]
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
h : n✝ ≤ n✝
⊢ castLE h falsum = falsum
[PROOFSTEP]
rfl
[GOAL]
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (equal t₁✝ t₂✝) = equal t₁✝ t₂✝
[PROOFSTEP]
simp [Fin.castLE_of_eq]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (rel R✝ ts✝) = rel R✝ ts✝
[PROOFSTEP]
simp [Fin.castLE_of_eq]
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ (h : n✝ ≤ n✝), castLE h f₁✝ = f₁✝
ih2 : ∀ (h : n✝ ≤ n✝), castLE h f₂✝ = f₂✝
h : n✝ ≤ n✝
⊢ castLE h (imp f₁✝ f₂✝) = imp f₁✝ f₂✝
[PROOFSTEP]
simp [Fin.castLE_of_eq, ih1, ih2]
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n : ℕ
h✝ : n ≤ n
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ (h : n✝ + 1 ≤ n✝ + 1), castLE h f✝ = f✝
h : n✝ ≤ n✝
⊢ castLE h (all f✝) = all f✝
[PROOFSTEP]
simp [Fin.castLE_of_eq, ih3]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ k m n : ℕ
km : k ≤ m
mn : m ≤ n
φ : BoundedFormula L α k
⊢ castLE mn (castLE km φ) = castLE (_ : k ≤ n) φ
[PROOFSTEP]
revert m n
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k : ℕ
φ : BoundedFormula L α k
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE (_ : k ≤ n) φ
[PROOFSTEP]
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k n✝ : ℕ
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km falsum) = castLE (_ : n✝ ≤ n) falsum
[PROOFSTEP]
intro m n km mn
[GOAL]
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (equal t₁✝ t₂✝)) = castLE (_ : n✝ ≤ n) (equal t₁✝ t₂✝)
[PROOFSTEP]
intro m n km mn
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (rel R✝ ts✝)) = castLE (_ : n✝ ≤ n) (rel R✝ ts✝)
[PROOFSTEP]
intro m n km mn
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₁✝) = castLE (_ : n✝ ≤ n) f₁✝
ih2 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₂✝) = castLE (_ : n✝ ≤ n) f₂✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (imp f₁✝ f₂✝)) = castLE (_ : n✝ ≤ n) (imp f₁✝ f₂✝)
[PROOFSTEP]
intro m n km mn
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE (_ : n✝ + 1 ≤ n) f✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (all f✝)) = castLE (_ : n✝ ≤ n) (all f✝)
[PROOFSTEP]
intro m n km mn
[GOAL]
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ castLE mn (castLE km falsum) = castLE (_ : n✝ ≤ n) falsum
[PROOFSTEP]
rfl
[GOAL]
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ castLE mn (castLE km (equal t₁✝ t₂✝)) = castLE (_ : n✝ ≤ n) (equal t₁✝ t₂✝)
[PROOFSTEP]
simp
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ castLE mn (castLE km (rel R✝ ts✝)) = castLE (_ : n✝ ≤ n) (rel R✝ ts✝)
[PROOFSTEP]
simp only [castLE, eq_self_iff_true, heq_iff_eq, true_and_iff]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ 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 (_ : n✝ ≤ n))) ∘ ts✝)
[PROOFSTEP]
rw [← Function.comp.assoc, Term.relabel_comp_relabel]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ 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 (_ : n✝ ≤ n))) ∘ ts✝)
[PROOFSTEP]
simp
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₁✝) = castLE (_ : n✝ ≤ n) f₁✝
ih2 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₂✝) = castLE (_ : n✝ ≤ n) f₂✝
m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ castLE mn (castLE km (imp f₁✝ f₂✝)) = castLE (_ : n✝ ≤ n) (imp f₁✝ f₂✝)
[PROOFSTEP]
simp [ih1, ih2]
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ k n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE (_ : n✝ + 1 ≤ n) f✝
m n : ℕ
km : n✝ ≤ m
mn : m ≤ n
⊢ castLE mn (castLE km (all f✝)) = castLE (_ : n✝ ≤ n) (all f✝)
[PROOFSTEP]
simp only [castLE, ih3]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ n n' m : ℕ
φ : BoundedFormula L α n
x✝ : ℕ
⊢ x✝ + 1 + n' ≤ x✝ + n' + 1
[PROOFSTEP]
rw [add_assoc, add_comm 1, add_assoc]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
L'' : Language
ft : (n : ℕ) → Term L (α ⊕ Fin n) → Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n → Relations L' n
ft' : (n : ℕ) → Term L' (β ⊕ Fin n) → Term L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → Relations L' n → Relations L'' n
n : ℕ
φ : BoundedFormula L α n
⊢ mapTermRel ft' fr' (fun x => id) (mapTermRel ft fr (fun x => id) φ) =
    mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) φ
[PROOFSTEP]
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ : ℕ
L'' : Language
ft : (n : ℕ) → Term L (α ⊕ Fin n) → Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n → Relations L' n
ft' : (n : ℕ) → Term L' (β ⊕ Fin n) → Term L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → Relations L' n → Relations L'' n
n n✝ : ℕ
⊢ mapTermRel ft' fr' (fun x => id) (mapTermRel ft fr (fun x => id) falsum) =
    mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) falsum
[PROOFSTEP]
rfl
[GOAL]
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ : ℕ
L'' : Language
ft : (n : ℕ) → Term L (α ⊕ Fin n) → Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n → Relations L' n
ft' : (n : ℕ) → Term L' (β ⊕ Fin n) → Term L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → Relations L' n → Relations L'' n
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ mapTermRel ft' fr' (fun x => id) (mapTermRel ft fr (fun x => id) (equal t₁✝ t₂✝)) =
    mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) (equal t₁✝ t₂✝)
[PROOFSTEP]
simp [mapTermRel]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ : ℕ
L'' : Language
ft : (n : ℕ) → Term L (α ⊕ Fin n) → Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n → Relations L' n
ft' : (n : ℕ) → Term L' (β ⊕ Fin n) → Term L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → Relations L' n → Relations L'' n
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ mapTermRel ft' fr' (fun x => id) (mapTermRel ft fr (fun x => id) (rel R✝ ts✝)) =
    mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) (rel R✝ ts✝)
[PROOFSTEP]
simp [mapTermRel]
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ : ℕ
L'' : Language
ft : (n : ℕ) → Term L (α ⊕ Fin n) → Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n → Relations L' n
ft' : (n : ℕ) → Term L' (β ⊕ Fin n) → Term L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → Relations L' n → Relations L'' n
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  mapTermRel ft' fr' (fun x => id) (mapTermRel ft fr (fun x => id) f₁✝) =
    mapTermRel (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 (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) (imp f₁✝ f₂✝)) =
    mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) (imp f₁✝ f₂✝)
[PROOFSTEP]
simp [mapTermRel, ih1, ih2]
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ : ℕ
L'' : Language
ft : (n : ℕ) → Term L (α ⊕ Fin n) → Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n → Relations L' n
ft' : (n : ℕ) → Term L' (β ⊕ Fin n) → Term L'' (γ ⊕ Fin n)
fr' : (n : ℕ) → Relations L' n → Relations L'' n
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 :
  mapTermRel ft' fr' (fun x => id) (mapTermRel ft fr (fun x => id) f✝) =
    mapTermRel (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) (all f✝)) =
    mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) (all f✝)
[PROOFSTEP]
simp [mapTermRel, ih3]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ n : ℕ
φ : BoundedFormula L α n
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) φ = φ
[PROOFSTEP]
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n n✝ : ℕ
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) falsum = falsum
[PROOFSTEP]
rfl
[GOAL]
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (equal t₁✝ t₂✝) = equal t₁✝ t₂✝
[PROOFSTEP]
simp [mapTermRel]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (rel R✝ ts✝) = rel R✝ ts✝
[PROOFSTEP]
simp [mapTermRel]
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : mapTermRel (fun x => id) (fun x => id) (fun x => id) f₁✝ = f₁✝
ih2 : mapTermRel (fun x => id) (fun x => id) (fun x => id) f₂✝ = f₂✝
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (imp f₁✝ f₂✝) = imp f₁✝ f₂✝
[PROOFSTEP]
simp [mapTermRel, ih1, ih2]
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝¹ n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : mapTermRel (fun x => id) (fun x => id) (fun x => id) f✝ = f✝
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (all f✝) = all f✝
[PROOFSTEP]
simp [mapTermRel, ih3]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
ft : (n : ℕ) → Term L (α ⊕ Fin n) ≃ Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n ≃ Relations L' n
n : ℕ
φ : BoundedFormula L α n
⊢ mapTermRel (fun n => ↑(ft n).symm) (fun n => ↑(fr n).symm) (fun x => id)
      (mapTermRel (fun n => ↑(ft n)) (fun n => ↑(fr n)) (fun x => id) φ) =
    φ
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n✝ : ℕ
ft : (n : ℕ) → Term L (α ⊕ Fin n) ≃ Term L' (β ⊕ Fin n)
fr : (n : ℕ) → Relations L n ≃ Relations L' n
n : ℕ
φ : BoundedFormula L' β n
⊢ mapTermRel (fun n => ↑(ft n)) (fun n => ↑(fr n)) (fun x => id)
      (mapTermRel (fun n => ↑(ft n).symm) (fun n => ↑(fr n).symm) (fun x => id) φ) =
    φ
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
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)
[PROOFSTEP]
ext x
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
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
[PROOFSTEP]
cases' x with x x
[GOAL]
case h.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
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)
[PROOFSTEP]
simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]
[GOAL]
case h.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ Sum.elim v xs (Sum.map id (↑finSumFinEquiv) (↑(Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)
[PROOFSTEP]
cases' g x with l r
[GOAL]
case h.inl.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
l : β
⊢ Sum.elim v xs (Sum.map id (↑finSumFinEquiv) (↑(Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (Sum.inl l)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inl l)
[PROOFSTEP]
simp
[GOAL]
case h.inl.inr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
r : Fin n
⊢ Sum.elim v xs (Sum.map id (↑finSumFinEquiv) (↑(Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (Sum.inr r)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inr r)
[PROOFSTEP]
simp
[GOAL]
case h.inr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
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)
[PROOFSTEP]
simp [BoundedFormula.relabelAux]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k : ℕ
⊢ relabelAux Sum.inl k = Sum.map id (natAdd n)
[PROOFSTEP]
ext x
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k : ℕ
x : α ⊕ Fin k
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k : ℕ
val✝ : α
⊢ relabelAux Sum.inl k (Sum.inl val✝) = Sum.map id (natAdd n) (Sum.inl val✝)
[PROOFSTEP]
simp [relabelAux]
[GOAL]
case h.inr
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)
[PROOFSTEP]
simp [relabelAux]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : BoundedFormula L α k
⊢ relabel g (BoundedFormula.not φ) = BoundedFormula.not (relabel g φ)
[PROOFSTEP]
simp [BoundedFormula.not]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : BoundedFormula L α (k + 1)
⊢ relabel g (all φ) = all (relabel g φ)
[PROOFSTEP]
rw [relabel, mapTermRel, relabel]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : BoundedFormula L α (k + 1)
⊢ all
      (castLE (_ : n + k + 1 ≥ n + (k + 1))
        (mapTermRel (fun x t => Term.relabel (relabelAux g x) t) (fun x => id)
          (fun x => castLE (_ : n + x + 1 ≥ n + (x + 1))) φ)) =
    all
      (mapTermRel (fun x t => Term.relabel (relabelAux g x) t) (fun x => id)
        (fun x => castLE (_ : n + x + 1 ≥ n + (x + 1))) φ)
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : BoundedFormula L α (k + 1)
⊢ relabel g (BoundedFormula.ex φ) = BoundedFormula.ex (relabel g φ)
[PROOFSTEP]
simp [BoundedFormula.ex]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
φ : BoundedFormula L α n
⊢ relabel Sum.inl φ = castLE (_ : 0 + n ≥ n) φ
[PROOFSTEP]
simp only [relabel, relabelAux_sum_inl]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
φ : BoundedFormula L α n
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) φ =
    castLE (_ : 0 + n ≥ n) φ
[PROOFSTEP]
induction' φ with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) falsum =
    castLE (_ : 0 + n✝ ≥ n✝) falsum
[PROOFSTEP]
rfl
[GOAL]
case equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (equal t₁✝ t₂✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (equal t₁✝ t₂✝)
[PROOFSTEP]
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (rel R✝ ts✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (rel R✝ ts✝)
[PROOFSTEP]
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
[GOAL]
case rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ (fun i => Term.relabel (Sum.map id (Fin.cast (_ : n✝ = 0 + n✝))) (ts✝ i)) =
    Term.relabel (Sum.map id (Fin.cast (_ : n✝ = 0 + n✝))) ∘ ts✝
[PROOFSTEP]
rfl
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f₁✝ =
    castLE (_ : 0 + n✝ ≥ n✝) f₁✝
ih2 :
  mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f₂✝ =
    castLE (_ : 0 + n✝ ≥ n✝) f₂✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (imp f₁✝ f₂✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (imp f₁✝ f₂✝)
[PROOFSTEP]
simp [mapTermRel, ih1, ih2]
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 :
  mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) f✝ =
    castLE (_ : 0 + (n✝ + 1) ≥ n✝ + 1) f✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id)
      (fun x => castLE (_ : 0 + x + 1 ≥ 0 + (x + 1))) (all f✝) =
    castLE (_ : 0 + n✝ ≥ n✝) (all f✝)
[PROOFSTEP]
simp [mapTermRel, ih3, castLE]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsAtomic (all φ)
⊢ False
[PROOFSTEP]
cases con
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsAtomic (BoundedFormula.ex φ)
⊢ False
[PROOFSTEP]
cases con
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsQF (all φ)
⊢ False
[PROOFSTEP]
cases' con with _ con
[GOAL]
case of_isAtomic
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsAtomic (all φ)
⊢ False
[PROOFSTEP]
exact φ.not_all_isAtomic con
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsQF (BoundedFormula.ex φ)
⊢ False
[PROOFSTEP]
cases' con with _ con _ _ con
[GOAL]
case of_isAtomic
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsAtomic (BoundedFormula.ex φ)
⊢ False
[PROOFSTEP]
exact φ.not_ex_isAtomic con
[GOAL]
case imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsQF (all (BoundedFormula.not φ))
h₂✝ : IsQF ⊥
⊢ False
[PROOFSTEP]
exact not_all_isQF _ con
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝¹ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
m : ℕ
φ : BoundedFormula L α m
h✝ : IsPrenex φ
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
x✝ : IsPrenex φ✝
h : IsPrenex (BoundedFormula.relabel f φ✝)
⊢ IsPrenex (BoundedFormula.relabel f (BoundedFormula.all φ✝))
[PROOFSTEP]
simp [h.all]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝¹ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
m : ℕ
φ : BoundedFormula L α m
h✝ : IsPrenex φ
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
x✝ : IsPrenex φ✝
h : IsPrenex (BoundedFormula.relabel f φ✝)
⊢ IsPrenex (BoundedFormula.relabel f (BoundedFormula.ex φ✝))
[PROOFSTEP]
simp [h.ex]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ : BoundedFormula L α n
hφ : IsQF φ
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImpRight φ ψ)
[PROOFSTEP]
induction' hψ with _ _ hψ _ _ _ ih1 _ _ _ ih2
[GOAL]
case of_isQF
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ φ✝)
[PROOFSTEP]
rw [hψ.toPrenexImpRight]
[GOAL]
case of_isQF
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (imp φ φ✝)
[PROOFSTEP]
exact (hφ.imp hψ).isPrenex
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih1 : ∀ {φ : BoundedFormula L α (n✝ + 1)}, IsQF φ → IsPrenex (toPrenexImpRight φ φ✝)
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ (all φ✝))
[PROOFSTEP]
exact (ih1 hφ.liftAt).all
[GOAL]
case ex
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih2 : ∀ {φ : BoundedFormula L α (n✝ + 1)}, IsQF φ → IsPrenex (toPrenexImpRight φ φ✝)
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ (BoundedFormula.ex φ✝))
[PROOFSTEP]
exact (ih2 hφ.liftAt).ex
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝ ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ : BoundedFormula L α n
hφ : IsPrenex φ
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp φ ψ)
[PROOFSTEP]
induction' hφ with _ _ hφ _ _ _ ih1 _ _ _ ih2
[GOAL]
case of_isQF
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp φ✝ ψ)
[PROOFSTEP]
rw [hφ.toPrenexImp]
[GOAL]
case of_isQF
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImpRight φ✝ ψ)
[PROOFSTEP]
exact isPrenex_toPrenexImpRight hφ hψ
[GOAL]
case all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih1 : ∀ {ψ : BoundedFormula L α (n✝ + 1)}, IsPrenex ψ → IsPrenex (toPrenexImp φ✝ ψ)
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp (all φ✝) ψ)
[PROOFSTEP]
exact (ih1 hψ.liftAt).ex
[GOAL]
case ex
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih2 : ∀ {ψ : BoundedFormula L α (n✝ + 1)}, IsPrenex ψ → IsPrenex (toPrenexImp φ✝ ψ)
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp (BoundedFormula.ex φ✝) ψ)
[PROOFSTEP]
exact (ih2 hψ.liftAt).all
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
⊢ onBoundedFormula (LHom.id L) = id
[PROOFSTEP]
ext f
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
f : BoundedFormula L α n
⊢ onBoundedFormula (LHom.id L) f = id f
[PROOFSTEP]
induction' f with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case h.falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
⊢ onBoundedFormula (LHom.id L) falsum = id falsum
[PROOFSTEP]
rfl
[GOAL]
case h.equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (LHom.id L) (equal t₁✝ t₂✝) = id (equal t₁✝ t₂✝)
[PROOFSTEP]
rw [onBoundedFormula, LHom.id_onTerm, id.def, id.def, id.def, Term.bdEqual]
[GOAL]
case h.rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (LHom.id L) (rel R✝ ts✝) = id (rel R✝ ts✝)
[PROOFSTEP]
rw [onBoundedFormula, LHom.id_onTerm]
[GOAL]
case h.rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ Relations.boundedFormula (onRelation (LHom.id L) R✝) (id ∘ ts✝) = id (rel R✝ ts✝)
[PROOFSTEP]
rfl
[GOAL]
case h.imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : onBoundedFormula (LHom.id L) f₁✝ = id f₁✝
ih2 : onBoundedFormula (LHom.id L) f₂✝ = id f₂✝
⊢ onBoundedFormula (LHom.id L) (imp f₁✝ f₂✝) = id (imp f₁✝ f₂✝)
[PROOFSTEP]
rw [onBoundedFormula, ih1, ih2, id.def, id.def, id.def]
[GOAL]
case h.all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : onBoundedFormula (LHom.id L) f✝ = id f✝
⊢ onBoundedFormula (LHom.id L) (all f✝) = id (all f✝)
[PROOFSTEP]
rw [onBoundedFormula, ih3, id.def, id.def]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ onBoundedFormula (comp φ ψ) = onBoundedFormula φ ∘ onBoundedFormula ψ
[PROOFSTEP]
ext f
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : BoundedFormula L α n
⊢ onBoundedFormula (comp φ ψ) f = (onBoundedFormula φ ∘ onBoundedFormula ψ) f
[PROOFSTEP]
induction' f with _ _ _ _ _ _ _ _ _ _ _ ih1 ih2 _ _ ih3
[GOAL]
case h.falsum
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
⊢ onBoundedFormula (comp φ ψ) falsum = (onBoundedFormula φ ∘ onBoundedFormula ψ) falsum
[PROOFSTEP]
rfl
[GOAL]
case h.equal
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (comp φ ψ) (equal t₁✝ t₂✝) = (onBoundedFormula φ ∘ onBoundedFormula ψ) (equal t₁✝ t₂✝)
[PROOFSTEP]
simp only [onBoundedFormula, comp_onTerm, Function.comp_apply]
[GOAL]
case h.rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ onBoundedFormula (comp φ ψ) (rel R✝ ts✝) = (onBoundedFormula φ ∘ onBoundedFormula ψ) (rel R✝ ts✝)
[PROOFSTEP]
simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]
[GOAL]
case h.rel
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (α ⊕ Fin n✝)
⊢ Relations.boundedFormula (onRelation φ (onRelation ψ R✝)) ((onTerm φ ∘ onTerm ψ) ∘ ts✝) =
    Relations.boundedFormula (onRelation φ (onRelation ψ R✝)) (onTerm φ ∘ onTerm ψ ∘ ts✝)
[PROOFSTEP]
rfl
[GOAL]
case h.imp
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 : onBoundedFormula (comp φ ψ) f₁✝ = (onBoundedFormula φ ∘ onBoundedFormula ψ) f₁✝
ih2 : onBoundedFormula (comp φ ψ) f₂✝ = (onBoundedFormula φ ∘ onBoundedFormula ψ) f₂✝
⊢ onBoundedFormula (comp φ ψ) (imp f₁✝ f₂✝) = (onBoundedFormula φ ∘ onBoundedFormula ψ) (imp f₁✝ f₂✝)
[PROOFSTEP]
simp only [onBoundedFormula, Function.comp_apply, ih1, ih2, eq_self_iff_true, and_self_iff]
[GOAL]
case h.all
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih3 : onBoundedFormula (comp φ ψ) f✝ = (onBoundedFormula φ ∘ onBoundedFormula ψ) f✝
⊢ onBoundedFormula (comp φ ψ) (all f✝) = (onBoundedFormula φ ∘ onBoundedFormula ψ) (all f✝)
[PROOFSTEP]
simp only [ih3, onBoundedFormula, Function.comp_apply]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.LeftInverse (LHom.onBoundedFormula φ.invLHom) (LHom.onBoundedFormula φ.toLHom)
[PROOFSTEP]
rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv, LHom.id_onBoundedFormula]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.RightInverse (LHom.onBoundedFormula φ.invLHom) (LHom.onBoundedFormula φ.toLHom)
[PROOFSTEP]
rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv, LHom.id_onBoundedFormula]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
⊢ distinctConstantsTheory L s =
    ⋃ (t : Finset ↑s), distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)
[PROOFSTEP]
classical
simp only [distinctConstantsTheory]
rw [← image_iUnion, ← iUnion_inter]
refine' congr rfl (congr (congr rfl _) rfl)
ext ⟨i, j⟩
simp only [prod_mk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion, mem_image,
  Finset.mem_coe, Subtype.exists, Subtype.coe_mk, exists_and_right, exists_eq_right]
refine' ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, _⟩, ⟨h.2, _⟩⟩, _⟩
· simp
· simp
· rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
  exact ⟨is, js⟩
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
⊢ distinctConstantsTheory L s =
    ⋃ (t : Finset ↑s), distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)
[PROOFSTEP]
simp only [distinctConstantsTheory]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
⊢ (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      (s ×ˢ s ∩ (diagonal α)ᶜ) =
    ⋃ (t : Finset ↑s),
      (fun ab =>
          Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
        (↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ∩
          (diagonal α)ᶜ)
[PROOFSTEP]
rw [← image_iUnion, ← iUnion_inter]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
⊢ (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      ((⋃ (i : Finset ↑s),
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)) ∩
        (diagonal α)ᶜ)
[PROOFSTEP]
refine' congr rfl (congr (congr rfl _) rfl)
[GOAL]
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
⊢ s ×ˢ s =
    ⋃ (i : Finset ↑s),
      ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case h.mk
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    (i, j) ∈
      ⋃ (i : Finset ↑s),
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
simp only [prod_mk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion, mem_image,
  Finset.mem_coe, Subtype.exists, Subtype.coe_mk, exists_and_right, exists_eq_right]
[GOAL]
case h.mk
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ i_1, (∃ x, { val := i, property := (_ : i ∈ s) } ∈ i_1) ∧ ∃ x, { val := j, property := (_ : j ∈ s) } ∈ i_1
[PROOFSTEP]
refine' ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, _⟩, ⟨h.2, _⟩⟩, _⟩
[GOAL]
case h.mk.refine'_1
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ { val := i, property := (_ : i ∈ s) } ∈ {{ val := i, property := (_ : i ∈ s) }, { val := j, property := (_ : j ∈ s) }}
[PROOFSTEP]
simp
[GOAL]
case h.mk.refine'_2
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ { val := j, property := (_ : j ∈ s) } ∈ {{ val := i, property := (_ : i ∈ s) }, { val := j, property := (_ : j ∈ s) }}
[PROOFSTEP]
simp
[GOAL]
case h.mk.refine'_3
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
i j : α
⊢ (∃ i_1, (∃ x, { val := i, property := (_ : i ∈ s) } ∈ i_1) ∧ ∃ x, { val := j, property := (_ : j ∈ s) } ∈ i_1) →
    i ∈ s ∧ j ∈ s
[PROOFSTEP]
rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
[GOAL]
case h.mk.refine'_3.intro.intro.intro.intro
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
s : Set α
i j : α
t : Finset ↑s
is : i ∈ s
h✝¹ : { val := i, property := (_ : i ∈ s) } ∈ t
js : j ∈ s
h✝ : { val := j, property := (_ : j ∈ s) } ∈ t
⊢ i ∈ s ∧ j ∈ s
[PROOFSTEP]
exact ⟨is, js⟩
