Theorem: IsLinearMap.smul_push₂ (SciLean/Core/Meta/GenerateLinearMapSimp.lean)

State before:
K : Type u'
inst✝⁶ : CommSemiring K
X : Type u
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module K X
Y : Type v
inst✝³ : AddCommGroup Y
inst✝² : Module K Y
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module K Z
f : X → Y
hf : IsLinearMap K f
g : X → Y → Z
hg : IsLinearMap K fun xy => g xy.1 xy.2
x : X
y : Y
k : K
⊢ k • g x y = g (k • x) (k • y)
Tactic:
have h := hg.map_smul k (x,y)
State after:
K : Type u'
inst✝⁶ : CommSemiring K
X : Type u
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module K X
Y : Type v
inst✝³ : AddCommGroup Y
inst✝² : Module K Y
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module K Z
f : X → Y
hf : IsLinearMap K f
g : X → Y → Z
hg : IsLinearMap K fun xy => g xy.1 xy.2
x : X
y : Y
k : K
h : g (k • (x, y)).1 (k • (x, y)).2 = k • g (x, y).1 (x, y).2
⊢ k • g x y = g (k • x) (k • y)

State before:
K : Type u'
inst✝⁶ : CommSemiring K
X : Type u
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module K X
Y : Type v
inst✝³ : AddCommGroup Y
inst✝² : Module K Y
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module K Z
f : X → Y
hf : IsLinearMap K f
g : X → Y → Z
hg : IsLinearMap K fun xy => g xy.1 xy.2
x : X
y : Y
k : K
h : g (k • (x, y)).1 (k • (x, y)).2 = k • g (x, y).1 (x, y).2
⊢ k • g x y = g (k • x) (k • y)
Tactic:
simp at h
State after:
K : Type u'
inst✝⁶ : CommSemiring K
X : Type u
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module K X
Y : Type v
inst✝³ : AddCommGroup Y
inst✝² : Module K Y
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module K Z
f : X → Y
hf : IsLinearMap K f
g : X → Y → Z
hg : IsLinearMap K fun xy => g xy.1 xy.2
x : X
y : Y
k : K
h : g (k • x) (k • y) = k • g x y
⊢ k • g x y = g (k • x) (k • y)

State before:
K : Type u'
inst✝⁶ : CommSemiring K
X : Type u
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module K X
Y : Type v
inst✝³ : AddCommGroup Y
inst✝² : Module K Y
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module K Z
f : X → Y
hf : IsLinearMap K f
g : X → Y → Z
hg : IsLinearMap K fun xy => g xy.1 xy.2
x : X
y : Y
k : K
h : g (k • x) (k • y) = k • g x y
⊢ k • g x y = g (k • x) (k • y)
Tactic:
rw[h]
State after:
no goals