internlm/Lean-Github huggingface dataset:
Theorem: SciLean.toDistribution.arg_f.parDistribDeriv_rule
Proof state before:
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = fun w dw => ↑fun x => ∂ (x_1:=w;dw), f x_1 x
Tactic:
funext x dx
Proof state after:
case h.h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = ↑fun x_1 => ∂ (x:=x;dx), f x x_1
Theorem: SciLean.toDistribution.arg_f.parDistribDeriv_rule
Proof state before:
case h.h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) = ↑fun x_1 => ∂ (x:=x;dx), f x x_1
Tactic:
ext φ
Proof state after:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) φ = (↑fun x_1 => ∂ (x:=x;dx), f x x_1) φ
Theorem: SciLean.toDistribution.arg_f.parDistribDeriv_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) φ = (↑fun x_1 => ∂ (x:=x;dx), f x x_1) φ
Tactic:
simp[Function.toDistribution]
Proof state after:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ ∂ (x':=x;dx), ∫' x, φ x • f x' x = ∫' x_1, φ x_1 • ∂ (x:=x;dx), f x x_1
Theorem: SciLean.toDistribution.arg_f.parDistribDeriv_rule
Proof state before:
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ ∂ (x':=x;dx), ∫' x, φ x • f x' x = ∫' x_1, φ x_1 • ∂ (x:=x;dx), f x x_1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prob.fdaction_mk_apply
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.9959
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.10394
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
val dval : Distribution X
φ : X → W × W
⊢ ⟪{ val := val, dval := dval }, φ⟫ = (⟪val, fun x => (φ x).1⟫, ⟪dval, fun x => (φ x).1⟫ + ⟪val, fun x => (φ x).2⟫)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.fdaction_unfold
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.13448
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.13883
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f' : FDistribution X
φ : X → W × W
⊢ ⟪f', φ⟫ = (⟪f'.val, fun x => (φ x).1⟫, ⟪f'.dval, fun x => (φ x).1⟫ + ⟪f'.val, fun x => (φ x).2⟫)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Prob.distribFwdDeriv_const
Proof state before:
W : Type ?u.22303
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.23178
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.23613
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (distribFwdDeriv fun x => a) = fun w _dw => { val := a, dval := 0 }
Tactic:
unfold distribFwdDeriv
Proof state after:
W : Type ?u.22303
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.23178
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.23613
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { val := (fun x => a) x, dval := distribDeriv (fun x => a) x dx }) = fun w _dw => { val := a, dval := 0 }
Theorem: SciLean.Prob.distribFwdDeriv_const
Proof state before:
W : Type ?u.22303
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.23178
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.23613
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
α : Type u_1
a : Distribution α
⊢ (fun x dx => { val := (fun x => a) x, dval := distribDeriv (fun x => a) x dx }) = fun w _dw => { val := a, dval := 0 }
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.Prob.distribFwdDeriv_comp
Proof state before:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ⟪distribFwdDeriv (fun x => f (g x)) x dx, φ⟫ =
    let ydy := fwdFDeriv ℝ g x dx;
    ⟪distribFwdDeriv f ydy.1 ydy.2, φ⟫
Tactic:
simp (disch := assumption) only [action, distribFwdDeriv, fwdFDeriv]
Proof state after:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv (fun x => f (g x)) x dx).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2) =
    ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv f (g x) ((fderiv ℝ g x) dx)).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2)
Theorem: SciLean.Prob.distribFwdDeriv_comp
Proof state before:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv (fun x => f (g x)) x dx).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2) =
    ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv f (g x) ((fderiv ℝ g x) dx)).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2)
Tactic:
simp (disch := assumption) only [distribution_action_normalize, distribDeriv_comp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDistribution.bind.arg_xf.distribFwdDeriv_rule
Proof state before:
W : Type u_1
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_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪distribFwdDeriv (fun x' => g x' >>= f x') x dx, φ⟫ =
    ⟪distribFwdDeriv g x dx, fun y => ⟪distribFwdDeriv (fun x => f x y) x dx, φ⟫⟫
Tactic:
simp (disch := assumption)
  [distribFwdDeriv, fdaction_mk_apply, action_bind,
   Bind.bind.arg_xf.distribDeriv_rule, Prod.mk.injEq, true_and, add_assoc]
Proof state after:
W : Type u_1
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_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪g x, fun x' => ⟪distribDeriv (fun x => f x x') x dx, fun x => (φ x).1⟫⟫ +
      ⟪g x, fun x' => ⟪f x x', fun x => (φ x).2⟫⟫ =
    ⟪g x, fun x_1 => ⟪distribDeriv (fun x => f x x_1) x dx, fun x => (φ x).1⟫ + ⟪f x x_1, fun x => (φ x).2⟫⟫
Theorem: SciLean.Prob.FDistribution.bind.arg_xf.distribFwdDeriv_rule
Proof state before:
W : Type u_1
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_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪g x, fun x' => ⟪distribDeriv (fun x => f x x') x dx, fun x => (φ x).1⟫⟫ +
      ⟪g x, fun x' => ⟪f x x', fun x => (φ x).2⟫⟫ =
    ⟪g x, fun x_1 => ⟪distribDeriv (fun x => f x x_1) x dx, fun x => (φ x).1⟫ + ⟪f x x_1, fun x => (φ x).2⟫⟫
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.Prob.ite.arg_te.distribFwdDeriv_rule
Proof state before:
W : Type u_1
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_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.40686
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
x dx : X
c : Prop
inst✝ : Decidable c
t e : X → Distribution Y
φ : Y → W × W
⊢ ⟪distribFwdDeriv (fun x => if c then t x else e x) x dx, φ⟫ =
    if c then ⟪distribFwdDeriv t x dx, φ⟫ else ⟪distribFwdDeriv e x dx, φ⟫
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Prob.ite.arg_te.distribFwdDeriv_rule
Proof state before:
W : Type u_1
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_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.40686
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
x dx : X
c : Prop
inst✝ : Decidable c
t e : X → Distribution Y
φ : Y → W × W
h : c
⊢ ⟪distribFwdDeriv (fun x => if c then t x else e x) x dx, φ⟫ =
    if c then ⟪distribFwdDeriv t x dx, φ⟫ else ⟪distribFwdDeriv e x dx, φ⟫
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Prob.ite.arg_te.distribFwdDeriv_rule
Proof state before:
W : Type u_1
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_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : CompleteSpace Y
Z : Type ?u.40686
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : CompleteSpace Z
x dx : X
c : Prop
inst✝ : Decidable c
t e : X → Distribution Y
φ : Y → W × W
h : ¬c
⊢ ⟪distribFwdDeriv (fun x => if c then t x else e x) x dx, φ⟫ =
    if c then ⟪distribFwdDeriv t x dx, φ⟫ else ⟪distribFwdDeriv e x dx, φ⟫
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.AutoImpl.impl_eq_spec
Proof state before:
α✝ : Type u_1
a : α✝
x : AutoImpl a
⊢ a = val x
Tactic:
cases x
Proof state after:
case exact
α✝ : Type u_1
a a✝ : α✝
h✝ : a✝ = a
⊢ a = val (AutoExactSolution.exact a✝ h✝)
Theorem: SciLean.AutoImpl.impl_eq_spec
Proof state before:
case exact
α✝ : Type u_1
a a✝ : α✝
h✝ : a✝ = a
⊢ a = val (AutoExactSolution.exact a✝ h✝)
Tactic:
rename_i a' h
Proof state after:
case exact
α✝ : Type u_1
a a' : α✝
h : a' = a
⊢ a = val (AutoExactSolution.exact a' h)
Theorem: SciLean.AutoImpl.impl_eq_spec
Proof state before:
case exact
α✝ : Type u_1
a a' : α✝
h : a' = a
⊢ a = val (AutoExactSolution.exact a' h)
Tactic:
simp[AutoImpl.val, val, h]
Proof state after:
no goals
Theorem: SciLean.AutoImpl.normalize_val
Proof state before:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ val (Eq.mpr h finish) = b
Tactic:
have h' : a = b := by apply AutoImpl.injectivity_axiom; apply h
Proof state after:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
h' : a = b
⊢ val (Eq.mpr h finish) = b
Theorem: SciLean.AutoImpl.normalize_val
Proof state before:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
h' : a = b
⊢ val (Eq.mpr h finish) = b
Tactic:
revert h
Proof state after:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl a = AutoImpl b), val (Eq.mpr h finish) = b
Theorem: SciLean.AutoImpl.normalize_val
Proof state before:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl a = AutoImpl b), val (Eq.mpr h finish) = b
Tactic:
rw[h']
Proof state after:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl b = AutoImpl b), val (Eq.mpr h finish) = b
Theorem: SciLean.AutoImpl.normalize_val
Proof state before:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl b = AutoImpl b), val (Eq.mpr h finish) = b
Tactic:
simp[val,finish,Eq.mpr]
Proof state after:
no goals
Theorem: SciLean.AutoImpl.normalize_val
Proof state before:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ a = b
Tactic:
apply AutoImpl.injectivity_axiom
Proof state after:
case a
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ AutoImpl a = AutoImpl b
Theorem: SciLean.AutoImpl.normalize_val
Proof state before:
case a
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ AutoImpl a = AutoImpl b
Tactic:
apply h
Proof state after:
no goals
Theorem: SciLean.fderiv.id_rule
Proof state before:
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.754
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.889
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.1024
inst✝² : Fintype ι
E : ι → Type ?u.1032
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
⊢ (fderiv K fun x => x) = fun x => fun dx =>L[K] dx
Tactic:
ext x dx
Proof state after:
case h.h
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.754
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.889
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.1024
inst✝² : Fintype ι
E : ι → Type ?u.1032
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x dx : X
⊢ (fderiv K (fun x => x) x) dx = (fun dx =>L[K] dx) dx
Theorem: SciLean.fderiv.id_rule
Proof state before:
case h.h
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.754
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.889
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.1024
inst✝² : Fintype ι
E : ι → Type ?u.1032
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x dx : X
⊢ (fderiv K (fun x => x) x) dx = (fun dx =>L[K] dx) dx
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.fderiv.const_rule
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.9160
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.9295
inst✝² : Fintype ι
E : ι → Type ?u.9303
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x : X
⊢ (fderiv K fun x_1 => x) = fun x => fun x =>L[K] 0
Tactic:
ext x dx
Proof state after:
case h.h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.9160
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.9295
inst✝² : Fintype ι
E : ι → Type ?u.9303
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x✝ : X
x dx : Y
⊢ (fderiv K (fun x => x✝) x) dx = (fun x =>L[K] 0) dx
Theorem: SciLean.fderiv.const_rule
Proof state before:
case h.h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.9160
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.9295
inst✝² : Fintype ι
E : ι → Type ?u.9303
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x✝ : X
x dx : Y
⊢ (fderiv K (fun x => x✝) x) dx = (fun x =>L[K] 0) dx
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.fderiv.apply_rule
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.25663
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.25805
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.25940
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
i : ι
⊢ (fderiv K fun x => x i) = fun x => fun dx =>L[K] dx i
Tactic:
funext x
Proof state after:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.25663
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.25805
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.25940
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
i : ι
x : (i : ι) → E i
⊢ fderiv K (fun x => x i) x = fun dx =>L[K] dx i
Theorem: SciLean.fderiv.apply_rule
Proof state before:
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type ?u.25663
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type ?u.25805
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.25940
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type u_1
inst✝² : Fintype ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
i : ι
x : (i : ι) → E i
⊢ fderiv K (fun x => x i) x = fun dx =>L[K] dx i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.fderiv.comp_rule_at
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ fderiv K (fun x => f (g x)) x =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K f y) dy;
      dz
Tactic:
rw[show (fun x => f (g x)) = f ∘ g by rfl]
Proof state after:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ fderiv K (f ∘ g) x =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K f y) dy;
      dz
Theorem: SciLean.fderiv.comp_rule_at
Proof state before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ fderiv K (f ∘ g) x =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K f y) dy;
      dz
Tactic:
rw[fderiv.comp x hf hg]
Proof state after:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_4
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.41811
inst✝² : Fintype ι
E : ι → Type ?u.41819
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : Y → Z
g : X → Y
x : X
hf : DifferentiableAt K f (g x)
hg : DifferentiableAt K g x
⊢ ContinuousLinearMap.comp (fderiv K f (g x)) (fderiv K g x) =
    let y := g x;
    fun dx =>L[K]
      let dy := (fderiv K g x) dx;
      let dz := (fderiv K f y) dy;
      dz