internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.action_mk_apply
Proof state before:
W : Type ?u.12970
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.13649
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
φ : X → Y
⊢ ⟪{ action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] => f }, φ⟫ = f φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.Distribution.ext
Proof state before:
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
x y : Distribution X
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪x, φ⟫ = ⟪y, φ⟫) →
    x = y
Tactic:
induction x
Proof state after:
case mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
y : Distribution X
action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪{ action := action✝ }, φ⟫ = ⟪y, φ⟫) →
    { action := action✝ } = y
Theorem: SciLean.Prob.Distribution.ext
Proof state before:
case mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
y : Distribution X
action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪{ action := action✝ }, φ⟫ = ⟪y, φ⟫) →
    { action := action✝ } = y
Tactic:
induction y
Proof state after:
case mk.mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪{ action := action✝¹ }, φ⟫ = ⟪{ action := action✝ }, φ⟫) →
    { action := action✝¹ } = { action := action✝ }
Theorem: SciLean.Prob.Distribution.ext
Proof state before:
case mk.mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪{ action := action✝¹ }, φ⟫ = ⟪{ action := action✝ }, φ⟫) →
    { action := action✝¹ } = { action := action✝ }
Tactic:
simp only [action_mk_apply, mk.injEq]
Proof state after:
case mk.mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      action✝¹ φ = action✝ φ) →
    action✝¹ = action✝
Theorem: SciLean.Prob.Distribution.ext
Proof state before:
case mk.mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      action✝¹ φ = action✝ φ) →
    action✝¹ = action✝
Tactic:
intro h
Proof state after:
case mk.mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
⊢ action✝¹ = action✝
Theorem: SciLean.Prob.Distribution.ext
Proof state before:
case mk.mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
⊢ action✝¹ = action✝
Tactic:
funext _ _ _ _ φ
Proof state after:
case mk.mk.h.h.h.h.h
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
x✝³ : Type u
x✝² : NormedAddCommGroup x✝³
x✝¹ : NormedSpace ℝ x✝³
x✝ : CompleteSpace x✝³
φ : X → x✝³
⊢ action✝¹ φ = action✝ φ
Theorem: SciLean.Prob.Distribution.ext
Proof state before:
case mk.mk.h.h.h.h.h
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
x✝³ : Type u
x✝² : NormedAddCommGroup x✝³
x✝¹ : NormedSpace ℝ x✝³
x✝ : CompleteSpace x✝³
φ : X → x✝³
⊢ action✝¹ φ = action✝ φ
Tactic:
apply (h φ)
Proof state after:
no goals
Theorem: SciLean.Prob.action_bind
Proof state before:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.25149
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
x : Distribution X
f : X → Distribution Y
φ : Y → W
⊢ ⟪x >>= f, φ⟫ = ⟪x, fun x' => ⟪f x', φ⟫⟫
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.apply_measure_as_distribution
Proof state before:
W : Type ?u.37841
inst✝¹² : NormedAddCommGroup W
inst✝¹¹ : NormedSpace ℝ W
inst✝¹⁰ : CompleteSpace W
X✝ : Type ?u.38068
inst✝⁹ : NormedAddCommGroup X✝
inst✝⁸ : NormedSpace ℝ X✝
inst✝⁷ : CompleteSpace X✝
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.38520
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
X : Type u_1
inst✝ : TopologicalSpace X
μ : Measure X
φ : X → Y
⊢ ⟪↑μ, φ⟫ = ∫ (x : X), φ x ∂μ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.action_is_integral
Proof state before:
W : Type ?u.38907
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : CompleteSpace W
X✝ : Type ?u.39134
inst✝¹⁰ : NormedAddCommGroup X✝
inst✝⁹ : NormedSpace ℝ X✝
inst✝⁸ : CompleteSpace X✝
Y✝ : Type ?u.39360
inst✝⁷ : NormedAddCommGroup Y✝
inst✝⁶ : NormedSpace ℝ Y✝
inst✝⁵ : CompleteSpace Y✝
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : CompleteSpace Z
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x : Measure X
f : X → Measure Y
φ : Y → Z
hφ : ∀ (x : X), Integrable φ (f x)
⊢ ⟪do
      let x ← ↑x
      ↑(f x), φ⟫ =
    ∫ (y : Y), φ y ∂Measure.bind x f
Tactic:
simp
Proof state after:
W : Type ?u.38907
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : CompleteSpace W
X✝ : Type ?u.39134
inst✝¹⁰ : NormedAddCommGroup X✝
inst✝⁹ : NormedSpace ℝ X✝
inst✝⁸ : CompleteSpace X✝
Y✝ : Type ?u.39360
inst✝⁷ : NormedAddCommGroup Y✝
inst✝⁶ : NormedSpace ℝ Y✝
inst✝⁵ : CompleteSpace Y✝
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : CompleteSpace Z
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x : Measure X
f : X → Measure Y
φ : Y → Z
hφ : ∀ (x : X), Integrable φ (f x)
⊢ ∫ (x' : X), ∫ (x : Y), φ x ∂f x' ∂x = ∫ (x : Y), φ x ∂Measure.bind x f
Theorem: SciLean.Prob.action_is_integral
Proof state before:
W : Type ?u.38907
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : CompleteSpace W
X✝ : Type ?u.39134
inst✝¹⁰ : NormedAddCommGroup X✝
inst✝⁹ : NormedSpace ℝ X✝
inst✝⁸ : CompleteSpace X✝
Y✝ : Type ?u.39360
inst✝⁷ : NormedAddCommGroup Y✝
inst✝⁶ : NormedSpace ℝ Y✝
inst✝⁵ : CompleteSpace Y✝
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : CompleteSpace Z
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x : Measure X
f : X → Measure Y
φ : Y → Z
hφ : ∀ (x : X), Integrable φ (f x)
⊢ ∫ (x' : X), ∫ (x : Y), φ x ∂f x' ∂x = ∫ (x : Y), φ x ∂Measure.bind x f
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.frontier_inter
Proof state before:
R : Type ?u.1691
inst✝⁷ : RealScalar R
W : Type ?u.1697
inst✝⁶ : SemiHilbert R W
X✝ : Type ?u.1724
inst✝⁵ : SemiHilbert R X✝
Y : Type ?u.1745
inst✝⁴ : SemiHilbert R Y
inst✝³ : Module ℝ Y
Z : Type ?u.2563
inst✝² : SemiHilbert R Z
inst✝¹ : Module ℝ Z
X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
hA : IsClosed A
hB : IsClosed B
⊢ frontier (A ∩ B) = frontier A ∩ B ∪ frontier B ∩ A
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.frontier_levelSet
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.3766
inst✝⁶ : SemiHilbert R W
X✝ : Type ?u.3793
inst✝⁵ : SemiHilbert R X✝
Y : Type ?u.3814
inst✝⁴ : SemiHilbert R Y
inst✝³ : Module ℝ Y
Z : Type ?u.4632
inst✝² : SemiHilbert R Z
inst✝¹ : Module ℝ Z
X : Type u_1
inst✝ : TopologicalSpace X
φ ψ : X → R
⊢ frontier {x | φ x ≤ ψ x} = {x | φ x = ψ x}
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.revDeriv_fst
Proof state before:
K : Type u_3
I : Type ?u.9289
inst✝²⁴ : RCLike K
X : Type u_2
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_1
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.9319
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.9330
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.9341
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.9366
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.9391
EI : I → Type ?u.9396
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.9530
J : Type ?u.9533
FJ : J → Type ?u.9538
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y
x : X
⊢ (revDeriv K f x).1 = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.revDeriv_snd_zero
Proof state before:
K : Type u_3
I : Type ?u.9802
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.9832
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.9843
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.9854
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.9879
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.9904
EI : I → Type ?u.9909
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.10043
J : Type ?u.10046
FJ : J → Type ?u.10051
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y
x : X
⊢ (revDeriv K f x).2 0 = 0
Tactic:
simp[revDeriv]
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate_fst
Proof state before:
K : Type u_3
I : Type ?u.11785
inst✝²⁴ : RCLike K
X : Type u_2
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_1
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.11815
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.11826
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.11837
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.11862
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.11887
EI : I → Type ?u.11892
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.12026
J : Type ?u.12029
FJ : J → Type ?u.12034
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y
x : X
⊢ (revDerivUpdate K f x).1 = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate_snd_zero
Proof state before:
K : Type u_3
I : Type ?u.12299
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.12329
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.12340
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.12351
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.12376
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.12401
EI : I → Type ?u.12406
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.12540
J : Type ?u.12543
FJ : J → Type ?u.12548
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y
x dx : X
⊢ (revDerivUpdate K f x).2 0 dx = dx
Tactic:
simp[revDerivUpdate]
Proof state after:
no goals
Theorem: SciLean.revDerivUpdate_snd_zero'
Proof state before:
K : Type u_3
I : Type ?u.14597
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type u_2
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.14627
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.14638
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.14649
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.14674
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type ?u.14699
EI : I → Type ?u.14704
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.14838
J : Type ?u.14841
FJ : J → Type ?u.14846
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → Y
x : X
dy : Y
⊢ (revDerivUpdate K f x).2 dy 0 = (revDeriv K f x).2 dy
Tactic:
simp[revDerivUpdate]
Proof state after:
no goals
Theorem: SciLean.revDerivProj_fst
Proof state before:
K : Type u_5
I : Type u_2
inst✝²⁴ : RCLike K
X : Type u_3
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.16947
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.16958
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.16969
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.16980
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.17005
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_1
EI : I → Type u_4
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.17169
J : Type ?u.17172
FJ : J → Type ?u.17177
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → E
x : X
⊢ (revDerivProj K I f x).1 = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.revDerivProj_snd_zero
Proof state before:
K : Type u_5
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.17636
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.17647
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.17658
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.17669
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.17694
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_2
EI : I → Type u_4
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.17858
J : Type ?u.17861
FJ : J → Type ?u.17866
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → E
x : X
i : I
⊢ (revDerivProj K I f x).2 i 0 = 0
Tactic:
simp[revDerivProj]
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate_fst
Proof state before:
K : Type u_5
I : Type u_2
inst✝²⁴ : RCLike K
X : Type u_3
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.20479
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.20490
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.20501
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.20512
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.20537
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_1
EI : I → Type u_4
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.20701
J : Type ?u.20704
FJ : J → Type ?u.20709
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → E
x : X
⊢ (revDerivProjUpdate K I f x).1 = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.revDerivProjUpdate_snd_zero
Proof state before:
K : Type u_5
I : Type u_3
inst✝²⁴ : RCLike K
X : Type u_1
inst✝²³ : SemiInnerProductSpace K X
Y : Type ?u.21154
inst✝²² : SemiInnerProductSpace K Y
Z : Type ?u.21165
inst✝²¹ : SemiInnerProductSpace K Z
W : Type ?u.21176
inst✝²⁰ : SemiInnerProductSpace K W
ι : Type ?u.21187
inst✝¹⁹ : IndexType ι
inst✝¹⁸ : LawfulIndexType ι
inst✝¹⁷ : DecidableEq ι
κ : Type ?u.21212
inst✝¹⁶ : IndexType κ
inst✝¹⁵ : LawfulIndexType κ
inst✝¹⁴ : DecidableEq κ
E : Type u_2
EI : I → Type u_4
inst✝¹³ : StructType E I EI
inst✝¹² : IndexType I
inst✝¹¹ : LawfulIndexType I
inst✝¹⁰ : DecidableEq I
inst✝⁹ : SemiInnerProductSpace K E
inst✝⁸ : (i : I) → SemiInnerProductSpace K (EI i)
inst✝⁷ : SemiInnerProductSpaceStruct K E I EI
F : Type ?u.21376
J : Type ?u.21379
FJ : J → Type ?u.21384
inst✝⁶ : StructType F J FJ
inst✝⁵ : IndexType J
inst✝⁴ : LawfulIndexType J
inst✝³ : DecidableEq J
inst✝² : SemiInnerProductSpace K F
inst✝¹ : (j : J) → SemiInnerProductSpace K (FJ j)
inst✝ : SemiInnerProductSpaceStruct K F J FJ
f : X → E
x dx : X
i : I
⊢ (revDerivProjUpdate K I f x).2 i 0 dx = dx
Tactic:
simp[revDerivProjUpdate]
Proof state after:
no goals