case var
L : Language
L' : Language
M : Type w
N : Type ?u.25879
P : Type ?u.25882
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
v : α → M
_a✝ : α
⊢ Term.realize v (onTerm φ (var _a✝)) = Term.realize v (var _a✝)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.25879
P : Type ?u.25882
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
v : α → M
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih : ∀ (a : Fin n), Term.realize v (onTerm φ (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (onTerm φ (func f ts)) = Term.realize v (func f ts)
L : Language
L' : Language
M : Type w
N : Type ?u.25879
P : Type ?u.25882
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
t : Term L α
v : α → M
⊢ Term.realize v (onTerm φ t) = Term.realize v t
induction' t with _ n f ts ih
no goals
case var
L : Language
L' : Language
M : Type w
N : Type ?u.25879
P : Type ?u.25882
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
v : α → M
_a✝ : α
⊢ Term.realize v (onTerm φ (var _a✝)) = Term.realize v (var _a✝)
rfl
no goals
case func
L : Language
L' : Language
M : Type w
N : Type ?u.25879
P : Type ?u.25882
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
v : α → M
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih : ∀ (a : Fin n), Term.realize v (onTerm φ (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (onTerm φ (func f ts)) = Term.realize v (func f ts)
simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]