internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Function.invFun.arg_f.cderiv_rule'
Proof state before:
case h.h
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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - 0 =
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
rw[← H]
Proof state after:
case h.h
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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z =
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Theorem: SciLean.Function.invFun.arg_f.cderiv_rule'
Proof state before:
case h.h
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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
H : (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z = 0
⊢ cderiv K (fun x => invFun (f x) z) x dx - (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z =
    let y := invFun (f x) z;
    let dfdx_y := cderiv K f x dx y;
    let df'dy := cderiv K (invFun (f x)) (f x y) dfdx_y;
    -df'dy
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Function.invFun.arg_f.cderiv_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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ (cderiv K (fun x => invFun (f x) ∘ f x) x dx ∘ invFun (f x)) z = 0
Tactic:
simp[invFun_comp (hf _).1.1]
Proof state after:
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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x' => invFun (f x) z) x dx = 0
Theorem: SciLean.Function.invFun.arg_f.cderiv_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.58775
inst✝⁴ : Vec K W
ι : Type ?u.58786
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.58813
inst✝ : (i : ι) → Vec K (E i)
f : X → Y → Z
z : Z
hf : ∀ (x : X), Diffeomorphism K (f x)
hf' : CDifferentiable K fun xy => f xy.1 xy.2
x dx : X
⊢ cderiv K (fun x' => invFun (f x) z) x dx = 0
Tactic:
fun_trans
Proof state after:
no goals
Theorem: SciLean.action_mk_apply
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.37862
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.39481
inst✝ : Vec R Z
f : (𝒟 X) ⊸[R] Y
φ : 𝒟 X
⊢ { action := f }.action φ = f φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.DistributionFun.ext
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
x y : 𝒟'(X, Y)
⊢ (∀ (φ : 𝒟 X), x.action φ = y.action φ) → x = y
Tactic:
induction x
Proof state after:
case mk
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
y : 𝒟'(X, Y)
action✝ : (𝒟 X) ⊸[R] Y
⊢ (∀ (φ : 𝒟 X), { action := action✝ }.action φ = y.action φ) → { action := action✝ } = y
Theorem: SciLean.DistributionFun.ext
Proof state before:
case mk
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
y : 𝒟'(X, Y)
action✝ : (𝒟 X) ⊸[R] Y
⊢ (∀ (φ : 𝒟 X), { action := action✝ }.action φ = y.action φ) → { action := action✝ } = y
Tactic:
induction y
Proof state after:
case mk.mk
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
action✝¹ action✝ : (𝒟 X) ⊸[R] Y
⊢ (∀ (φ : 𝒟 X), { action := action✝¹ }.action φ = { action := action✝ }.action φ) →
    { action := action✝¹ } = { action := action✝ }
Theorem: SciLean.DistributionFun.ext
Proof state before:
case mk.mk
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
action✝¹ action✝ : (𝒟 X) ⊸[R] Y
⊢ (∀ (φ : 𝒟 X), { action := action✝¹ }.action φ = { action := action✝ }.action φ) →
    { action := action✝¹ } = { action := action✝ }
Tactic:
simp only [action_mk_apply, mk.injEq]
Proof state after:
case mk.mk
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
action✝¹ action✝ : (𝒟 X) ⊸[R] Y
⊢ (∀ (φ : 𝒟 X), action✝¹ φ = action✝ φ) → action✝¹ = action✝
Theorem: SciLean.DistributionFun.ext
Proof state before:
case mk.mk
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.41811
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.43430
inst✝ : Vec R Z
action✝¹ action✝ : (𝒟 X) ⊸[R] Y
⊢ (∀ (φ : 𝒟 X), action✝¹ φ = action✝ φ) → action✝¹ = action✝
Tactic:
aesop
Proof state after:
no goals
Theorem: SciLean.action_vecDirac
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.143544
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.145163
inst✝ : Vec R Z
x : X
y : Y
φ : 𝒟 X
⊢ (vecDirac x y).action φ = φ x • y
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.action_bind
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.150809
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_4
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type u_3
inst✝ : Vec R Z
x : 𝒟'(X, Z)
f : X → 𝒟'(Y, R)
φ : 𝒟 Y
⊢ (DistributionFun.bind x f).action φ = x.extAction fun x' => (f x').action φ
Tactic:
simp[DistributionFun.bind]
Proof state after:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.150809
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_4
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type u_3
inst✝ : Vec R Z
x : 𝒟'(X, Z)
f : X → 𝒟'(Y, R)
φ : 𝒟 Y
⊢ (limit n → ∞, { action := fun φ ⊸ x.action (testFunApprox n fun x => (f x).action φ) }).action φ =
    x.extAction fun x' => (f x').action φ
Theorem: SciLean.action_bind
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.150809
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_4
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type u_3
inst✝ : Vec R Z
x : 𝒟'(X, Z)
f : X → 𝒟'(Y, R)
φ : 𝒟 Y
⊢ (limit n → ∞, { action := fun φ ⊸ x.action (testFunApprox n fun x => (f x).action φ) }).action φ =
    x.extAction fun x' => (f x').action φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.zero_action
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.174391
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.176010
inst✝ : Vec R Z
φ : 𝒟 X
⊢ 0.action φ = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.DistributionFun.add_action
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.180378
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.181997
inst✝ : Vec R Z
T T' : 𝒟'(X, Y)
φ : 𝒟 X
⊢ (T + T').action φ = T.action φ + T'.action φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.DistributionFun.sub_action
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.187198
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.188817
inst✝ : Vec R Z
T T' : 𝒟'(X, Y)
φ : 𝒟 X
⊢ (T - T').action φ = T.action φ - T'.action φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.DistributionFun.smul_action
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.193462
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.195081
inst✝ : Vec R Z
r : R
T : 𝒟'(X, Y)
φ : 𝒟 X
⊢ (r • T).action φ = r • T.action φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.DistributionFun.neg_action
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.199801
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.201420
inst✝ : Vec R Z
T : 𝒟'(X, Y)
φ : 𝒟 X
⊢ (-T).action φ = -T.action φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.DistributionFun.fintype_sum_action
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.204688
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_3
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_4
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.206307
inst✝¹ : Vec R Z
I : Type u_1
inst✝ : Fintype I
T : I → 𝒟'(X, Y)
φ : 𝒟 X
⊢ (∑ i : I, T i).action φ = ∑ i : I, (T i).action φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.indextype_sum_action
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.213403
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_3
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type (max (max u_4 u_2) u_3)
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.215022
inst✝¹ : Vec R Z
I : Type u_1
inst✝ : IndexType I
T : I → 𝒟'(X, Y)
φ : 𝒟 X
⊢ ( ∑ i, T i).action φ = ∑ i, (T i).action φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.zero_extAction
Proof state before:
R : Type u_2
inst✝⁶ : RealScalar R
W : Type ?u.220097
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_3
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_1
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.221716
inst✝ : Vec R Z
φ : X → R
⊢ 0.extAction φ = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.add_extAction
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.223509
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.225128
inst✝ : Vec R Z
T T' : 𝒟'(X, Y)
φ : X → R
⊢ (T + T').extAction φ = T.extAction φ + T'.extAction φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.sub_extAction
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.228378
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.229997
inst✝ : Vec R Z
T T' : 𝒟'(X, Y)
φ : X → R
⊢ (T - T').extAction φ = T.extAction φ - T'.extAction φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.smul_extAction
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.232691
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.234310
inst✝ : Vec R Z
r : R
T : 𝒟'(X, Y)
φ : X → R
⊢ (r • T).extAction φ = r • T.extAction φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.neg_extAction
Proof state before:
R : Type u_1
inst✝⁶ : RealScalar R
W : Type ?u.237132
inst✝⁵ : Vec R W
inst✝⁴ : Module ℝ W
X : Type u_2
inst✝³ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝² : Vec R Y
inst✝¹ : Module ℝ Y
Z : Type ?u.238751
inst✝ : Vec R Z
T : 𝒟'(X, Y)
φ : X → R
⊢ (-T).extAction φ = -T.extAction φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.fintype_sum_extAction
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.240154
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_3
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_4
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.241773
inst✝¹ : Vec R Z
I : Type u_1
inst✝ : Fintype I
T : I → 𝒟'(X, Y)
φ : X → R
⊢ (∑ i : I, T i).extAction φ = ∑ i : I, (T i).extAction φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.indextype_sum_extAction
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.244994
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_3
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type (max (max u_4 u_2) u_3)
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.246613
inst✝¹ : Vec R Z
I : Type u_1
inst✝ : IndexType I
T : I → 𝒟'(X, Y)
φ : X → R
⊢ ( ∑ i, T i).extAction φ = ∑ i, (T i).extAction φ
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.action_iteD
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.264880
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_1
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.266499
inst✝¹ : Vec R Z
inst✝ : MeasureSpace X
A : Set X
t e : 𝒟'(X, Y)
φ : 𝒟 X
⊢ (ifD A then
          t
        else
          e).action
      φ =
    (t.extAction fun x => if x ∈ A then φ x else 0) + e.extAction fun x => if x ∉ A then φ x else 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.DistributionFun.extAction_iteD
Proof state before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.272009
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_1
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.273628
inst✝¹ : Vec R Z
inst✝ : MeasureSpace X
A : Set X
t e : 𝒟'(X, Y)
φ : X → R
⊢ (ifD A then
          t
        else
          e).extAction
      φ =
    (t.extAction fun x => if x ∈ A then φ x else 0) + e.extAction fun x => if x ∉ A then φ x else 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.iteD_restrict
Proof state before:
R : Type u_1
inst✝⁷ : RealScalar R
W : Type ?u.304829
inst✝⁶ : Vec R W
inst✝⁵ : Module ℝ W
X : Type u_2
inst✝⁴ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝³ : Vec R Y
inst✝² : Module ℝ Y
Z : Type ?u.306448
inst✝¹ : Vec R Z
inst✝ : MeasureSpace X
T : 𝒟'(X, Y)
A : Set X
⊢ (ifD A then
      T
    else
      0) =
    T.restrict A
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Function.toDistributionFun_action
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.347144
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_2
inst✝⁶ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.348763
inst✝³ : Vec R Z
inst✝² : MeasureSpace X
X₁ : Type ?u.348787
inst✝¹ : Vec R X₁
X₂ : Type ?u.348808
inst✝ : Vec R X₂
f : X → Y
φ : 𝒟 X
⊢ (↑f).action φ = ∫' x, φ x • f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Function.toDistributionFun_zero
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.357030
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_2
inst✝⁶ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.358649
inst✝³ : Vec R Z
inst✝² : MeasureSpace X
X₁ : Type ?u.358673
inst✝¹ : Vec R X₁
X₂ : Type ?u.358694
inst✝ : Vec R X₂
⊢ (↑fun x => 0) = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.id_rule
Proof state before:
tag : Lean.Name
R : Type u_2
inst✝²⁰ : Ring R
ι : Type u_3
X : Type u_4
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.22489
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.23223
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.24755
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.25553
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.26351
E : κ → Type ?u.26356
ME : κ → Type ?u.26361
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
⊢ (broadcast tag R ι fun x => x) = fun mx => mx
Tactic:
unfold broadcast
Proof state after:
tag : Lean.Name
R : Type u_2
inst✝²⁰ : Ring R
ι : Type u_3
X : Type u_4
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.22489
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.23223
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.24755
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.25553
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.26351
E : κ → Type ?u.26356
ME : κ → Type ?u.26361
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => x) ((BroadcastType.equiv tag) mx i)) =
    fun mx => mx
Theorem: SciLean.id_rule
Proof state before:
tag : Lean.Name
R : Type u_2
inst✝²⁰ : Ring R
ι : Type u_3
X : Type u_4
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type ?u.22489
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.23223
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type ?u.24755
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.25553
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.26351
E : κ → Type ?u.26356
ME : κ → Type ?u.26361
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => x) ((BroadcastType.equiv tag) mx i)) =
    fun mx => mx
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.const_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_6
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.32506
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.34836
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.35634
E : κ → Type ?u.35639
ME : κ → Type ?u.35644
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
y : Y
⊢ (broadcast tag R ι fun x => y) = fun x => broadcastIntro tag R fun x => y
Tactic:
unfold broadcast
Proof state after:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_6
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.32506
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.34836
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.35634
E : κ → Type ?u.35639
ME : κ → Type ?u.35644
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
y : Y
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => y) ((BroadcastType.equiv tag) mx i)) =
    fun x => broadcastIntro tag R fun x => y
Theorem: SciLean.const_rule
Proof state before:
tag : Lean.Name
R : Type u_3
inst✝²⁰ : Ring R
ι : Type u_4
X : Type u_5
inst✝¹⁹ : AddCommGroup X
inst✝¹⁸ : Module R X
Y : Type u_6
inst✝¹⁷ : AddCommGroup Y
inst✝¹⁶ : Module R Y
Z : Type ?u.32506
inst✝¹⁵ : AddCommGroup Z
inst✝¹⁴ : Module R Z
MX : Type u_1
inst✝¹³ : AddCommGroup MX
inst✝¹² : Module R MX
inst✝¹¹ : BroadcastType tag R ι X MX
MY : Type u_2
inst✝¹⁰ : AddCommGroup MY
inst✝⁹ : Module R MY
inst✝⁸ : BroadcastType tag R ι Y MY
MZ : Type ?u.34836
inst✝⁷ : AddCommGroup MZ
inst✝⁶ : Module R MZ
inst✝⁵ : BroadcastType tag R ι Z MZ
κ : Type ?u.35634
E : κ → Type ?u.35639
ME : κ → Type ?u.35644
inst✝⁴ : (j : κ) → AddCommGroup (E j)
inst✝³ : (j : κ) → Module R (E j)
inst✝² : (j : κ) → AddCommGroup (ME j)
inst✝¹ : (j : κ) → Module R (ME j)
inst✝ : (j : κ) → BroadcastType tag R ι (E j) (ME j)
y : Y
⊢ (fun mx => (LinearEquiv.symm (BroadcastType.equiv tag)) fun i => (fun x => y) ((BroadcastType.equiv tag) mx i)) =
    fun x => broadcastIntro tag R fun x => y
Tactic:
simp [broadcastIntro]
Proof state after:
no goals