internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.FDRand.fdpure_fdE
Proof state before:
R : Type ?u.18889
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ fdE (fdpure x dx) φ = (φ x, (fderiv ℝ φ x) dx)
Tactic:
simp (disch:=sorry) only [fdpure,fdE,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_fdE
Proof state before:
R : Type ?u.20309
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
f : X → FDRand Y
φ : Y → Z
⊢ fdE (bind x f) φ = fdE' x fun x' => fdE (f x') φ
Tactic:
simp (disch:=sorry) only [bind,fdpure,fdE,fdE',rand_simp,rand_push_E]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_fdE'
Proof state before:
R : Type ?u.22079
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
f : X → FDRand Y
φ : Y → Z × Z
⊢ fdE' (bind x f) φ = fdE' x fun x' => fdE' (f x') φ
Tactic:
simp (disch:=sorry) only [bind,fdpure,fdE,fdE',rand_simp,rand_push_E,add_assoc]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.FDRand_mk_zero_fdE
Proof state before:
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ fdE { val := x, dval := 0 } φ = (E x φ, 0)
Tactic:
simp [fdE,DRand.dE]
Proof state after:
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ testFunctionExtension 0.action φ = 0
Theorem: SciLean.Prob.FDRand.FDRand_mk_zero_fdE
Proof state before:
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ testFunctionExtension 0.action φ = 0
Tactic:
apply testFunctionExtension_ext
Proof state after:
case h
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ ∀ (φ : X → ℝ) (y : X), 0.action φ • y = 0
Theorem: SciLean.Prob.FDRand.FDRand_mk_zero_fdE
Proof state before:
case h
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ ∀ (φ : X → ℝ) (y : X), 0.action φ • y = 0
Tactic:
intro _ _
Proof state after:
case h
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
φ✝ : X → ℝ
y✝ : X
⊢ 0.action φ✝ • y✝ = 0
Theorem: SciLean.Prob.FDRand.FDRand_mk_zero_fdE
Proof state before:
case h
R : Type ?u.24869
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
φ✝ : X → ℝ
y✝ : X
⊢ 0.action φ✝ • y✝ = 0
Tactic:
simp [rand_simp,zero_smul]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.FDRand_mk_fdE
Proof state before:
R : Type ?u.28335
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : Rand X
dx : DRand X
φ : X → Y
⊢ fdE { val := x, dval := dx } φ = (E x φ, DRand.dE dx φ)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.expectedValueAndChange_as_fdmean
Proof state before:
R : Type ?u.45469
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
φ : X → Y
⊢ fdE x φ =
    fdmean
      (let x' ~~ x
      fdpure (φ x') 0)
Tactic:
simp (disch:=sorry) only [rand_simp,mean,fdE,fdmean,bind,fdpure,id]
Proof state after:
R : Type ?u.45469
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
φ : X → Y
⊢ (E x.val φ, DRand.dE x.dval φ) =
    (E
        (let x' ~ x.val
        Rand.pure (φ x'))
        id,
      (DRand.dE x.dval fun x' => φ x') + E x.val fun x' => (fderiv ℝ id (φ x')) 0)
Theorem: SciLean.Prob.FDRand.expectedValueAndChange_as_fdmean
Proof state before:
R : Type ?u.45469
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 Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
φ : X → Y
⊢ (E x.val φ, DRand.dE x.dval φ) =
    (E
        (let x' ~ x.val
        Rand.pure (φ x'))
        id,
      (DRand.dE x.dval fun x' => φ x') + E x.val fun x' => (fderiv ℝ id (φ x')) 0)
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.Prob.distribDeriv_const
Proof state before:
W : Type ?u.3082
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (distribDeriv fun x => a) = fun w dw => 0
Tactic:
unfold distribDeriv
Proof state after:
W : Type ?u.3082
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx =>
      {
        action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ =>
          (fderiv ℝ (fun x => ⟪(fun x => a) x, φ⟫) x) dx }) =
    fun w dw => 0
Theorem: SciLean.Prob.distribDeriv_const
Proof state before:
W : Type ?u.3082
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx =>
      {
        action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ =>
          (fderiv ℝ (fun x => ⟪(fun x => a) x, φ⟫) x) dx }) =
    fun w dw => 0
Tactic:
simp
Proof state after:
W : Type ?u.3082
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ => 0 }) = fun w dw => 0
Theorem: SciLean.Prob.distribDeriv_const
Proof state before:
W : Type ?u.3082
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.3535
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.3761
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] φ => 0 }) = fun w dw => 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Prod.fst.arg_self.isomorph_rule
Proof state before:
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
⊢ (isomorph `RealToFloat fun x => (f x).1) = fun x => (isomorph `RealToFloat f x).1
Tactic:
funext x
Proof state after:
case h
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ isomorph `RealToFloat (fun x => (f x).1) x = (isomorph `RealToFloat f x).1
Theorem: Prod.fst.arg_self.isomorph_rule
Proof state before:
case h
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ isomorph `RealToFloat (fun x => (f x).1) x = (isomorph `RealToFloat f x).1
Tactic:
unfold isomorph
Proof state after:
case h
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ (IsomorphicType.equiv `RealToFloat) ((fun x => (f x).1) ((IsomorphicType.equiv `RealToFloat).symm x)) =
    ((IsomorphicType.equiv `RealToFloat) (f ((IsomorphicType.equiv `RealToFloat).symm x))).1
Theorem: Prod.fst.arg_self.isomorph_rule
Proof state before:
case h
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ (IsomorphicType.equiv `RealToFloat) ((fun x => (f x).1) ((IsomorphicType.equiv `RealToFloat).symm x)) =
    ((IsomorphicType.equiv `RealToFloat) (f ((IsomorphicType.equiv `RealToFloat).symm x))).1
Tactic:
unfold IsomorphicType.equiv
Proof state after:
case h
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ inst✝¹.1 ((fun x => (f x).1) (inst✝².1.symm x)) =
    ({
            equiv :=
              {
                toFun := fun x =>
                  match x with
                  | (a, b) => (inst✝¹.1 a, inst✝.1 b),
                invFun := fun x =>
                  match x with
                  | (a', b') => (inst✝¹.1.symm a', inst✝.1.symm b'),
                left_inv := ⋯, right_inv := ⋯ } }.1
        (f (inst✝².1.symm x))).1
Theorem: Prod.fst.arg_self.isomorph_rule
Proof state before:
case h
α✝ : Type ?u.1407
α'✝ : Type ?u.1410
β : Type ?u.1413
β' : Type ?u.1416
γ : Type ?u.1419
γ' : Type ?u.1422
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ inst✝¹.1 ((fun x => (f x).1) (inst✝².1.symm x)) =
    ({
            equiv :=
              {
                toFun := fun x =>
                  match x with
                  | (a, b) => (inst✝¹.1 a, inst✝.1 b),
                invFun := fun x =>
                  match x with
                  | (a', b') => (inst✝¹.1.symm a', inst✝.1.symm b'),
                left_inv := ⋯, right_inv := ⋯ } }.1
        (f (inst✝².1.symm x))).1
Tactic:
simp
Proof state after:
no goals
Theorem: Prod.snd.arg_self.isomorph_rule
Proof state before:
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
⊢ (isomorph `RealToFloat fun x => (f x).2) = fun x => (isomorph `RealToFloat f x).2
Tactic:
funext x
Proof state after:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ isomorph `RealToFloat (fun x => (f x).2) x = (isomorph `RealToFloat f x).2
Theorem: Prod.snd.arg_self.isomorph_rule
Proof state before:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ isomorph `RealToFloat (fun x => (f x).2) x = (isomorph `RealToFloat f x).2
Tactic:
unfold isomorph
Proof state after:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ (IsomorphicType.equiv `RealToFloat) ((fun x => (f x).2) ((IsomorphicType.equiv `RealToFloat).symm x)) =
    ((IsomorphicType.equiv `RealToFloat) (f ((IsomorphicType.equiv `RealToFloat).symm x))).2
Theorem: Prod.snd.arg_self.isomorph_rule
Proof state before:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ (IsomorphicType.equiv `RealToFloat) ((fun x => (f x).2) ((IsomorphicType.equiv `RealToFloat).symm x)) =
    ((IsomorphicType.equiv `RealToFloat) (f ((IsomorphicType.equiv `RealToFloat).symm x))).2
Tactic:
unfold IsomorphicType.equiv
Proof state after:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ inst✝.1 ((fun x => (f x).2) (inst✝².1.symm x)) =
    ({
            equiv :=
              {
                toFun := fun x =>
                  match x with
                  | (a, b) => (inst✝¹.1 a, inst✝.1 b),
                invFun := fun x =>
                  match x with
                  | (a', b') => (inst✝¹.1.symm a', inst✝.1.symm b'),
                left_inv := ⋯, right_inv := ⋯ } }.1
        (f (inst✝².1.symm x))).2
Theorem: Prod.snd.arg_self.isomorph_rule
Proof state before:
case h
α✝ : Type ?u.9557
α'✝ : Type ?u.9560
β : Type ?u.9563
β' : Type ?u.9566
γ : Type ?u.9569
γ' : Type ?u.9572
inst✝⁵ : IsomorphicType `RealToFloat α✝ α'✝
inst✝⁴ : IsomorphicType `RealToFloat β β'
inst✝³ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
α' : Type u_2
β₁ : Type u_3
β₂ : Type u_4
β₁' : Type u_5
β₂' : Type u_6
inst✝² : IsomorphicType `RealToFloat α α'
inst✝¹ : IsomorphicType `RealToFloat β₁ β₁'
inst✝ : IsomorphicType `RealToFloat β₂ β₂'
f : α → β₁ × β₂
x : α'
⊢ inst✝.1 ((fun x => (f x).2) (inst✝².1.symm x)) =
    ({
            equiv :=
              {
                toFun := fun x =>
                  match x with
                  | (a, b) => (inst✝¹.1 a, inst✝.1 b),
                invFun := fun x =>
                  match x with
                  | (a', b') => (inst✝¹.1.symm a', inst✝.1.symm b'),
                left_inv := ⋯, right_inv := ⋯ } }.1
        (f (inst✝².1.symm x))).2
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.cderiv.arg_dx.hasSemiAdjoint
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.1534
inst✝⁴ : SemiInnerProductSpace K Z
ι : Type ?u.1545
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.1572
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : X → Y
x : X
hf : HasAdjDiff K f
⊢ HasSemiAdjoint K (cderiv K f x)
Tactic:
fun_prop
Proof state after:
no goals