internlm/Lean-Github huggingface dataset:
Theorem: SciLean.cintegral.arg_f.parDistribDeriv_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝¹² : RealScalar R
W : Type u_2
inst✝¹¹ : Vec R W
X : Type u_3
inst✝¹⁰ : Vec R X
inst✝⁹ : MeasureSpace X
Y : Type u_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), ∫' x, φ x • ∫' y, f x' x y =
    ⟪∂ (x':=w;dw), ∫' x, φ x • fun φ ⊸[R] ∫' x_1, φ x_1 • f x' x x_1, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsLinearMap.add_push
Proof 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
x x' : X
⊢ f x + f x' = f (x + x')
Tactic:
rw[hf.map_add]
Proof state after:
no goals
Theorem: IsLinearMap.add_pull
Proof 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
x x' : X
⊢ f (x + x') = f x + f x'
Tactic:
rw[hf.map_add]
Proof state after:
no goals
Theorem: IsLinearMap.sum_push
Proof 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✝
f : X → Y
hf : IsLinearMap K f
ι : Type
inst✝¹ : IndexType ι
inst✝ : IndexType ι
x : ι → X
⊢  ∑ i, f (x i) = f ( ∑ i, x i)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsLinearMap.sum_pull
Proof 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✝
f : X → Y
hf : IsLinearMap K f
ι : Type
inst✝¹ : IndexType ι
inst✝ : IndexType ι
x : ι → X
⊢ f ( ∑ i, x i) = ∑ i, f (x i)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsLinearMap.sub_push
Proof 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
x x' : X
⊢ f x - f x' = f (x - x')
Tactic:
rw[hf.map_sub]
Proof state after:
no goals
Theorem: IsLinearMap.sub_pull
Proof 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
x x' : X
⊢ f (x - x') = f x - f x'
Tactic:
rw[hf.map_sub]
Proof state after:
no goals
Theorem: IsLinearMap.smul_push
Proof 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
x : X
k : K
⊢ k • f x = f (k • x)
Tactic:
rw[hf.map_smul]
Proof state after:
no goals
Theorem: IsLinearMap.smul_pull
Proof 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
x : X
k : K
⊢ f (k • x) = k • f x
Tactic:
rw[hf.map_smul]
Proof state after:
no goals
Theorem: IsLinearMap.neg_push
Proof 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
x : X
⊢ -f x = f (-x)
Tactic:
rw[hf.map_neg]
Proof state after:
no goals
Theorem: IsLinearMap.neg_pull
Proof 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
x : X
⊢ f (-x) = -f x
Tactic:
rw[hf.map_neg]
Proof state after:
no goals
Theorem: IsLinearMap.app_zero
Proof 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
⊢ f 0 = 0
Tactic:
rw[hf.map_zero]
Proof state after:
no goals
Theorem: IsLinearMap.add_push₂
Proof 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' : X
y y' : Y
⊢ g x y + g x' y' = g (x + x') (y + y')
Tactic:
have h := hg.map_add (x,y) (x',y')
Proof 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' : X
y y' : Y
h : g ((x, y) + (x', y')).1 ((x, y) + (x', y')).2 = g (x, y).1 (x, y).2 + g (x', y').1 (x', y').2
⊢ g x y + g x' y' = g (x + x') (y + y')
Theorem: IsLinearMap.add_push₂
Proof 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' : X
y y' : Y
h : g ((x, y) + (x', y')).1 ((x, y) + (x', y')).2 = g (x, y).1 (x, y).2 + g (x', y').1 (x', y').2
⊢ g x y + g x' y' = g (x + x') (y + y')
Tactic:
simp at h
Proof 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' : X
y y' : Y
h : g (x + x') (y + y') = g x y + g x' y'
⊢ g x y + g x' y' = g (x + x') (y + y')
Theorem: IsLinearMap.add_push₂
Proof 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' : X
y y' : Y
h : g (x + x') (y + y') = g x y + g x' y'
⊢ g x y + g x' y' = g (x + x') (y + y')
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.add_pull₂
Proof 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' : X
y y' : Y
⊢ g (x + x') (y + y') = g x y + g x' y'
Tactic:
have h := hg.map_add (x,y) (x',y')
Proof 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' : X
y y' : Y
h : g ((x, y) + (x', y')).1 ((x, y) + (x', y')).2 = g (x, y).1 (x, y).2 + g (x', y').1 (x', y').2
⊢ g (x + x') (y + y') = g x y + g x' y'
Theorem: IsLinearMap.add_pull₂
Proof 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' : X
y y' : Y
h : g ((x, y) + (x', y')).1 ((x, y) + (x', y')).2 = g (x, y).1 (x, y).2 + g (x', y').1 (x', y').2
⊢ g (x + x') (y + y') = g x y + g x' y'
Tactic:
simp at h
Proof 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' : X
y y' : Y
h : g (x + x') (y + y') = g x y + g x' y'
⊢ g (x + x') (y + y') = g x y + g x' y'
Theorem: IsLinearMap.add_pull₂
Proof 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' : X
y y' : Y
h : g (x + x') (y + y') = g x y + g x' y'
⊢ g (x + x') (y + y') = g x y + g x' y'
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.sub_push₂
Proof 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' : X
y y' : Y
⊢ g x y - g x' y' = g (x - x') (y - y')
Tactic:
have h := hg.map_sub (x,y) (x',y')
Proof 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' : X
y y' : Y
h : g ((x, y) - (x', y')).1 ((x, y) - (x', y')).2 = g (x, y).1 (x, y).2 - g (x', y').1 (x', y').2
⊢ g x y - g x' y' = g (x - x') (y - y')
Theorem: IsLinearMap.sub_push₂
Proof 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' : X
y y' : Y
h : g ((x, y) - (x', y')).1 ((x, y) - (x', y')).2 = g (x, y).1 (x, y).2 - g (x', y').1 (x', y').2
⊢ g x y - g x' y' = g (x - x') (y - y')
Tactic:
simp at h
Proof 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' : X
y y' : Y
h : g (x - x') (y - y') = g x y - g x' y'
⊢ g x y - g x' y' = g (x - x') (y - y')
Theorem: IsLinearMap.sub_push₂
Proof 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' : X
y y' : Y
h : g (x - x') (y - y') = g x y - g x' y'
⊢ g x y - g x' y' = g (x - x') (y - y')
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.sub_pull₂
Proof 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' : X
y y' : Y
⊢ g (x - x') (y - y') = g x y - g x' y'
Tactic:
have h := hg.map_sub (x,y) (x',y')
Proof 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' : X
y y' : Y
h : g ((x, y) - (x', y')).1 ((x, y) - (x', y')).2 = g (x, y).1 (x, y).2 - g (x', y').1 (x', y').2
⊢ g (x - x') (y - y') = g x y - g x' y'
Theorem: IsLinearMap.sub_pull₂
Proof 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' : X
y y' : Y
h : g ((x, y) - (x', y')).1 ((x, y) - (x', y')).2 = g (x, y).1 (x, y).2 - g (x', y').1 (x', y').2
⊢ g (x - x') (y - y') = g x y - g x' y'
Tactic:
simp at h
Proof 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' : X
y y' : Y
h : g (x - x') (y - y') = g x y - g x' y'
⊢ g (x - x') (y - y') = g x y - g x' y'
Theorem: IsLinearMap.sub_pull₂
Proof 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' : X
y y' : Y
h : g (x - x') (y - y') = g x y - g x' y'
⊢ g (x - x') (y - y') = g x y - g x' y'
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.smul_push₂
Proof 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)
Proof 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)
Theorem: IsLinearMap.smul_push₂
Proof 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
Proof 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)
Theorem: IsLinearMap.smul_push₂
Proof 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]
Proof state after:
no goals
Theorem: IsLinearMap.smul_pull₂
Proof 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
⊢ g (k • x) (k • y) = k • g x y
Tactic:
have h := hg.map_smul k (x,y)
Proof 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
⊢ g (k • x) (k • y) = k • g x y
Theorem: IsLinearMap.smul_pull₂
Proof 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
⊢ g (k • x) (k • y) = k • g x y
Tactic:
simp at h
Proof 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
⊢ g (k • x) (k • y) = k • g x y
Theorem: IsLinearMap.smul_pull₂
Proof 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
⊢ g (k • x) (k • y) = k • g x y
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.neg_push₂
Proof 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
⊢ -g x y = g (-x) (-y)
Tactic:
have h := hg.map_neg (x,y)
Proof 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
h : g (-(x, y)).1 (-(x, y)).2 = -g (x, y).1 (x, y).2
⊢ -g x y = g (-x) (-y)
Theorem: IsLinearMap.neg_push₂
Proof 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
h : g (-(x, y)).1 (-(x, y)).2 = -g (x, y).1 (x, y).2
⊢ -g x y = g (-x) (-y)
Tactic:
simp at h
Proof 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
h : g (-x) (-y) = -g x y
⊢ -g x y = g (-x) (-y)
Theorem: IsLinearMap.neg_push₂
Proof 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
h : g (-x) (-y) = -g x y
⊢ -g x y = g (-x) (-y)
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.neg_pull₂
Proof 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
⊢ g (-x) (-y) = -g x y
Tactic:
have h := hg.map_neg (x,y)
Proof 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
h : g (-(x, y)).1 (-(x, y)).2 = -g (x, y).1 (x, y).2
⊢ g (-x) (-y) = -g x y
Theorem: IsLinearMap.neg_pull₂
Proof 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
h : g (-(x, y)).1 (-(x, y)).2 = -g (x, y).1 (x, y).2
⊢ g (-x) (-y) = -g x y
Tactic:
simp at h
Proof 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
h : g (-x) (-y) = -g x y
⊢ g (-x) (-y) = -g x y
Theorem: IsLinearMap.neg_pull₂
Proof 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
h : g (-x) (-y) = -g x y
⊢ g (-x) (-y) = -g x y
Tactic:
rw[h]
Proof state after:
no goals
Theorem: IsLinearMap.app_zero₂
Proof 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
⊢ g 0 0 = 0
Tactic:
have h := hg.map_zero
Proof 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
h : g 0.1 0.2 = 0
⊢ g 0 0 = 0
Theorem: IsLinearMap.app_zero₂
Proof 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
h : g 0.1 0.2 = 0
⊢ g 0 0 = 0
Tactic:
simp at h
Proof 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
h : g 0 0 = 0
⊢ g 0 0 = 0
Theorem: IsLinearMap.app_zero₂
Proof 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
h : g 0 0 = 0
⊢ g 0 0 = 0
Tactic:
rw[h]
Proof state after:
no goals
Theorem: Float3.x.as_struct_proj
Proof state before:
⊢ x = fun v => structProj v (Sum.inl ())
Tactic:
rfl
Proof state after:
no goals