internlm/Lean-Github huggingface dataset:
Theorem: SciLean.IndexType.sum.arg_f.ContCDiff_rule
Proof state before:
K✝ : Type ?u.33900
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.33908
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.33921
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.33932
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.33943
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.33952
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.33998
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type ?u.34018
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
⊢ ContCDiff K n fun x =>  ∑ i, f x i
Tactic:
intro x
Proof state after:
K✝ : Type ?u.33900
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.33908
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.33921
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.33932
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.33943
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.33952
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.33998
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type ?u.34018
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
x : X
⊢ ContCDiffAt K n (fun x =>  ∑ i, f x i) x
Theorem: SciLean.IndexType.sum.arg_f.ContCDiff_rule
Proof state before:
K✝ : Type ?u.33900
inst✝¹¹ : RCLike K✝
n : ℕ∞
X✝ : Type ?u.33908
inst✝¹⁰ : Vec K✝ X✝
Y✝ : Type ?u.33921
inst✝⁹ : Vec K✝ Y✝
Z✝ : Type ?u.33932
inst✝⁸ : Vec K✝ Z✝
ι✝ : Type ?u.33943
inst✝⁷ : IndexType ι✝
E✝ : ι✝ → Type ?u.33952
inst✝⁶ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁵ : RCLike K
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.33998
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type ?u.34018
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
hf : ∀ (i : ι), ContCDiff K n fun x => f x i
x : X
⊢ ContCDiffAt K n (fun x =>  ∑ i, f x i) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.36006
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.36014
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.36027
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.36038
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.36049
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.36058
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.36074
inst✝⁸ : RCLike K
X✝ : Type ?u.36080
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.36093
inst✝⁶ : Vec K Y✝
Z : Type ?u.36104
inst✝⁵ : Vec K Z
ι : Type ?u.36115
inst✝⁴ : IndexType ι
E : ι → Type ?u.36124
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
x : X
hf : ContCDiffAt R n f x
hg : ContCDiffAt R n g x
⊢ ContCDiffAt R n (fun x => ⟪f x, g x⟫_R) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.ContCDiff_rule
Proof state before:
K✝ : Type ?u.36496
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.36504
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.36517
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.36528
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.36539
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.36548
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.36564
inst✝⁸ : RCLike K
X✝ : Type ?u.36570
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.36583
inst✝⁶ : Vec K Y✝
Z : Type ?u.36594
inst✝⁵ : Vec K Z
ι : Type ?u.36605
inst✝⁴ : IndexType ι
E : ι → Type ?u.36614
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : ContCDiff R n f
hg : ContCDiff R n g
⊢ ContCDiff R n fun x => ⟪f x, g x⟫_R
Tactic:
intro x
Proof state after:
K✝ : Type ?u.36496
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.36504
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.36517
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.36528
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.36539
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.36548
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.36564
inst✝⁸ : RCLike K
X✝ : Type ?u.36570
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.36583
inst✝⁶ : Vec K Y✝
Z : Type ?u.36594
inst✝⁵ : Vec K Z
ι : Type ?u.36605
inst✝⁴ : IndexType ι
E : ι → Type ?u.36614
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : ContCDiff R n f
hg : ContCDiff R n g
x : X
⊢ ContCDiffAt R n (fun x => ⟪f x, g x⟫_R) x
Theorem: SciLean.Inner.inner.arg_a0a1.ContCDiff_rule
Proof state before:
K✝ : Type ?u.36496
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.36504
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.36517
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.36528
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.36539
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.36548
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.36564
inst✝⁸ : RCLike K
X✝ : Type ?u.36570
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.36583
inst✝⁶ : Vec K Y✝
Z : Type ?u.36594
inst✝⁵ : Vec K Z
ι : Type ?u.36605
inst✝⁴ : IndexType ι
E : ι → Type ?u.36614
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : ContCDiff R n f
hg : ContCDiff R n g
x : X
⊢ ContCDiffAt R n (fun x => ⟪f x, g x⟫_R) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Norm2.norm2.arg_a0.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.37395
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.37403
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.37416
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.37427
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.37438
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.37447
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.37463
inst✝⁸ : RCLike K
X✝ : Type ?u.37469
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.37482
inst✝⁶ : Vec K Y✝
Z : Type ?u.37493
inst✝⁵ : Vec K Z
ι : Type ?u.37504
inst✝⁴ : IndexType ι
E : ι → Type ?u.37513
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : ContCDiffAt R n f x
⊢ ContCDiffAt R n (fun x => ‖f x‖₂²) x
Tactic:
simp[← SemiInnerProductSpace.inner_norm2]
Proof state after:
K✝ : Type ?u.37395
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.37403
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.37416
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.37427
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.37438
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.37447
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.37463
inst✝⁸ : RCLike K
X✝ : Type ?u.37469
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.37482
inst✝⁶ : Vec K Y✝
Z : Type ?u.37493
inst✝⁵ : Vec K Z
ι : Type ?u.37504
inst✝⁴ : IndexType ι
E : ι → Type ?u.37513
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : ContCDiffAt R n f x
⊢ ContCDiffAt R n (fun x => ⟪f x, f x⟫_R) x
Theorem: SciLean.Norm2.norm2.arg_a0.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.37395
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.37403
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.37416
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.37427
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.37438
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.37447
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.37463
inst✝⁸ : RCLike K
X✝ : Type ?u.37469
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.37482
inst✝⁶ : Vec K Y✝
Z : Type ?u.37493
inst✝⁵ : Vec K Z
ι : Type ?u.37504
inst✝⁴ : IndexType ι
E : ι → Type ?u.37513
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : ContCDiffAt R n f x
⊢ ContCDiffAt R n (fun x => ⟪f x, f x⟫_R) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Norm2.norm2.arg_a0.ContCDiff_rule
Proof state before:
K✝ : Type ?u.38767
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.38775
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.38788
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.38799
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.38810
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.38819
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.38835
inst✝⁸ : RCLike K
X✝ : Type ?u.38841
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.38854
inst✝⁶ : Vec K Y✝
Z : Type ?u.38865
inst✝⁵ : Vec K Z
ι : Type ?u.38876
inst✝⁴ : IndexType ι
E : ι → Type ?u.38885
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
⊢ ContCDiff R n fun x => ‖f x‖₂²
Tactic:
intro x
Proof state after:
K✝ : Type ?u.38767
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.38775
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.38788
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.38799
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.38810
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.38819
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.38835
inst✝⁸ : RCLike K
X✝ : Type ?u.38841
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.38854
inst✝⁶ : Vec K Y✝
Z : Type ?u.38865
inst✝⁵ : Vec K Z
ι : Type ?u.38876
inst✝⁴ : IndexType ι
E : ι → Type ?u.38885
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
x : X
⊢ ContCDiffAt R n (fun x => ‖f x‖₂²) x
Theorem: SciLean.Norm2.norm2.arg_a0.ContCDiff_rule
Proof state before:
K✝ : Type ?u.38767
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.38775
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.38788
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.38799
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.38810
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.38819
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.38835
inst✝⁸ : RCLike K
X✝ : Type ?u.38841
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.38854
inst✝⁶ : Vec K Y✝
Z : Type ?u.38865
inst✝⁵ : Vec K Z
ι : Type ?u.38876
inst✝⁴ : IndexType ι
E : ι → Type ?u.38885
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
x : X
⊢ ContCDiffAt R n (fun x => ‖f x‖₂²) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.ContCDiffAt_rule
Proof state before:
K✝ : Type ?u.39487
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.39495
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.39508
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.39519
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.39530
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.39539
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.39555
inst✝⁸ : RCLike K
X✝ : Type ?u.39561
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.39574
inst✝⁶ : Vec K Y✝
Z : Type ?u.39585
inst✝⁵ : Vec K Z
ι : Type ?u.39596
inst✝⁴ : IndexType ι
E : ι → Type ?u.39605
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : ContCDiffAt R n f x
hx : f x ≠ 0
⊢ ContCDiffAt R n (fun x => ‖f x‖₂[R]) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.ContCDiff_rule
Proof state before:
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
⊢ ContCDiff R n fun x => ‖f x‖₂[R]
Tactic:
intro x
Proof state after:
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ ContCDiffAt R n (fun x => ‖f x‖₂[R]) x
Theorem: SciLean.norm₂.arg_x.ContCDiff_rule
Proof state before:
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ ContCDiffAt R n (fun x => ‖f x‖₂[R]) x
Tactic:
fun_prop (disch:=aesop)
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.ContCDiff_rule
Proof state before:
case funProp.discharger
K✝ : Type ?u.40925
inst✝¹⁴ : RCLike K✝
n : ℕ∞
X✝¹ : Type ?u.40933
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.40946
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.40957
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.40968
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.40977
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.40993
inst✝⁸ : RCLike K
X✝ : Type ?u.40999
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.41012
inst✝⁶ : Vec K Y✝
Z : Type ?u.41023
inst✝⁵ : Vec K Z
ι : Type ?u.41034
inst✝⁴ : IndexType ι
E : ι → Type ?u.41043
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : ContCDiff R n f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ f x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Basis.proj.arg_x.ContCDiffAt_rule
Proof state before:
K✝¹ : Type ?u.45253
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.45261
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.45274
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.45285
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.45296
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.45305
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.45321
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.45327
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.45340
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.45351
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.45362
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.45371
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.45485
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.45570
inst✝ : FinVec IZ K Z
i : IX
x : X
⊢ ContCDiffAt K n (fun x => ℼ i x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DualBasis.dualProj.arg_x.ContCDiffAt_rule
Proof state before:
K✝¹ : Type ?u.46029
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.46037
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.46050
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.46061
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.46072
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.46081
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.46097
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.46103
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.46116
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.46127
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.46138
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.46147
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.46261
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.46346
inst✝ : FinVec IZ K Z
i : IX
x : X
⊢ ContCDiffAt K n (fun x => ℼ' i x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.toDual.arg_x.ContCDiffAt_rule
Proof state before:
K✝¹ : Type ?u.46805
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.46813
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.46826
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.46837
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.46848
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.46857
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.46873
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.46879
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.46892
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.46903
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.46914
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.46923
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.47037
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.47122
inst✝ : FinVec IZ K Z
x : X
⊢ ContCDiffAt K n (fun x => toDual x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.fromDual.arg_x.ContCDiffAt_rule
Proof state before:
K✝¹ : Type ?u.47454
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.47462
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.47475
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.47486
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.47497
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.47506
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.47522
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.47528
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.47541
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.47552
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.47563
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.47572
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.47686
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.47771
inst✝ : FinVec IZ K Z
x : X
⊢ ContCDiffAt K n (fun x => fromDual x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Basis.proj.arg_x.ContCDiff_rule
Proof state before:
K✝¹ : Type ?u.48103
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.48111
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.48124
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.48135
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.48146
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.48155
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.48171
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.48177
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.48190
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.48201
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.48212
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.48221
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.48335
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.48420
inst✝ : FinVec IZ K Z
i : IX
⊢ ContCDiff K n fun x => ℼ i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DualBasis.dualProj.arg_x.ContCDiff_rule
Proof state before:
K✝¹ : Type ?u.48872
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.48880
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.48893
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.48904
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.48915
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.48924
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.48940
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.48946
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.48959
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.48970
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.48981
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.48990
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.49104
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.49189
inst✝ : FinVec IZ K Z
i : IX
⊢ ContCDiff K n fun x => ℼ' i x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.toDual.arg_x.ContCDiff_rule
Proof state before:
K✝¹ : Type ?u.49641
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.49649
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.49662
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.49673
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.49684
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.49693
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.49709
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.49715
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.49728
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.49739
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.49750
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.49759
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.49873
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.49958
inst✝ : FinVec IZ K Z
⊢ ContCDiff K n fun x => toDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.fromDual.arg_x.ContCDiff_rule
Proof state before:
K✝¹ : Type ?u.50282
inst✝²⁴ : RCLike K✝¹
n : ℕ∞
X✝¹ : Type ?u.50290
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.50303
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.50314
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.50325
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.50334
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.50350
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.50356
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.50369
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.50380
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.50391
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.50400
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
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 ?u.50514
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.50599
inst✝ : FinVec IZ K Z
⊢ ContCDiff K n fun x => fromDual x
Tactic:
sorry_proof
Proof state after:
no goals