internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.DRand.dpure_bindDR
Proof state before:
R : Type ?u.31468
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
f : X → Rand Y
⊢ bindDR (dpure x dx) f = randDeriv f x dx
Tactic:
apply ext
Proof state after:
case a
R : Type ?u.31468
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
f : X → Rand Y
⊢ ∀ (φ : Y → ℝ), (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Theorem: SciLean.Prob.DRand.dpure_bindDR
Proof state before:
case a
R : Type ?u.31468
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
f : X → Rand Y
⊢ ∀ (φ : Y → ℝ), (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Tactic:
intro φ
Proof state after:
case a
R : Type ?u.31468
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
f : X → Rand Y
φ : Y → ℝ
⊢ (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Theorem: SciLean.Prob.DRand.dpure_bindDR
Proof state before:
case a
R : Type ?u.31468
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
f : X → Rand Y
φ : Y → ℝ
⊢ (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Tactic:
simp only [bindDR, dpure, dE, randDeriv,E]
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.bindDR_bindDR
Proof state before:
R : Type ?u.32714
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x : DRand X
g : X → Rand Y
f : Y → Rand Z
⊢ bindDR (bindDR x g) f = bindDR x fun x' => Rand.bind (g x') f
Tactic:
simp (disch:=sorry) only [bindDR,rand_simp,rand_push_E]
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.bindRD_bindDR
Proof state before:
R : Type ?u.34225
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x : Rand X
g : X → DRand Y
f : Y → Rand Z
⊢ bindDR (bindRD x g) f = bindRD x fun x' => bindDR (g x') f
Tactic:
simp (disch:=sorry) only [bindDR,bindRD,rand_simp]
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.id_rule
Proof state before:
K : Type u_2
inst✝⁷ : RCLike K
X : Type u_1
inst✝⁶ : SemiInnerProductSpace K X
Y : Type ?u.105
inst✝⁵ : SemiInnerProductSpace K Y
Z : Type ?u.116
inst✝⁴ : SemiInnerProductSpace K Z
ι : Type ?u.127
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.154
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
⊢ (semiAdjoint K fun x => x) = fun x => x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.const_rule
Proof state before:
K : Type u_3
inst✝⁷ : RCLike K
X : Type u_1
inst✝⁶ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁵ : SemiInnerProductSpace K Y
Z : Type ?u.291
inst✝⁴ : SemiInnerProductSpace K Z
ι : Type ?u.302
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.329
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
⊢ (semiAdjoint K fun x => 0) = fun x => 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.comp_rule
Proof state before:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_4
inst✝⁶ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁵ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁴ : SemiInnerProductSpace K Z
ι : Type ?u.1772
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1799
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
⊢ (semiAdjoint K fun x => f (g x)) = fun z =>
    let y := semiAdjoint K f z;
    let x := semiAdjoint K g y;
    x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.let_rule
Proof state before:
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_4
inst✝⁴ : SemiInnerProductSpace K Z
ι : Type ?u.2103
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.2130
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y → Z
g : X → Y
hf : HasSemiAdjoint K ↿f
hg : HasSemiAdjoint K g
⊢ (semiAdjoint K fun x =>
      let y := g x;
      f x y) =
    fun z =>
    let xy := semiAdjoint K (fun xy => f xy.1 xy.2) z;
    let x' := semiAdjoint K g xy.2;
    xy.1 + x'
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.Prod.mk.arg_fstsnd.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.6409
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.6415
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.6428
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.6439
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.6450
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.6477
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_4
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.6534
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.6545
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.6572
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
g : X → Y
f : X → Z
hg : HasSemiAdjoint K g
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => (g x, f x)) = fun yz =>
    let x₁ := semiAdjoint K g yz.1;
    let x₂ := semiAdjoint K f yz.2;
    x₁ + x₂
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.Prod.fst.arg_self.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.8126
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.8132
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.8145
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.8156
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.8167
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.8194
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_1
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_2
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.8251
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.8262
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.8289
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y × Z
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => (f x).1) = fun y => semiAdjoint K (fun x => f x) (y, 0)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.Prod.snd.arg_self.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.9121
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.9127
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.9140
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.9151
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.9162
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.9189
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_1
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_2
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.9246
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.9257
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9284
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y × Z
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => (f x).2) = fun z => semiAdjoint K f (0, z)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HAdd.hAdd.arg_a0a1.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.10114
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.10120
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.10133
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.10144
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.10155
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.10182
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.10228
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.10239
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.10250
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.10277
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
⊢ (semiAdjoint K fun x => f x + g x) = fun y =>
    let x₁ := semiAdjoint K f y;
    let x₂ := semiAdjoint K g y;
    x₁ + x₂
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HSub.hSub.arg_a0a1.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.12852
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.12858
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.12871
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.12882
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.12893
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.12920
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.12966
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.12977
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.12988
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13015
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
⊢ (semiAdjoint K fun x => f x - g x) = fun y =>
    let x₁ := semiAdjoint K f y;
    let x₂ := semiAdjoint K g y;
    x₁ - x₂
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.Neg.neg.arg_a0.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.14518
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.14524
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.14537
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.14548
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.14559
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.14586
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.14632
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.14643
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.14654
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.14681
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
⊢ (semiAdjoint K fun x => -f x) = fun y => -semiAdjoint K f y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HMul.hMul.arg_a0.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.15338
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.15344
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.15357
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.15368
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.15379
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.15406
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type ?u.15441
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.15452
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.15463
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.15474
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15501
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : K
f : X → K
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => f x * c) = fun y => (starRingEnd K) c • semiAdjoint K (fun x => f x) y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HMul.hMul.arg_a1.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.17569
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.17575
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.17588
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.17599
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.17610
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.17637
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type ?u.17672
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.17683
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.17694
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.17705
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17732
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : K
f : X → K
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => c * f x) = fun y => (starRingEnd K) c • semiAdjoint K (fun x => f x) y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HSMul.hSMul.arg_a0.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.19800
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.19806
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝¹ : Type ?u.19819
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝¹
Z✝ : Type ?u.19830
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.19841
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.19868
inst✝¹⁰ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y✝ : Type ?u.19903
inst✝⁷ : SemiInnerProductSpace K Y✝
Z : Type ?u.19914
inst✝⁶ : SemiInnerProductSpace K Z
W : Type ?u.19925
inst✝⁵ : SemiInnerProductSpace K W
ι : Type ?u.19936
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.19963
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
Y : Type u_1
inst✝ : SemiHilbert K Y
y' : Y
f : X → K
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => f x • y') = fun y => semiAdjoint K (fun x => f x) ⟪y', y⟫_K
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HSMul.hSMul.arg_a1.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.21779
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.21785
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.21798
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.21809
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.21820
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.21847
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.21893
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.21904
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.21915
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.21942
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : K
g : X → Y
hg : HasSemiAdjoint K g
⊢ (semiAdjoint K fun x => c • g x) = fun y => (starRingEnd K) c • semiAdjoint K g y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.HDiv.hDiv.arg_a0.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.25283
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.25289
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.25302
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.25313
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.25324
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.25351
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type ?u.25386
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.25397
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.25408
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.25419
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.25446
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → K
c : K
hf : HasSemiAdjoint K f
⊢ (semiAdjoint K fun x => f x / c) = fun y => ((starRingEnd K) c)⁻¹ • semiAdjoint K f y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.Finset.sum.arg_f.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.27546
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.27552
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.27565
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.27576
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝¹ : Type ?u.27587
inst✝¹³ : IndexType ι✝¹
inst✝¹² : LawfulIndexType ι✝¹
inst✝¹¹ : DecidableEq ι✝¹
E✝ : ι✝¹ → Type ?u.27614
inst✝¹⁰ : (i : ι✝¹) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y : Type u_4
inst✝⁷ : SemiInnerProductSpace K Y
Z : Type ?u.27660
inst✝⁶ : SemiInnerProductSpace K Z
W : Type ?u.27671
inst✝⁵ : SemiInnerProductSpace K W
ι✝ : Type ?u.27682
inst✝⁴ : IndexType ι✝
inst✝³ : LawfulIndexType ι✝
inst✝² : DecidableEq ι✝
E : ι✝ → Type ?u.27709
inst✝¹ : (i : ι✝) → SemiInnerProductSpace K (E i)
ι : Type u_1
inst✝ : Fintype ι
f : X → ι → Y
hf : ∀ (i : ι), HasSemiAdjoint K fun x => f x i
⊢ (semiAdjoint K fun x => ∑ i : ι, f x i) = fun y => ∑ i : ι, semiAdjoint K (fun x => f x i) y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.IndexType.sum.arg_f.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.31242
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.31248
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.31261
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.31272
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.31283
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.31310
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.31356
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.31367
inst✝⁴ : SemiInnerProductSpace K W
ι : Type u_3
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.31405
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → ι → Y
hf : ∀ (i : ι), HasSemiAdjoint K fun x => f x i
⊢ (semiAdjoint K fun x =>  ∑ i, f x i) = fun y =>  ∑ i, semiAdjoint K (fun x => f x i) y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.semiAdjoint.ite.arg_te.semiAdjoint_rule
Proof state before:
K✝ : Type ?u.34023
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.34029
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.34042
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.34053
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.34064
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.34091
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.34137
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.34148
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.34159
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.34186
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
dec : Decidable c
t e : X → Y
⊢ (semiAdjoint K fun x => if c then t x else e x) = fun y => if c then semiAdjoint K t y else semiAdjoint K e y
Tactic:
induction dec
Proof state after:
case isFalse
K✝ : Type ?u.34023
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.34029
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.34042
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.34053
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.34064
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.34091
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.34137
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.34148
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.34159
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.34186
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t e : X → Y
h✝ : ¬c
⊢ (semiAdjoint K fun x => if c then t x else e x) = fun y => if c then semiAdjoint K t y else semiAdjoint K e y

case isTrue
K✝ : Type ?u.34023
inst✝¹⁶ : RCLike K✝
X✝ : Type ?u.34029
inst✝¹⁵ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.34042
inst✝¹⁴ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.34053
inst✝¹³ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.34064
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.34091
inst✝⁹ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type ?u.34137
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.34148
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.34159
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.34186
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t e : X → Y
h✝ : c
⊢ (semiAdjoint K fun x => if c then t x else e x) = fun y => if c then semiAdjoint K t y else semiAdjoint K e y