internlm/Lean-Github huggingface dataset:
Theorem: Int.two_not_cube
Proof state before:
r : ℤ
H : r ^ 3 = 2
⊢ False
Tactic:
apply two_not_cube r.natAbs
Proof state after:
r : ℤ
H : r ^ 3 = 2
⊢ r.natAbs ^ 3 = 2
Theorem: Int.two_not_cube
Proof state before:
r : ℤ
H : r ^ 3 = 2
⊢ r.natAbs ^ 3 = 2
Tactic:
rw [← Int.natAbs_pow, H]
Proof state after:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs 2 = 2
Theorem: Int.two_not_cube
Proof state before:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs 2 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: IndexType.card_sum
Proof state before:
ι✝ : Type v
inst✝² : IndexType ι✝
ι : Type u_1
κ : Type u_2
inst✝¹ : IndexType ι
inst✝ : IndexType κ
⊢ card (ι ⊕ κ) = card ι + card κ
Tactic:
rfl
Proof state after:
no goals
Theorem: IndexType.card_prod
Proof state before:
ι✝ : Type v
inst✝² : IndexType ι✝
ι : Type u_1
κ : Type u_2
inst✝¹ : IndexType ι
inst✝ : IndexType κ
⊢ card (ι × κ) = card ι * card κ
Tactic:
rfl
Proof state after:
no goals
Theorem: IndexType.card_unit
Proof state before:
ι : Type v
inst✝ : IndexType ι
⊢ card Unit = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: IndexType.sum_linearize
Proof state before:
ι : Type v
inst✝⁴ : IndexType ι
I : Type u_1
X : Type u_2
inst✝³ : Add X
inst✝² : Zero X
inst✝¹ : IndexType I
inst✝ : LawfulIndexType I
f : I → X
⊢  ∑ i, f i = ∑ i, f (fromFin i)
Tactic:
simp only [sum]
Proof state after:
ι : Type v
inst✝⁴ : IndexType ι
I : Type u_1
X : Type u_2
inst✝³ : Add X
inst✝² : Zero X
inst✝¹ : IndexType I
inst✝ : LawfulIndexType I
f : I → X
⊢ fold (IndexType.univ I) (fun s i => s + f i) 0 = fold (IndexType.univ (Fin (card I))) (fun s i => s + f (fromFin i)) 0
Theorem: IndexType.sum_linearize
Proof state before:
ι : Type v
inst✝⁴ : IndexType ι
I : Type u_1
X : Type u_2
inst✝³ : Add X
inst✝² : Zero X
inst✝¹ : IndexType I
inst✝ : LawfulIndexType I
f : I → X
⊢ fold (IndexType.univ I) (fun s i => s + f i) 0 = fold (IndexType.univ (Fin (card I))) (fun s i => s + f (fromFin i)) 0
Tactic:
rw[fold_linearize]
Proof state after:
no goals
Theorem: SciLean.Rand.flip.pdf_wrt_flip
Proof state before:
R : Type
inst✝¹ : RealScalar R
inst✝ : MeasureSpace R
θ θ' : R
⊢ pdf R (flip θ) (flip θ').ℙ = fun b => if b = true then θ / θ' else (1 - θ) / (1 - θ')
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.flip.pdf
Proof state before:
R : Type
inst✝¹ : RealScalar R
inst✝ : MeasureSpace R
x : R
⊢ Rand.pdf R (flip x) Measure.count = fun b =>
    let x := (x ⊔ 0) ⊓ 1;
    if b = true then x else 1 - x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.flip.integral
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ ∫' x, f x ∂(flip θ).ℙ = θ • f true + (1 - θ) • f false
Tactic:
simp [rand_simp,flip.measure]
Proof state after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ ∫' x,
      f
        x ∂(ENNReal.ofReal (Scalar.toReal R θ) • Measure.dirac true +
        ENNReal.ofReal (Scalar.toReal R (1 - θ)) • Measure.dirac false) =
    θ • f true + (1 - θ) • f false
Theorem: SciLean.Rand.flip.integral
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ ∫' x,
      f
        x ∂(ENNReal.ofReal (Scalar.toReal R θ) • Measure.dirac true +
        ENNReal.ofReal (Scalar.toReal R (1 - θ)) • Measure.dirac false) =
    θ • f true + (1 - θ) • f false
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Rand.flip.E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ (flip θ).𝔼 f = θ • f true + (1 - θ) • f false
Tactic:
simp only [𝔼,flip.integral]
Proof state after:
no goals
Theorem: SciLean.Rand.add_as_flip_E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ x + y = (flip θ).𝔼 fun b => if b = true then θ⁻¹ • x else (1 - θ)⁻¹ • y
Tactic:
simp[flip.E]
Proof state after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Theorem: SciLean.Rand.add_as_flip_E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Tactic:
have : θ ≠ 0 := by aesop
Proof state after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Theorem: SciLean.Rand.add_as_flip_E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Tactic:
have : 1 - θ ≠ 0 := by sorry_proof
Proof state after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this✝ : θ ≠ 0
this : 1 - θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Theorem: SciLean.Rand.add_as_flip_E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this✝ : θ ≠ 0
this : 1 - θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Tactic:
simp (disch:=assumption)
Proof state after:
no goals
Theorem: SciLean.Rand.add_as_flip_E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ θ ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.Rand.add_as_flip_E
Proof state before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ 1 - θ ≠ 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.arg_dx.IsLinearMap_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.10079
inst✝⁵ : Vec K Z
W : Type u_4
inst✝⁴ : Vec K W
ι : Type ?u.10101
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.10128
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
x : X
dx : W → X
hf : CDifferentiableAt K f x
hdx : IsLinearMap K dx
⊢ IsLinearMap K fun w => cderiv K f x (dx w)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.cderiv.arg_f.IsSmoothLinearMap_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ IsSmoothLinearMap K fun x => cderiv K fun x_1 => f x x_1
Tactic:
constructor
Proof state after:
case left
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ IsLinearMap K fun x => cderiv K fun x_1 => f x x_1

case right
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ CDifferentiable K fun x => cderiv K fun x_1 => f x x_1
Theorem: SciLean.cderiv.arg_f.IsSmoothLinearMap_rule
Proof state before:
case left
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ IsLinearMap K fun x => cderiv K fun x_1 => f x x_1

case right
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ CDifferentiable K fun x => cderiv K fun x_1 => f x x_1
Tactic:
fun_prop
Proof state after:
case right
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ CDifferentiable K fun x => cderiv K fun x_1 => f x x_1
Theorem: SciLean.cderiv.arg_f.IsSmoothLinearMap_rule
Proof state before:
case right
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_3
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.14968
inst✝⁴ : Vec K W
ι : Type ?u.14979
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.15006
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
hf :
  CDifferentiable K fun x =>
    match x with
    | (x, y) => f x y
hf' : ∀ (y : Y), IsLinearMap K fun x => f x y
⊢ CDifferentiable K fun x => cderiv K fun x_1 => f x x_1
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.id_rule
Proof state before:
K : Type u_2
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type ?u.18202
inst✝⁶ : Vec K Y
Z : Type ?u.18213
inst✝⁵ : Vec K Z
W : Type ?u.18224
inst✝⁴ : Vec K W
ι : Type ?u.18235
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18262
inst✝ : (i : ι) → Vec K (E i)
⊢ (cderiv K fun x => x) = fun x dx => dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.const_rule
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_1
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type ?u.18418
inst✝⁵ : Vec K Z
W : Type ?u.18429
inst✝⁴ : Vec K W
ι : Type ?u.18440
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18467
inst✝ : (i : ι) → Vec K (E i)
x : X
⊢ (cderiv K fun x_1 => x) = fun x dx => 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.comp_rule_at
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.19295
inst✝⁴ : Vec K W
ι : Type ?u.19306
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.19333
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
x : X
hf : CDifferentiableAt K f (g x)
hg : CDifferentiableAt K g x
⊢ cderiv K (fun x => f (g x)) x =
    let y := g x;
    fun dx =>
    let dy := cderiv K g x dx;
    let dz := cderiv K f y dy;
    dz
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.comp_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_2
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type ?u.19639
inst✝⁴ : Vec K W
ι : Type ?u.19650
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.19677
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : CDifferentiable K f
hg : CDifferentiable K g
⊢ (cderiv K fun x => f (g x)) = fun x =>
    let y := g x;
    fun dx =>
    let dy := cderiv K g x dx;
    let dz := cderiv K f y dy;
    dz
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.let_rule_at
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.19984
inst✝⁴ : Vec K W
ι : Type ?u.19995
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.20022
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
g : X → Y
x : X
hf : CDifferentiableAt K (↿f) (x, g x)
hg : CDifferentiableAt K g x
⊢ cderiv K
      (fun x =>
        let y := g x;
        f x y)
      x =
    let y := g x;
    fun dx =>
    let dy := cderiv K g x dx;
    let dz := cderiv K (fun xy => f xy.1 xy.2) (x, y) (dx, dy);
    dz
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.let_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.20485
inst✝⁴ : Vec K W
ι : Type ?u.20496
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.20523
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
g : X → Y
hf : CDifferentiable K fun xy => f xy.1 xy.2
hg : CDifferentiable K g
⊢ (cderiv K fun x =>
      let y := g x;
      f x y) =
    fun x =>
    let y := g x;
    fun dx =>
    let dy := cderiv K g x dx;
    let dz := cderiv K (fun xy => f xy.1 xy.2) (x, y) (dx, dy);
    dz
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.apply_rule
Proof state before:
K : Type u_3
inst✝⁸ : RCLike K
X : Type ?u.20874
inst✝⁷ : Vec K X
Y : Type ?u.20887
inst✝⁶ : Vec K Y
Z : Type ?u.20898
inst✝⁵ : Vec K Z
W : Type ?u.20909
inst✝⁴ : Vec K W
ι : Type u_1
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_2
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ (cderiv K fun x => x i) = fun x dx => dx i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.pi_rule_at
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.21720
inst✝⁶ : Vec K Y
Z : Type ?u.21731
inst✝⁵ : Vec K Z
W : Type ?u.21742
inst✝⁴ : Vec K W
ι : Type u_4
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
f : X → (i : ι) → E i
x : X
hf : ∀ (i : ι), CDifferentiableAt K (fun x => f x i) x
⊢ cderiv K (fun x i => f x i) x = fun dx i => cderiv K (fun x => f x i) x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.cderiv.pi_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type ?u.22558
inst✝⁶ : Vec K Y
Z : Type ?u.22569
inst✝⁵ : Vec K Z
W : Type ?u.22580
inst✝⁴ : Vec K W
ι : Type u_4
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ (cderiv K fun x i => f x i) = fun x dx i => cderiv K (fun x => f x i) x dx
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.cderiv_rule_at
Proof state before:
K✝ : Type ?u.23567
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.23573
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.23586
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.23597
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.23608
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.23619
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.23646
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.23703
inst✝⁴ : Vec K W
ι : Type ?u.23714
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.23741
inst✝ : (i : ι) → Vec K (E i)
x : X
g : X → Y
hg : CDifferentiableAt K g x
f : X → Z
hf : CDifferentiableAt K f x
⊢ cderiv K (fun x => (g x, f x)) x = fun dx => (cderiv K g x dx, cderiv K f x dx)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.cderiv_rule
Proof state before:
K✝ : Type ?u.24079
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.24085
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.24098
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.24109
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.24120
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.24131
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.24158
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.24215
inst✝⁴ : Vec K W
ι : Type ?u.24226
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.24253
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : CDifferentiable K g
f : X → Z
hf : CDifferentiable K f
⊢ (cderiv K fun x => (g x, f x)) = fun x dx => (cderiv K g x dx, cderiv K f x dx)
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.24079
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.24085
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.24098
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.24109
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.24120
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.24131
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.24158
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.24215
inst✝⁴ : Vec K W
ι : Type ?u.24226
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.24253
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : CDifferentiable K g
f : X → Z
hf : CDifferentiable K f
x : X
⊢ cderiv K (fun x => (g x, f x)) x = fun dx => (cderiv K g x dx, cderiv K f x dx)
Theorem: SciLean.Prod.mk.arg_fstsnd.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.24079
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.24085
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.24098
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.24109
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.24120
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.24131
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.24158
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type u_4
inst✝⁵ : Vec K Z
W : Type ?u.24215
inst✝⁴ : Vec K W
ι : Type ?u.24226
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.24253
inst✝ : (i : ι) → Vec K (E i)
g : X → Y
hg : CDifferentiable K g
f : X → Z
hf : CDifferentiable K f
x : X
⊢ cderiv K (fun x => (g x, f x)) x = fun dx => (cderiv K g x dx, cderiv K f x dx)
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.cderiv_rule_at
Proof state before:
K✝ : Type ?u.25720
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.25726
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.25739
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.25750
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.25761
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.25772
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.25799
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.25856
inst✝⁴ : Vec K W
ι : Type ?u.25867
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.25894
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y × Z
hf : CDifferentiableAt K f x
⊢ cderiv K (fun x => (f x).1) x = fun dx => (cderiv K f x dx).1
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.Prod.fst.arg_self.cderiv_rule
Proof state before:
K✝ : Type ?u.27548
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.27554
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.27567
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.27578
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.27589
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.27600
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.27627
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.27684
inst✝⁴ : Vec K W
ι : Type ?u.27695
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.27722
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
⊢ (cderiv K fun x => (f x).1) = fun x dx => (cderiv K f x dx).1
Tactic:
funext x
Proof state after:
case h
K✝ : Type ?u.27548
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.27554
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.27567
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.27578
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.27589
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.27600
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.27627
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.27684
inst✝⁴ : Vec K W
ι : Type ?u.27695
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.27722
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
x : X
⊢ cderiv K (fun x => (f x).1) x = fun dx => (cderiv K f x dx).1
Theorem: SciLean.Prod.fst.arg_self.cderiv_rule
Proof state before:
case h
K✝ : Type ?u.27548
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.27554
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.27567
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.27578
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.27589
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.27600
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.27627
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.27684
inst✝⁴ : Vec K W
ι : Type ?u.27695
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.27722
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : CDifferentiable K f
x : X
⊢ cderiv K (fun x => (f x).1) x = fun dx => (cderiv K f x dx).1
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.Prod.snd.arg_self.cderiv_rule_at
Proof state before:
K✝ : Type ?u.28916
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.28922
inst✝¹⁶ : Vec K✝ X✝
Y✝ : Type ?u.28935
inst✝¹⁵ : Vec K✝ Y✝
Z✝ : Type ?u.28946
inst✝¹⁴ : Vec K✝ Z✝
W✝ : Type ?u.28957
inst✝¹³ : Vec K✝ W✝
ι✝ : Type ?u.28968
inst✝¹² : IndexType ι✝
inst✝¹¹ : LawfulIndexType ι✝
inst✝¹⁰ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28995
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_3
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_2
inst✝⁵ : Vec K Z
W : Type ?u.29052
inst✝⁴ : Vec K W
ι : Type ?u.29063
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29090
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → Y × Z
hf : CDifferentiableAt K f x
⊢ cderiv K (fun x => (f x).2) x = fun dx => (cderiv K f x dx).2
Tactic:
fun_trans
Proof state after:
no goals