case var
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
_a✝ : β
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (var _a✝)) = realize v (var _a✝)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n : ℕ
f : Functions (L[[α]]) n
ts : Fin n → Term (L[[α]]) β
ih : ∀ (a : Fin n), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func f ts)) = realize v (func f ts)
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
t : Term (L[[α]]) β
v : β → M
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars t) = realize v t
induction' t with _ n f ts ih
no goals
case var
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
_a✝ : β
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (var _a✝)) = realize v (var _a✝)
simp
case func.zero
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
f : Functions (L[[α]]) Nat.zero
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func f ts)) = realize v (func f ts)

case func.succ
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
f : Functions (L[[α]]) (Nat.succ n✝)
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func f ts)) = realize v (func f ts)
case func
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n : ℕ
f : Functions (L[[α]]) n
ts : Fin n → Term (L[[α]]) β
ih : ∀ (a : Fin n), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func f ts)) = realize v (func f ts)
cases n
case func.zero.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L Nat.zero
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inl val✝) ts)) =
    realize v (func (Sum.inl val✝) ts)

case func.zero.inr
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions (constantsOn α) Nat.zero
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inr val✝) ts)) =
    realize v (func (Sum.inr val✝) ts)
case func.zero
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
f : Functions (L[[α]]) Nat.zero
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func f ts)) = realize v (func f ts)
cases f
case func.zero.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L Nat.zero
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)
case func.zero.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L Nat.zero
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inl val✝) ts)) =
    realize v (func (Sum.inl val✝) ts)
simp only [realize, ih, Nat.zero_eq, constantsOn, mk₂_Functions]
no goals
case func.zero.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L Nat.zero
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)
rw [withConstants_funMap_sum_inl]
case func.zero.inr
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions (constantsOn α) Nat.zero
⊢ ↑(Language.con L val✝) = ↑(Sum.inr val✝)
case func.zero.inr
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions (constantsOn α) Nat.zero
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inr val✝) ts)) =
    realize v (func (Sum.inr val✝) ts)
simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
no goals
case func.zero.inr
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
ts : Fin Nat.zero → Term (L[[α]]) β
ih :
  ∀ (a : Fin Nat.zero), realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions (constantsOn α) Nat.zero
⊢ ↑(Language.con L val✝) = ↑(Sum.inr val✝)
rfl
case func.succ.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L (Nat.succ n✝)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inl val✝) ts)) =
    realize v (func (Sum.inl val✝) ts)

case func.succ.inr
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
f : Functions (constantsOn α) (Nat.succ n✝)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inr f) ts)) =
    realize v (func (Sum.inr f) ts)
case func.succ
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
f : Functions (L[[α]]) (Nat.succ n✝)
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func f ts)) = realize v (func f ts)
cases' f with _ f
case func.succ.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L (Nat.succ n✝)
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)
case func.succ.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L (Nat.succ n✝)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inl val✝) ts)) =
    realize v (func (Sum.inl val✝) ts)
simp only [realize, ih, constantsOn, mk₂_Functions]
no goals
case func.succ.inl
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
val✝ : Functions L (Nat.succ n✝)
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)
rw [withConstants_funMap_sum_inl]
no goals
case func.succ.inr
L : Language
L' : Language
M : Type w
N : Type ?u.15741
P : Type ?u.15744
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
v : β → M
n✝ : ℕ
ts : Fin (Nat.succ n✝) → Term (L[[α]]) β
ih :
  ∀ (a : Fin (Nat.succ n✝)),
    realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (ts a)) = realize v (ts a)
f : Functions (constantsOn α) (Nat.succ n✝)
⊢ realize (Sum.elim (fun a => ↑(Language.con L a)) v) (constantsToVars (func (Sum.inr f) ts)) =
    realize v (func (Sum.inr f) ts)
exact isEmptyElim f