internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prod.mk.arg_fstsnd.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_2 u_3)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_2 u_3)
inst✝ : FinVec IZ K Z
g : X → Y
f : X → Z
⊢ (toMatrix K fun x => (g x, f x)) = fun i jx =>
    match i with
    | Sum.inl iy => ℼ iy (g ⅇ jx)
    | Sum.inr iz => ℼ iz (f ⅇ jx)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (toMatrix K fun x => (f x).1) = fun iy ix => toMatrix K f (Sum.inl iy) ix
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => (f x).1) ⅇ j)) = fun iy ix => ℼ(Sum.inl iy) (f ⅇ ix)
Theorem: SciLean.Prod.fst.arg_self.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => (f x).1) ⅇ j)) = fun iy ix => ℼ(Sum.inl iy) (f ⅇ ix)
Tactic:
simp[Basis.basis,Basis.proj]
Proof state after:
no goals
Theorem: SciLean.Prod.snd.arg_self.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (toMatrix K fun x => (f x).2) = fun iz ix => toMatrix K f (Sum.inr iz) ix
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => (f x).2) ⅇ j)) = fun iz ix => ℼ(Sum.inr iz) (f ⅇ ix)
Theorem: SciLean.Prod.snd.arg_self.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_3
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_1 u_2)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_1 u_2)
inst✝ : FinVec IZ K Z
f : X → Y × Z
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => (f x).2) ⅇ j)) = fun iz ix => ℼ(Sum.inr iz) (f ⅇ ix)
Tactic:
simp[Basis.basis,Basis.proj]
Proof state after:
no goals
Theorem: SciLean.HAdd.hAdd.arg_a0a1.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.36134
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (toMatrix K fun x => f x + g x) = fun i j => toMatrix K f i j + toMatrix K g i j
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.36134
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f x + g x) ⅇ j)) = fun i j => ℼ i (f ⅇ j) + ℼ i (g ⅇ j)
Theorem: SciLean.HAdd.hAdd.arg_a0a1.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.36134
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f x + g x) ⅇ j)) = fun i j => ℼ i (f ⅇ j) + ℼ i (g ⅇ j)
Tactic:
simp[(Basis.proj.arg_x.IsLinearMap_rule _).map_add]
Proof state after:
no goals
Theorem: SciLean.HSub.hSub.arg_a0a1.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.47833
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (toMatrix K fun x => f x - g x) = fun i j => toMatrix K f i j - toMatrix K g i j
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.47833
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f x - g x) ⅇ j)) = fun i j => ℼ i (f ⅇ j) - ℼ i (g ⅇ j)
Theorem: SciLean.HSub.hSub.arg_a0a1.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.47833
inst✝ : FinVec IZ K Z
f g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f x - g x) ⅇ j)) = fun i j => ℼ i (f ⅇ j) - ℼ i (g ⅇ j)
Tactic:
simp[(Basis.proj.arg_x.IsLinearMap_rule _).map_sub]
Proof state after:
no goals
Theorem: SciLean.Neg.neg.arg_a0.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.61817
inst✝ : FinVec IZ K Z
f : X → Y
hf : IsLinearMap K f
⊢ (toMatrix K fun x => -f x) = fun i j => -toMatrix K f i j
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.61817
inst✝ : FinVec IZ K Z
f : X → Y
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => -f x) ⅇ j)) = fun i j => -ℼ i (f ⅇ j)
Theorem: SciLean.Neg.neg.arg_a0.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.61817
inst✝ : FinVec IZ K Z
f : X → Y
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => -f x) ⅇ j)) = fun i j => -ℼ i (f ⅇ j)
Tactic:
simp[(Basis.proj.arg_x.IsLinearMap_rule _).map_neg]
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a1.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.72585
inst✝ : FinVec IZ K Z
k : K
f : X → Y
hf : IsLinearMap K f
⊢ (toMatrix K fun x => k • f x) = fun i j => k * toMatrix K f i j
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.72585
inst✝ : FinVec IZ K Z
k : K
f : X → Y
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => k • f x) ⅇ j)) = fun i j => k * ℼ i (f ⅇ j)
Theorem: SciLean.HSMul.hSMul.arg_a1.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.72585
inst✝ : FinVec IZ K Z
k : K
f : X → Y
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => k • f x) ⅇ j)) = fun i j => k * ℼ i (f ⅇ j)
Tactic:
simp[(Basis.proj.arg_x.IsLinearMap_rule _).map_smul]
Proof state after:
no goals
Theorem: SciLean.HSMul.hSMul.arg_a0.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.83634
inst✝ : FinVec IZ K Z
f : X → K
y : Y
hf : IsLinearMap K f
⊢ (toMatrix K fun x => f x • y) = fun i j => f ⅇ j * ℼ i y
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.83634
inst✝ : FinVec IZ K Z
f : X → K
y : Y
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => f x • y) ⅇ j)) = fun i j => f ⅇ j * ℼ i y
Theorem: SciLean.HSMul.hSMul.arg_a0.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.83634
inst✝ : FinVec IZ K Z
f : X → K
y : Y
hf : IsLinearMap K f
⊢ (fun i j => ℼ i ((fun x => f x • y) ⅇ j)) = fun i j => f ⅇ j * ℼ i y
Tactic:
simp[(Basis.proj.arg_x.IsLinearMap_rule _).map_smul]
Proof state after:
no goals
Theorem: SciLean.SciLean.EnumType.sum.arg_f.toMatrix_rule
Proof state before:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (toMatrix K fun x =>  ∑ i, f x i) = fun i j =>  ∑ i', toMatrix K (fun x => f x i') i j
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ((fun x =>  ∑ i, f x i) ⅇ j)) = fun i j =>  ∑ i', ℼ i ((fun x => f x i') ⅇ j)
Theorem: SciLean.SciLean.EnumType.sum.arg_f.toMatrix_rule
Proof state before:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ((fun x =>  ∑ i, f x i) ⅇ j)) = fun i j =>  ∑ i', ℼ i ((fun x => f x i') ⅇ j)
Tactic:
simp
Proof state after:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ( ∑ i, f (ⅇ j) i)) = fun i j =>  ∑ i', ℼ i (f (ⅇ j) i')
Theorem: SciLean.SciLean.EnumType.sum.arg_f.toMatrix_rule
Proof state before:
K : Type
inst✝¹³ : RCLike K
IX : Type
inst✝¹² : IndexType IX
inst✝¹¹ : LawfulIndexType IX
inst✝¹⁰ : DecidableEq IX
X : Type u_2
inst✝⁹ : FinVec IX K X
IY : Type
inst✝⁸ : IndexType IY
inst✝⁷ : LawfulIndexType IY
inst✝⁶ : DecidableEq IY
Y : Type
inst✝⁵ : FinVec IY K Y
IZ : Type
inst✝⁴ : IndexType IZ
inst✝³ : LawfulIndexType IZ
inst✝² : DecidableEq IZ
Z : Type ?u.94168
inst✝¹ : FinVec IZ K Z
ι : Type u_1
inst✝ : IndexType ι
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ (fun i j => ℼ i ( ∑ i, f (ⅇ j) i)) = fun i j =>  ∑ i', ℼ i (f (ⅇ j) i')
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.SciLean.mulVec.arg_x_i.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.101564
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.101649
inst✝ : FinVec IZ K Z
W : Type u_1
iy : IY
A : IY → IX → K
x : W → IX → K
hx : IX → sorryAx Prop true
⊢ sorryAx ((x_1 : ?m.105951 A x hx) → ?m.105952 A x hx x_1 → K) true = fun x_1 iw =>
     ∑ ix', A iy ix' * x (sorryAx W true) ix'
Tactic:
sorry_proof
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.101564
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.101649
inst✝ : FinVec IZ K Z
⊢ {W : Type u_1} → {iy : IY} → (IY → IX → K) → (W → IX → K) → (IX → sorryAx Prop true) → Sort u_2

K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.101564
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.101649
inst✝ : FinVec IZ K Z
⊢ {W : Type u_1} →
    {iy : IY} → (A : IY → IX → K) → (x : W → IX → K) → (hx : IX → sorryAx Prop true) → ?m.105951 A x hx → Type u_3
Theorem: SciLean.norm₂_squared_nat
Proof state before:
R : Type u_1
K : Type u_2
X : Type u_3
inst✝¹ : Scalar R K
inst✝ : Norm2 K X
x : X
⊢ ‖x‖₂ ^ 2 = ‖x‖₂²
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.norm₂_squared
Proof state before:
R : Type u_1
K : Type u_2
X : Type u_3
inst✝¹ : Scalar R K
inst✝ : Norm2 K X
x : X
⊢ ‖x‖₂ ^ 2 = ‖x‖₂²
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_norm
Proof state before:
R : Type u_1
inst✝ : RealScalar R
r : R
⊢ ‖r‖₂[R] = Scalar.abs r
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.norm₂_prod
Proof state before:
R : Type u_1
K : Type u_2
X : Type u_3
Y : Type u_4
inst✝³ : Scalar R K
inst✝² : AddCommMonoid K
inst✝¹ : Inner K X
inst✝ : Inner K Y
x : X
y : Y
⊢ ‖(x, y)‖₂ = Scalar.sqrt (‖x‖₂² + ‖y‖₂²)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.norm₂_scalar
Proof state before:
R : Type u_1
inst✝ : RealScalar R
x : R
⊢ ‖x‖₂[R] = Scalar.abs x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.norm2_scalar
Proof state before:
R : Type u_1
inst✝ : RealScalar R
x : R
⊢ ‖x‖₂² = x ^ 2
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.surfaceDirac_dirac
Proof state before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
⊢ surfaceDirac {x} f 0 = Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)
Tactic:
ext φ
Proof state after:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (surfaceDirac {x} f 0) φ = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Theorem: SciLean.surfaceDirac_dirac
Proof state before:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (surfaceDirac {x} f 0) φ = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Tactic:
unfold surfaceDirac
Proof state after:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (fun φ ⊸[R] ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x}) φ =
    (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Theorem: SciLean.surfaceDirac_dirac
Proof state before:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (fun φ ⊸[R] ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x}) φ =
    (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Tactic:
dsimp
Proof state after:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x} = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Theorem: SciLean.surfaceDirac_dirac
Proof state before:
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ ∫' x, φ x • f x ∂(surfaceMeasure 0).restrict {x} = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.toDistribution.arg_f.parDistribDeriv_rule
Proof state before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
⊢ (parDistribDeriv fun w => ↑fun x => f w x) = fun w dw => ↑fun x => ∂ (x_1:=w;dw), f x_1 x
Tactic:
unfold parDistribDeriv
Proof state after:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = fun w dw => ↑fun x => ∂ (x_1:=w;dw), f x_1 x