internlm/Lean-Github huggingface dataset:
Theorem: Float3.x.as_struct_modify
Proof state before:
f : Float → Float
v : Float3
⊢ { x := f v.x, y := v.y, z := v.z } = structModify (Sum.inl ()) f v
Tactic:
rfl
Proof state after:
no goals
Theorem: Float3.y.as_struct_proj
Proof state before:
⊢ y = fun v => structProj v (Sum.inr (Sum.inl ()))
Tactic:
rfl
Proof state after:
no goals
Theorem: Float3.y.as_struct_modify
Proof state before:
f : Float → Float
v : Float3
⊢ { x := v.x, y := f v.y, z := v.z } = structModify (Sum.inr (Sum.inl ())) f v
Tactic:
rfl
Proof state after:
no goals
Theorem: Float3.z.as_struct_proj
Proof state before:
⊢ z = fun v => structProj v (Sum.inr (Sum.inr ()))
Tactic:
rfl
Proof state after:
no goals
Theorem: Float3.z.as_struct_modify
Proof state before:
f : Float → Float
v : Float3
⊢ { x := v.x, y := v.y, z := f v.z } = structModify (Sum.inr (Sum.inr ())) f v
Tactic:
rfl
Proof state after:
no goals
Theorem: Float3.mk.as_struct_make
Proof state before:
f : (i : Unit ⊕ Unit ⊕ Unit) → Sum.rec (fun x => Float) (fun t => Sum.rec (fun x => Float) (fun x => Float) t) i
⊢ { x := f (Sum.inl ()), y := f (Sum.inr (Sum.inl ())), z := f (Sum.inr (Sum.inr ())) } = structMake f
Tactic:
rfl
Proof state after:
no goals
Theorem: Float3.x.arg_self.IsLinearMap_rule
Proof state before:
⊢ IsLinearMap Float fun v => v.x
Tactic:
rw[Float3.x.as_struct_proj]
Proof state after:
⊢ IsLinearMap Float fun v => (fun v => structProj v (Sum.inl ())) v
Theorem: Float3.x.arg_self.IsLinearMap_rule
Proof state before:
⊢ IsLinearMap Float fun v => (fun v => structProj v (Sum.inl ())) v
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Float3.x.arg_self.CDifferentiable_rule
Proof state before:
⊢ CDifferentiable Float fun v => v.x
Tactic:
rw[Float3.x.as_struct_proj]
Proof state after:
⊢ CDifferentiable Float fun v => (fun v => structProj v (Sum.inl ())) v
Theorem: Float3.x.arg_self.CDifferentiable_rule
Proof state before:
⊢ CDifferentiable Float fun v => (fun v => structProj v (Sum.inl ())) v
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Float3.x.arg_self.IsSmoothLinearMap_rule
Proof state before:
⊢ IsSmoothLinearMap Float fun v => v.x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: Float3.x.arg_self.HasSemiAdjoint_rule
Proof state before:
⊢ HasSemiAdjoint Float fun v => v.x
Tactic:
rw[Float3.x.as_struct_proj]
Proof state after:
⊢ HasSemiAdjoint Float fun v => (fun v => structProj v (Sum.inl ())) v
Theorem: Float3.x.arg_self.HasSemiAdjoint_rule
Proof state before:
⊢ HasSemiAdjoint Float fun v => (fun v => structProj v (Sum.inl ())) v
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
⊢ HasAdjDiff Float fun v => v.x
Tactic:
intro x
Proof state after:
x : Float3
⊢ HasAdjDiffAt Float (fun v => v.x) x
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
x : Float3
⊢ HasAdjDiffAt Float (fun v => v.x) x
Tactic:
constructor
Proof state after:
case left
x : Float3
⊢ CDifferentiableAt Float (fun v => v.x) x

case right
x : Float3
⊢ HasSemiAdjoint Float (∂ (v:=x), v.x)
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
case left
x : Float3
⊢ CDifferentiableAt Float (fun v => v.x) x

case right
x : Float3
⊢ HasSemiAdjoint Float (∂ (v:=x), v.x)
Tactic:
. fun_prop
Proof state after:
case right
x : Float3
⊢ HasSemiAdjoint Float (∂ (v:=x), v.x)
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
case right
x : Float3
⊢ HasSemiAdjoint Float (∂ (v:=x), v.x)
Tactic:
. fun_trans; fun_prop
Proof state after:
no goals
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
case left
x : Float3
⊢ CDifferentiableAt Float (fun v => v.x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
case right
x : Float3
⊢ HasSemiAdjoint Float (∂ (v:=x), v.x)
Tactic:
fun_trans
Proof state after:
case right
x : Float3
⊢ HasSemiAdjoint Float fun dx => dx.x
Theorem: Float3.x.arg_self.HasAdjDiff_rule
Proof state before:
case right
x : Float3
⊢ HasSemiAdjoint Float fun dx => dx.x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.jacobian.comp_rule
Proof state before:
R : Type u_1
inst✝³ : RealScalar R
U : Type u_2
inst✝² : SemiHilbert R U
V : Type u_3
inst✝¹ : SemiHilbert R V
W : Type ?u.33364
inst✝ : SemiHilbert R W
f : U → V
g : U → U
hf : HasAdjDiff R f
hg : HasAdjDiff R g
⊢ (jacobian R fun x => f (g x)) = fun x => jacobian R f x * jacobian R g x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.split_integral_over_set_of_ite
Proof state before:
R : Type u_3
inst✝⁶ : RealScalar R
inst✝⁵ : DecidableRel fun x x_1 => x ≤ x_1
X : Type u_1
inst✝⁴ : MeasureSpace X
Y : Type u_2
inst✝³ : AddCommGroup Y
inst✝² : _root_.Module ℝ Y
Z : Type ?u.77184
inst✝¹ : AddCommGroup Z
inst✝ : _root_.Module ℝ Z
φ ψ : X → R
f g : X → Y
A : Set X
⊢ ∫' x, if ψ x ≤ φ x then f x else g x ∂volume.restrict A =
    ∫' x, f x ∂volume.restrict ({x' | 0 ≤ φ x' - ψ x'} ∩ A) + ∫' x, g x ∂volume.restrict ({x' | 0 ≤ ψ x' - φ x'} ∩ A)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cintegral.arg_f.CDifferentiable_rule
Proof state before:
α : Type ?u.82209
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.82883
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ CDifferentiable R fun x => ∫' y, f x y ∂μ
Tactic:
have := hf
Proof state after:
α : Type ?u.82209
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.82883
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf this : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ CDifferentiable R fun x => ∫' y, f x y ∂μ
Theorem: SciLean.cintegral.arg_f.CDifferentiable_rule
Proof state before:
α : Type ?u.82209
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.82883
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf this : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ CDifferentiable R fun x => ∫' y, f x y ∂μ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cintegral.arg_f.cderiv_rule
Proof state before:
α : Type ?u.84708
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.85382
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (y : β), CDifferentiable R fun x => f x y
⊢ (cderiv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, cderiv R (fun x => f x y) x dx ∂μ
Tactic:
have := hf
Proof state after:
α : Type ?u.84708
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.85382
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf this : ∀ (y : β), CDifferentiable R fun x => f x y
⊢ (cderiv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, cderiv R (fun x => f x y) x dx ∂μ
Theorem: SciLean.cintegral.arg_f.cderiv_rule
Proof state before:
α : Type ?u.84708
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.85382
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf this : ∀ (y : β), CDifferentiable R fun x => f x y
⊢ (cderiv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, cderiv R (fun x => f x y) x dx ∂μ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cintegral.arg_f.fwdDeriv_rule
Proof state before:
α : Type ?u.87292
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.87966
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ (fwdDeriv R fun x => ∫' y, f x y ∂μ) = fun x dx => ∫' y, fwdDeriv R (fun x => f x y) x dx ∂μ
Tactic:
unfold fwdDeriv
Proof state after:
α : Type ?u.87292
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.87966
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => ((fun x => ∫' y, f x y ∂μ) x, cderiv R (fun x => ∫' y, f x y ∂μ) x dx)) = fun x dx =>
    ∫' y, ((fun x => f x y) x, cderiv R (fun x => f x y) x dx) ∂μ
Theorem: SciLean.cintegral.arg_f.fwdDeriv_rule
Proof state before:
α : Type ?u.87292
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.87966
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (x : β), CDifferentiable R fun x_1 => f x_1 x
⊢ (fun x dx => ((fun x => ∫' y, f x y ∂μ) x, cderiv R (fun x => ∫' y, f x y ∂μ) x dx)) = fun x dx =>
    ∫' y, ((fun x => f x y) x, cderiv R (fun x => f x y) x dx) ∂μ
Tactic:
fun_trans [cintegral_prod_mk]
Proof state after:
no goals
Theorem: SciLean.cintegral.arg_f.IsLinearMap_rule
Proof state before:
α : Type ?u.96092
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.96766
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (y : β), IsLinearMap R fun x => f x y
⊢ IsLinearMap R fun x => ∫' y, f x y ∂μ
Tactic:
have := hf
Proof state after:
α : Type ?u.96092
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.96766
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf this : ∀ (y : β), IsLinearMap R fun x => f x y
⊢ IsLinearMap R fun x => ∫' y, f x y ∂μ
Theorem: SciLean.cintegral.arg_f.IsLinearMap_rule
Proof state before:
α : Type ?u.96092
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.96766
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf this : ∀ (y : β), IsLinearMap R fun x => f x y
⊢ IsLinearMap R fun x => ∫' y, f x y ∂μ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cintegral.arg_f.IsSmoothLinearMap_rule
Proof state before:
α : Type ?u.99883
inst✝⁸ : MeasurableSpace α
β : Type u_1
inst✝⁷ : MeasurableSpace β
R : Type u_2
inst✝⁶ : RCLike R
X : Type u_3
inst✝⁵ : Vec R X
inst✝⁴ : _root_.Module ℝ X
Y : Type ?u.100557
inst✝³ : Vec R Y
inst✝² : _root_.Module ℝ Y
Z : Type u_4
inst✝¹ : Vec R Z
inst✝ : _root_.Module ℝ Z
f : X → β → Z
μ : Measure β
hf : ∀ (y : β), IsSmoothLinearMap R fun x => f x y
⊢ IsSmoothLinearMap R fun x => ∫' y, f x y ∂μ
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.scalar_abs_one
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ Scalar.abs 1 = 1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_abs_zero
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ Scalar.abs 0 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_abs_neg
Proof state before:
R : Type u_1
inst✝ : RealScalar R
r : R
⊢ Scalar.abs (-r) = Scalar.abs r
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_div_one
Proof state before:
R : Type u_1
inst✝ : RealScalar R
x : R
⊢ x / 1 = x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_sqrt_one
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ Scalar.sqrt 1 = 1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_sqrt_zero
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ Scalar.sqrt 0 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_max_one_zero
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ max 1 0 = 1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_max_zero_one
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ max 0 1 = 1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_min_one_zero
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ min 1 0 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.scalar_min_zero_one
Proof state before:
R : Type u_1
inst✝ : RealScalar R
⊢ min 0 1 = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Scalar.ofReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : ℝ
⊢ ofReal R (if c then t else e) = if c then ofReal R t else ofReal R e
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : ℝ
h : c
⊢ ofReal R (if c then t else e) = if c then ofReal R t else ofReal R e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : ℝ
h : ¬c
⊢ ofReal R (if c then t else e) = if c then ofReal R t else ofReal R e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ℝ
e : ¬c → ℝ
⊢ ofReal R (if h : c then t h else e h) = if h : c then ofReal R (t h) else ofReal R (e h)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ℝ
e : ¬c → ℝ
h : c
⊢ ofReal R (if h : c then t h else e h) = if h : c then ofReal R (t h) else ofReal R (e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ℝ
e : ¬c → ℝ
h : ¬c
⊢ ofReal R (if h : c then t h else e h) = if h : c then ofReal R (t h) else ofReal R (e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : R
⊢ toReal R (if c then t else e) = if c then toReal R t else toReal R e
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : R
h : c
⊢ toReal R (if c then t else e) = if c then toReal R t else toReal R e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : R
h : ¬c
⊢ toReal R (if c then t else e) = if c then toReal R t else toReal R e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → R
e : ¬c → R
⊢ toReal R (if h : c then t h else e h) = if h : c then toReal R (t h) else toReal R (e h)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → R
e : ¬c → R
h : c
⊢ toReal R (if h : c then t h else e h) = if h : c then toReal R (t h) else toReal R (e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → R
e : ¬c → R
h : ¬c
⊢ toReal R (if h : c then t h else e h) = if h : c then toReal R (t h) else toReal R (e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofENNReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : ENNReal
⊢ ↑(if c then t else e) = if c then ↑t else ↑e
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofENNReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : ENNReal
h : c
⊢ ↑(if c then t else e) = if c then ↑t else ↑e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofENNReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : ENNReal
h : ¬c
⊢ ↑(if c then t else e) = if c then ↑t else ↑e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofENNReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ENNReal
e : ¬c → ENNReal
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofENNReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ENNReal
e : ¬c → ENNReal
h : c
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.ofENNReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → ENNReal
e : ¬c → ENNReal
h : ¬c
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toENNReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : R
⊢ ↑(if c then t else e) = if c then ↑t else ↑e
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toENNReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : R
h : c
⊢ ↑(if c then t else e) = if c then ↑t else ↑e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toENNReal_ite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t e : R
h : ¬c
⊢ ↑(if c then t else e) = if c then ↑t else ↑e
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toENNReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → R
e : ¬c → R
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toENNReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → R
e : ¬c → R
h : c
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.Scalar.toENNReal_dite
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
c : Prop
inst✝ : Decidable c
t : c → R
e : ¬c → R
h : ¬c
⊢ ↑(if h : c then t h else e h) = if h : c then ↑(t h) else ↑(e h)
Tactic:
simp[h]
Proof state after:
no goals
Theorem: ListN.add_elemwise
Proof state before:
α : Type u_1
n : Nat
inst✝ : Add α
x y : α
xs ys : ListN α n
⊢ cons x xs + cons y ys = cons (x + y) (xs + ys)
Tactic:
rfl
Proof state after:
no goals
Theorem: ListN.sub_elemwise
Proof state before:
α : Type u_1
n : Nat
inst✝ : Sub α
x y : α
xs ys : ListN α n
⊢ cons x xs - cons y ys = cons (x - y) (xs - ys)
Tactic:
rfl
Proof state after:
no goals
Theorem: ListN.mul_elemwise
Proof state before:
α : Type u_1
n : Nat
inst✝ : Mul α
x y : α
xs ys : ListN α n
⊢ cons x xs * cons y ys = cons (x * y) (xs * ys)
Tactic:
rfl
Proof state after:
no goals
Theorem: ListN.div_elemwise
Proof state before:
α : Type u_1
n : Nat
inst✝ : Div α
x y : α
xs ys : ListN α n
⊢ cons x xs / cons y ys = cons (x / y) (xs / ys)
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Scalar.exp.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.737
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fwdDeriv C fun w => exp (x w)) = fun w dw =>
    let xdx := fwdDeriv C x w dw;
    let e := exp xdx.1;
    (e, xdx.2 * e)
Tactic:
unfold fwdDeriv
Proof state after:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.737
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => exp (x w)) x_1, cderiv C (fun w => exp (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let e := exp xdx.1;
    (e, xdx.2 * e)
Theorem: SciLean.Scalar.exp.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.737
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => exp (x w)) x_1, cderiv C (fun w => exp (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let e := exp xdx.1;
    (e, xdx.2 * e)
Tactic:
fun_trans
Proof state after:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.737
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (exp (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * exp (fwdDeriv C (fun w => x w) x_1 dx).1)) =
    fun w dw => (exp (x w), cderiv C x w dw * exp (x w))
Theorem: SciLean.Scalar.exp.arg_x.fwdDeriv_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.737
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (exp (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * exp (fwdDeriv C (fun w => x w) x_1 dx).1)) =
    fun w dw => (exp (x w), cderiv C x w dw * exp (x w))
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Scalar.exp.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ HasAdjDiff C fun u => exp (x u)
Tactic:
intro x
Proof state after:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => exp (x✝ u)) x
Theorem: SciLean.Scalar.exp.arg_x.HasAdjDiff_rule
Proof state before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => exp (x✝ u)) x
Tactic:
constructor
Proof state after:
case left
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => exp (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.3145
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => exp (x✝ u)) x)