case var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
_a✝ : α
⊢ Term.realize (↑g ∘ v) (var _a✝) = ↑g (Term.realize v (var _a✝))

case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
⊢ Term.realize (↑g ∘ v) (func _f✝ _ts✝) = ↑g (Term.realize v (func _f✝ _ts✝))
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
t : Term L α
v : α → M
⊢ Term.realize (↑g ∘ v) t = ↑g (Term.realize v t)
induction t
no goals
case var
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
_a✝ : α
⊢ Term.realize (↑g ∘ v) (var _a✝) = ↑g (Term.realize v (var _a✝))
rfl
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i => Term.realize (↑g ∘ v) (_ts✝ i)) = funMap _f✝ (↑g ∘ fun i => Term.realize v (_ts✝ i))
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
⊢ Term.realize (↑g ∘ v) (func _f✝ _ts✝) = ↑g (Term.realize v (func _f✝ _ts✝))
rw [Term.realize, Term.realize, g.map_fun]
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
⊢ (fun i => Term.realize (↑g ∘ v) (_ts✝ i)) = ↑g ∘ fun i => Term.realize v (_ts✝ i)
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i => Term.realize (↑g ∘ v) (_ts✝ i)) = funMap _f✝ (↑g ∘ fun i => Term.realize v (_ts✝ i))
refine' congr rfl _
case func.h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
x : Fin l✝
⊢ Term.realize (↑g ∘ v) (_ts✝ x) = (↑g ∘ fun i => Term.realize v (_ts✝ i)) x
case func
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
⊢ (fun i => Term.realize (↑g ∘ v) (_ts✝ i)) = ↑g ∘ fun i => Term.realize v (_ts✝ i)
ext x
no goals
case func.h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.26756
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
g : M →[L] N
v : α → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (↑g ∘ v) (_ts✝ a) = ↑g (Term.realize v (_ts✝ a))
x : Fin l✝
⊢ Term.realize (↑g ∘ v) (_ts✝ x) = (↑g ∘ fun i => Term.realize v (_ts✝ i)) x
simp [*]