internlm/Lean-Github huggingface dataset:
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a0.HasSemiAdjoint_rule
Proof state before:
case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K
Tactic:
. fun_prop
Proof state after:
no goals
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a0.HasSemiAdjoint_rule
Proof state before:
case semiAdjoint_exists
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∃ f', ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪f' y_1, x⟫_K
Tactic:
apply Exists.intro (fun (c : K) => (conj c) • semiAdjoint K f y) _
Proof state after:
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∀ (x : X) (y_1 : K),
    TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪(fun c => (starRingEnd K) c • semiAdjoint K f y) y_1, x⟫_K
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a0.HasSemiAdjoint_rule
Proof state before:
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∀ (x : X) (y_1 : K),
    TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪(fun c => (starRingEnd K) c • semiAdjoint K f y) y_1, x⟫_K
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a0.HasSemiAdjoint_rule
Proof state before:
case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a1.HasSemiAdjoint_rule
Proof state before:
case is_differentiable
K✝¹ : Type ?u.55418
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.55424
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.55437
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.55448
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.55459
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.55470
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.55497
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.55513
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.55519
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.55532
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.55543
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.55554
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.55565
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.55592
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪y, f x⟫_K
Tactic:
. fun_prop
Proof state after:
no goals
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a1.HasSemiAdjoint_rule
Proof state before:
case semiAdjoint_exists
K✝¹ : Type ?u.55418
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.55424
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.55437
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.55448
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.55459
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.55470
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.55497
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.55513
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.55519
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.55532
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.55543
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.55554
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.55565
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.55592
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∃ f', ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪y, f x⟫_K⟫_K = ⟪f' y_1, x⟫_K
Tactic:
apply Exists.intro (fun (c : K) => c • semiAdjoint K f y) _
Proof state after:
K✝¹ : Type ?u.55418
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.55424
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.55437
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.55448
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.55459
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.55470
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.55497
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.55513
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.55519
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.55532
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.55543
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.55554
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.55565
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.55592
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪y, f x⟫_K⟫_K = ⟪(fun c => c • semiAdjoint K f y) y_1, x⟫_K
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a1.HasSemiAdjoint_rule
Proof state before:
K✝¹ : Type ?u.55418
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.55424
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.55437
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.55448
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.55459
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.55470
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.55497
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.55513
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.55519
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.55532
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.55543
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.55554
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.55565
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.55592
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪y, f x⟫_K⟫_K = ⟪(fun c => c • semiAdjoint K f y) y_1, x⟫_K
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a1.HasSemiAdjoint_rule
Proof state before:
case is_differentiable
K✝¹ : Type ?u.55418
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.55424
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.55437
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.55448
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.55459
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.55470
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.55497
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.55513
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.55519
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.55532
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.55543
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.55554
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.55565
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.55592
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪y, f x⟫_K
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.HasSemiAdjoint.SciLean.semiAdjoint.arg_y.HasSemiAdjoint_rule
Proof state before:
K✝ : Type ?u.58357
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.58363
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.58376
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.58387
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
W✝ : Type ?u.58398
inst✝¹³ : SemiInnerProductSpace K✝ W✝
ι✝ : Type ?u.58409
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.58436
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.58482
inst✝⁵ : SemiInnerProductSpace K Z
W : Type u_2
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.58504
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58531
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
a0 : W → Y
ha0 : HasSemiAdjoint K a0
⊢ HasSemiAdjoint K fun w => semiAdjoint K f (a0 w)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.mk_fst
Proof state before:
X Y : Type u_1
x : X
y : Y
⊢ { fst := x, snd := y }.fst = x
Tactic:
simp
Proof state after:
no goals
Theorem: MProd.mk_snd
Proof state before:
X Y : Type u_1
x : X
y : Y
⊢ { fst := x, snd := y }.snd = y
Tactic:
simp
Proof state after:
no goals
Theorem: MProd.add_mk
Proof state before:
X Y : Type u_1
inst✝¹ : Add X
inst✝ : Add Y
x x' : X
y y' : Y
⊢ { fst := x, snd := y } + { fst := x', snd := y' } = { fst := x + x', snd := y + y' }
Tactic:
rfl
Proof state after:
no goals
Theorem: MProd.sub_mk
Proof state before:
X Y : Type u_1
inst✝¹ : Sub X
inst✝ : Sub Y
x x' : X
y y' : Y
⊢ { fst := x, snd := y } - { fst := x', snd := y' } = { fst := x - x', snd := y - y' }
Tactic:
rfl
Proof state after:
no goals
Theorem: MProd.smul_mk
Proof state before:
K : Type u_1
X Y : Type u_2
inst✝¹ : SMul K X
inst✝ : SMul K Y
k : K
x : X
y : Y
⊢ k • { fst := x, snd := y } = { fst := k • x, snd := k • y }
Tactic:
rfl
Proof state after:
no goals
Theorem: MProd.neg_mk
Proof state before:
X Y : Type u_1
inst✝¹ : Neg X
inst✝ : Neg Y
x : X
y : Y
⊢ -{ fst := x, snd := y } = { fst := -x, snd := -y }
Tactic:
rfl
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.CDifferentiable_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : Vec K X
Y : Type u_3
inst✝¹ : Vec K Y
W : Type u_2
inst✝ : Vec K W
f : W → X
g : W → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ CDifferentiable K fun w => { fst := f w, snd := g w }
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.cderiv_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : Vec K X
Y : Type u_3
inst✝¹ : Vec K Y
W : Type u_2
inst✝ : Vec K W
f : W → X
g : W → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (cderiv K fun w => { fst := f w, snd := g w }) = fun w dw =>
    let dx := cderiv K f w dw;
    let dy := cderiv K g w dw;
    { fst := dx, snd := dy }
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.fwdDeriv_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : Vec K X
Y : Type u_3
inst✝¹ : Vec K Y
W : Type u_2
inst✝ : Vec K W
f : W → X
g : W → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (fwdDeriv K fun w => { fst := f w, snd := g w }) = fun w dw =>
    let xdx := fwdDeriv K f w dw;
    let ydy := fwdDeriv K g w dw;
    ({ fst := xdx.1, snd := ydy.1 }, { fst := xdx.2, snd := ydy.2 })
Tactic:
unfold fwdDeriv
Proof state after:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : Vec K X
Y : Type u_3
inst✝¹ : Vec K Y
W : Type u_2
inst✝ : Vec K W
f : W → X
g : W → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (fun x dx => ((fun w => { fst := f w, snd := g w }) x, cderiv K (fun w => { fst := f w, snd := g w }) x dx)) =
    fun w dw =>
    let xdx := (f w, cderiv K f w dw);
    let ydy := (g w, cderiv K g w dw);
    ({ fst := xdx.1, snd := ydy.1 }, { fst := xdx.2, snd := ydy.2 })
Theorem: MProd.mk.arg_fstsnd.fwdDeriv_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : Vec K X
Y : Type u_3
inst✝¹ : Vec K Y
W : Type u_2
inst✝ : Vec K W
f : W → X
g : W → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (fun x dx => ((fun w => { fst := f w, snd := g w }) x, cderiv K (fun w => { fst := f w, snd := g w }) x dx)) =
    fun w dw =>
    let xdx := (f w, cderiv K f w dw);
    let ydy := (g w, cderiv K g w dw);
    ({ fst := xdx.1, snd := ydy.1 }, { fst := xdx.2, snd := ydy.2 })
Tactic:
fun_trans
Proof state after:
no goals
Theorem: MProd.fst.arg_self.CDifferentiable_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : Vec K X
Y : Type u_1
inst✝¹ : Vec K Y
W : Type u_3
inst✝ : Vec K W
f : W → MProd X Y
hf : CDifferentiable K f
⊢ CDifferentiable K fun w => (f w).fst
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.fst.arg_self.fwdDeriv_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : Vec K X
Y : Type u_1
inst✝¹ : Vec K Y
W : Type u_3
inst✝ : Vec K W
f : W → MProd X Y
hf : CDifferentiable K f
⊢ (fwdDeriv K fun w => (f w).fst) = fun w dw =>
    let xydxy := fwdDeriv K f w dw;
    (xydxy.1.fst, xydxy.2.fst)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.snd.arg_self.CDifferentiable_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : Vec K X
Y : Type u_1
inst✝¹ : Vec K Y
W : Type u_3
inst✝ : Vec K W
f : W → MProd X Y
hf : CDifferentiable K f
⊢ CDifferentiable K fun w => (f w).snd
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.snd.arg_self.fwdDeriv_rule
Proof state before:
K : Type u_2
inst✝³ : RCLike K
X : Type u_1
inst✝² : Vec K X
Y : Type u_1
inst✝¹ : Vec K Y
W : Type u_3
inst✝ : Vec K W
f : W → MProd X Y
hf : CDifferentiable K f
⊢ (fwdDeriv K fun w => (f w).snd) = fun w dw =>
    let xydxy := fwdDeriv K f w dw;
    (xydxy.1.snd, xydxy.2.snd)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.HasSemiAdjoint_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
⊢ HasSemiAdjoint K fun w => { fst := f w, snd := g w }
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.semiAdjoint_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
⊢ (semiAdjoint K fun w => { fst := f w, snd := g w }) = fun xy =>
    let w₁ := semiAdjoint K f xy.fst;
    let w₂ := semiAdjoint K g xy.snd;
    w₁ + w₂
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.HasAdjDiff_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ HasAdjDiff K fun w => { fst := f w, snd := g w }
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasAdjDiffAt K (fun w => { fst := f w, snd := g w }) x
Theorem: MProd.mk.arg_fstsnd.HasAdjDiff_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasAdjDiffAt K (fun w => { fst := f w, snd := g w }) x
Tactic:
constructor
Proof state after:
case left
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ CDifferentiableAt K (fun w => { fst := f w, snd := g w }) x

case right
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasSemiAdjoint K (cderiv K (fun w => { fst := f w, snd := g w }) x)
Theorem: MProd.mk.arg_fstsnd.HasAdjDiff_rule
Proof state before:
case left
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ CDifferentiableAt K (fun w => { fst := f w, snd := g w }) x

case right
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasSemiAdjoint K (cderiv K (fun w => { fst := f w, snd := g w }) x)
Tactic:
fun_prop
Proof state after:
case right
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasSemiAdjoint K (cderiv K (fun w => { fst := f w, snd := g w }) x)
Theorem: MProd.mk.arg_fstsnd.HasAdjDiff_rule
Proof state before:
case right
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasSemiAdjoint K (cderiv K (fun w => { fst := f w, snd := g w }) x)
Tactic:
fun_trans
Proof state after:
case right
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasSemiAdjoint K fun dw => { fst := cderiv K (fun w => f w) x dw, snd := cderiv K (fun w => g w) x dw }
Theorem: MProd.mk.arg_fstsnd.HasAdjDiff_rule
Proof state before:
case right
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
⊢ HasSemiAdjoint K fun dw => { fst := cderiv K (fun w => f w) x dw, snd := cderiv K (fun w => g w) x dw }
Tactic:
fun_prop
Proof state after:
no goals
Theorem: MProd.mk.arg_fstsnd.revDeriv_rule
Proof state before:
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
⊢ (revDeriv K fun w => { fst := f w, snd := g w }) = fun w =>
    let xdf' := revDeriv K f w;
    let ydg' := revDeriv K g w;
    ({ fst := xdf'.1, snd := ydg'.1 }, fun dxy => xdf'.2 dxy.fst + ydg'.2 dxy.snd)
Tactic:
sorry_proof
Proof state after:
no goals