case h
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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))
ext x
case h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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)

case h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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)
case h
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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
cases' x with x x
case h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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)
case h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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)
simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]
no goals
case h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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)
cases' g x with l r <;> simp
no goals
case h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.79266
P : Type ?u.79269
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.79297
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)
simp [BoundedFormula.relabelAux]