case var
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h✝ : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
a : α ⊕ γ
h : ↑(varFinsetLeft (var a)) ⊆ s
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (var a) (Set.inclusion h)) = realize (Sum.elim v xs) (var a)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h✝ : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinsetLeft (_ts✝ a)) ⊆ s),
    realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (_ts✝ a) (Set.inclusion h)) =
      realize (Sum.elim v xs) (_ts✝ a)
h : ↑(varFinsetLeft (func _f✝ _ts✝)) ⊆ s
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (func _f✝ _ts✝) (Set.inclusion h)) =
    realize (Sum.elim v xs) (func _f✝ _ts✝)
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft t (Set.inclusion h)) = realize (Sum.elim v xs) t
induction' t with a _ _ _ ih
no goals
case var
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h✝ : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
a : α ⊕ γ
h : ↑(varFinsetLeft (var a)) ⊆ s
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (var a) (Set.inclusion h)) = realize (Sum.elim v xs) (var a)
cases a <;> rfl
case func
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h✝¹ : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinsetLeft (_ts✝ a)) ⊆ s),
    realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (_ts✝ a) (Set.inclusion h)) =
      realize (Sum.elim v xs) (_ts✝ a)
h✝ : ↑(Finset.biUnion Finset.univ fun i => varFinsetLeft (_ts✝ i)) ⊆ s
h : ∀ (i : Fin l✝), i ∈ ↑Finset.univ → ↑(varFinsetLeft (_ts✝ i)) ⊆ s
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (func _f✝ _ts✝) (Set.inclusion h✝)) =
    realize (Sum.elim v xs) (func _f✝ _ts✝)
case func
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h✝ : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinsetLeft (_ts✝ a)) ⊆ s),
    realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (_ts✝ a) (Set.inclusion h)) =
      realize (Sum.elim v xs) (_ts✝ a)
h : ↑(varFinsetLeft (func _f✝ _ts✝)) ⊆ s
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (func _f✝ _ts✝) (Set.inclusion h)) =
    realize (Sum.elim v xs) (func _f✝ _ts✝)
simp_rw [varFinsetLeft, Finset.coe_biUnion, Set.iUnion_subset_iff] at h
no goals
case func
L : Language
L' : Language
M : Type w
N : Type ?u.12423
P : Type ?u.12426
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_1
t : Term L (α ⊕ γ)
s : Set α
h✝¹ : ↑(varFinsetLeft t) ⊆ s
v : α → M
xs : γ → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) (h : ↑(varFinsetLeft (_ts✝ a)) ⊆ s),
    realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (_ts✝ a) (Set.inclusion h)) =
      realize (Sum.elim v xs) (_ts✝ a)
h✝ : ↑(Finset.biUnion Finset.univ fun i => varFinsetLeft (_ts✝ i)) ⊆ s
h : ∀ (i : Fin l✝), i ∈ ↑Finset.univ → ↑(varFinsetLeft (_ts✝ i)) ⊆ s
⊢ realize (Sum.elim (v ∘ Subtype.val) xs) (restrictVarLeft (func _f✝ _ts✝) (Set.inclusion h✝)) =
    realize (Sum.elim v xs) (func _f✝ _ts✝)
exact congr rfl (funext fun i => ih i (h i (Finset.mem_univ i)))