internlm/Lean-Github huggingface dataset:
Theorem: SciLean.dite.arg_te.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
dec : Decidable c
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x
Tactic:
induction dec
Proof state after:
case isFalse
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
h✝ : ¬c
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x

case isTrue
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
h✝ : c
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x
Theorem: SciLean.dite.arg_te.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
h : c
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x
Tactic:
case isTrue h  => simp[ht,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
h : ¬c
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x
Tactic:
case isFalse h => simp[he,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
h : c
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x
Tactic:
simp[ht,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiffAt_rule
Proof state before:
K✝ : Type ?u.77306
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77312
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77325
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77336
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77347
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77374
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77420
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.77431
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.77442
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.77469
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
x : X
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiffAt K (t h) x
he : ∀ (h : ¬c), HasAdjDiffAt K (e h) x
h : ¬c
⊢ HasAdjDiffAt K (fun x => if x_1 : c then t x_1 x else e x_1 x) x
Tactic:
simp[he,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
dec : Decidable c
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
induction dec
Proof state after:
case isFalse
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
h✝ : ¬c
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x

case isTrue
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
h✝ : c
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x
Theorem: SciLean.dite.arg_te.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
h : c
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
case isTrue h  => simp[ht,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
h : ¬c
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
case isFalse h => simp[he,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
h : c
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
simp[ht,h]
Proof state after:
no goals
Theorem: SciLean.dite.arg_te.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.77878
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.77884
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.77897
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.77908
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.77919
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.77946
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_3
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.77992
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.78003
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.78014
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.78041
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → Y
e : ¬c → X → Y
ht : ∀ (h : c), HasAdjDiff K (t h)
he : ∀ (h : ¬c), HasAdjDiff K (e h)
h : ¬c
⊢ HasAdjDiff K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
simp[he,h]
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.HasAdjDiffAt_rule
Proof state before:
case right
K✝ : Type ?u.78670
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.78676
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.78689
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.78700
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.78711
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.78738
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.78754
inst✝¹¹ : RCLike K
X✝ : Type ?u.78760
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.78773
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.78784
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.78795
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.78806
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.78833
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f g : X → Y
hf : HasAdjDiffAt R f x
hg : HasAdjDiffAt R g x
⊢ HasSemiAdjoint R (cderiv R (fun x => ⟪f x, g x⟫_R) x)
Tactic:
fun_trans
Proof state after:
case right
K✝ : Type ?u.78670
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.78676
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.78689
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.78700
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.78711
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.78738
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.78754
inst✝¹¹ : RCLike K
X✝ : Type ?u.78760
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.78773
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.78784
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.78795
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.78806
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.78833
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f g : X → Y
hf : HasAdjDiffAt R f x
hg : HasAdjDiffAt R g x
⊢ HasSemiAdjoint R fun dx => ⟪cderiv R (fun x => f x) x dx, g x⟫_R + ⟪f x, cderiv R (fun x => g x) x dx⟫_R
Theorem: SciLean.Inner.inner.arg_a0a1.HasAdjDiffAt_rule
Proof state before:
case right
K✝ : Type ?u.78670
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.78676
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.78689
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.78700
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.78711
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.78738
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.78754
inst✝¹¹ : RCLike K
X✝ : Type ?u.78760
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.78773
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.78784
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.78795
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.78806
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.78833
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
x : X
f g : X → Y
hf : HasAdjDiffAt R f x
hg : HasAdjDiffAt R g x
⊢ HasSemiAdjoint R fun dx => ⟪cderiv R (fun x => f x) x dx, g x⟫_R + ⟪f x, cderiv R (fun x => g x) x dx⟫_R
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.Inner.inner.arg_a0a1.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.82437
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.82443
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.82456
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.82467
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.82478
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.82505
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.82521
inst✝¹¹ : RCLike K
X✝ : Type ?u.82527
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.82540
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.82551
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.82562
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.82573
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.82600
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
⊢ HasAdjDiff R fun x => ⟪f x, g x⟫_R
Tactic:
intro x
Proof state after:
K✝ : Type ?u.82437
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.82443
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.82456
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.82467
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.82478
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.82505
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.82521
inst✝¹¹ : RCLike K
X✝ : Type ?u.82527
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.82540
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.82551
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.82562
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.82573
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.82600
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x : X
⊢ HasAdjDiffAt R (fun x => ⟪f x, g x⟫_R) x
Theorem: SciLean.Inner.inner.arg_a0a1.HasAdjDiff_rule
Proof state before:
K✝ : Type ?u.82437
inst✝¹⁹ : RCLike K✝
X✝¹ : Type ?u.82443
inst✝¹⁸ : SemiInnerProductSpace K✝ X✝¹
Y✝¹ : Type ?u.82456
inst✝¹⁷ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.82467
inst✝¹⁶ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.82478
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.82505
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type ?u.82521
inst✝¹¹ : RCLike K
X✝ : Type ?u.82527
inst✝¹⁰ : SemiInnerProductSpace K X✝
Y✝ : Type ?u.82540
inst✝⁹ : SemiInnerProductSpace K Y✝
Z : Type ?u.82551
inst✝⁸ : SemiInnerProductSpace K Z
W : Type ?u.82562
inst✝⁷ : SemiInnerProductSpace K W
ι : Type ?u.82573
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.82600
inst✝³ : (i : ι) → SemiInnerProductSpace K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : HasAdjDiff R f
hg : HasAdjDiff R g
x : X
⊢ HasAdjDiffAt R (fun x => ⟪f x, g x⟫_R) x
Tactic:
fun_prop
Proof state after:
no goals