internlm/Lean-Github huggingface dataset:
Theorem: Function.invFun.Inv.inv.arg_a0.invFun_rule_group
Proof state before:
X✝ : Type ?u.1497
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1503
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1509
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.1515
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.1521
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1539
inst✝¹ : Nonempty Z
inst✝ : Group Y
f : X → Y
hf : Bijective f
⊢ (invFun fun x => (f x)⁻¹) = fun y => invFun f y⁻¹
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.Inv.inv.arg_a0.invFun_rule_field
Proof state before:
X✝ : Type ?u.1749
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1755
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1761
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.1767
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.1773
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1791
inst✝¹ : Nonempty Z
inst✝ : Field Y
f : X → Y
hf : Bijective f
hf' : ∀ (x : X), f x ≠ 0
⊢ (invFun fun x => (f x)⁻¹) = fun y => invFun f y⁻¹
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.HAdd.hAdd.arg_a0.invFun_rule
Proof state before:
X✝ : Type ?u.1996
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.2002
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.2008
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.2014
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.2020
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.2038
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
y : Y
hf : Bijective f
⊢ (invFun fun x => f x + y) = fun y' => invFun f (y' - y)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.HAdd.hAdd.arg_a1.invFun_rule
Proof state before:
X✝ : Type ?u.2736
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.2742
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.2748
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.2754
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.2760
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.2778
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
y : Y
f : X → Y
hf : Bijective f
⊢ (invFun fun x => y + f x) = fun y' => invFun f (-y + y')
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.HSub.hSub.arg_a0.invFun_rule
Proof state before:
X✝ : Type ?u.3787
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.3793
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.3799
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.3805
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.3811
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.3829
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
y : Y
hf : Bijective f
⊢ (invFun fun x => f x - y) = fun y' => invFun f (y' + y)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.HSub.hSub.arg_a1.invFun_rule
Proof state before:
X✝ : Type ?u.4527
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.4533
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.4539
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.4545
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.4551
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.4569
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
y : Y
f : X → Y
hf : Bijective f
⊢ (invFun fun x => y - f x) = fun y' => invFun f (y - y')
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.Equiv.toFun.arg_a0.invFun_rule
Proof state before:
X✝ : Type ?u.10643
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.10649
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.10655
inst✝⁵ : Nonempty Z✝
X₁ : Type ?u.10661
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.10667
inst✝³ : Nonempty X₂
X : Type u_3
inst✝² : Nonempty X
Y : Type u_1
inst✝¹ : Nonempty Y
Z : Type u_2
inst✝ : Nonempty Z
f : Y ≃ Z
g : X → Y
hf : Bijective g
⊢ (invFun fun x => f (g x)) = fun z => invFun g (f.invFun z)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Function.invFun.Equiv.invFun.arg_a0.invFun_rule
Proof state before:
X✝ : Type ?u.10851
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.10857
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.10863
inst✝⁵ : Nonempty Z✝
X₁ : Type ?u.10869
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.10875
inst✝³ : Nonempty X₂
X : Type u_3
inst✝² : Nonempty X
Y : Type u_1
inst✝¹ : Nonempty Y
Z : Type u_2
inst✝ : Nonempty Z
f : Y ≃ Z
g : X → Z
hf : Bijective g
⊢ (invFun fun x => f.invFun (g x)) = fun z => invFun g (f z)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.id_rule
Proof state before:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.3337
inst✝⁵ : Vec K Y
Z : Type ?u.3348
inst✝⁴ : Vec K Z
ι : Type ?u.3359
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3386
inst✝ : (i : ι) → Vec K (E i)
⊢ IsSmoothLinearMap K fun x => x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.const_zero_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.3750
inst✝⁴ : Vec K Z
ι : Type ?u.3761
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3788
inst✝ : (i : ι) → Vec K (E i)
⊢ IsSmoothLinearMap K fun x => 0
Tactic:
constructor <;> first | fun_prop | apply IsLinearMap.isLinearMap_const_zero
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.const_zero_rule
Proof state before:
case right
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.3750
inst✝⁴ : Vec K Z
ι : Type ?u.3761
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.3788
inst✝ : (i : ι) → Vec K (E i)
⊢ CDifferentiable K fun x => 0
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.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
ι : Type ?u.4954
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.4981
inst✝ : (i : ι) → Vec K (E i)
f : Y → Z
g : X → Y
hf : IsSmoothLinearMap K f
hg : IsSmoothLinearMap K g
⊢ IsSmoothLinearMap K fun x => f (g x)
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.apply_rule
Proof state before:
K : Type u_1
inst✝⁷ : RCLike K
X : Type ?u.5739
inst✝⁶ : Vec K X
Y : Type ?u.5752
inst✝⁵ : Vec K Y
Z : Type ?u.5763
inst✝⁴ : Vec K Z
ι : Type u_2
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
⊢ IsSmoothLinearMap K fun x => x i
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
⊢ IsSmoothLinearMap K fun x i => f x i
Tactic:
have := fun i => (hf i).1
Proof state after:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ IsSmoothLinearMap K fun x i => f x i
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this : ∀ (i : ι), IsLinearMap K fun x => f x i
⊢ IsSmoothLinearMap K fun x i => f x i
Tactic:
have := fun i => (hf i).2
Proof state after:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ IsSmoothLinearMap K fun x i => f x i
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ IsSmoothLinearMap K fun x i => f x i
Tactic:
constructor
Proof state after:
case left
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ IsLinearMap K fun x i => f x i

case right
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x i => f x i
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
case left
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ IsLinearMap K fun x i => f x i

case right
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x i => f x i
Tactic:
. fun_prop
Proof state after:
case right
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x i => f x i
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
case right
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x i => f x i
Tactic:
. fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
case left
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ IsLinearMap K fun x i => f x i
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.pi_rule
Proof state before:
case right
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.7976
inst✝⁵ : Vec K Y
Z : Type ?u.7987
inst✝⁴ : Vec K Z
ι : 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 : ι), IsSmoothLinearMap K fun x => f x i
this✝ : ∀ (i : ι), IsLinearMap K fun x => f x i
this : ∀ (i : ι), CDifferentiable K fun x => f x i
⊢ CDifferentiable K fun x i => f x i
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.Prod.mk.arg_fstsnd.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.10721
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.10727
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.10740
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.10751
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.10762
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.10789
inst✝⁸ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type u_4
inst✝⁵ : Vec K Y
Z : Type u_3
inst✝⁴ : Vec K Z
ι : Type ?u.10846
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.10873
inst✝ : (i : ι) → Vec K (E i)
f : X → Z
g : X → Y
hf : IsSmoothLinearMap K f
hg : IsSmoothLinearMap K g
⊢ IsSmoothLinearMap K fun x => (g x, f x)
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.Prod.fst.arg_self.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.11763
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.11769
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.11782
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.11793
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.11804
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.11831
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
ι : Type ?u.11888
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.11915
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => (f x).1
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.Prod.snd.arg_self.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.12609
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.12615
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.12628
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.12639
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.12650
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.12677
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
ι : Type ?u.12734
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.12761
inst✝ : (i : ι) → Vec K (E i)
f : X → Y × Z
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => (f x).2
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.Neg.neg.arg_a0.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.13455
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.13461
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.13474
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.13485
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.13496
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.13523
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.13569
inst✝⁴ : Vec K Z
ι : Type ?u.13580
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.13607
inst✝ : (i : ι) → Vec K (E i)
f : X → Y
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => -f x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HAdd.hAdd.arg_a0a1.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.14374
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.14380
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.14393
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.14404
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.14415
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.14442
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.14488
inst✝⁴ : Vec K Z
ι : Type ?u.14499
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.14526
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : IsSmoothLinearMap K f
hg : IsSmoothLinearMap K g
⊢ IsSmoothLinearMap K fun x => f x + g x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HSub.hSub.arg_a0a1.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.16342
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.16348
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.16361
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.16372
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.16383
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.16410
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.16456
inst✝⁴ : Vec K Z
ι : Type ?u.16467
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.16494
inst✝ : (i : ι) → Vec K (E i)
f g : X → Y
hf : IsSmoothLinearMap K f
hg : IsSmoothLinearMap K g
⊢ IsSmoothLinearMap K fun x => f x - g x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HMul.hMul.arg_a0.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.17774
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.17780
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.17793
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.17804
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.17815
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.17842
inst✝⁸ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.17877
inst✝⁵ : Vec K Y
Z : Type ?u.17888
inst✝⁴ : Vec K Z
ι : Type ?u.17899
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.17926
inst✝ : (i : ι) → Vec K (E i)
f : X → K
hf : IsSmoothLinearMap K f
y' : K
⊢ IsSmoothLinearMap K fun x => f x * y'
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HMul.hMul.arg_a1.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.18593
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.18599
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.18612
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.18623
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.18634
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.18661
inst✝⁸ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type u_1
inst✝⁷ : RCLike K
X : Type u_2
inst✝⁶ : Vec K X
Y : Type ?u.18696
inst✝⁵ : Vec K Y
Z : Type ?u.18707
inst✝⁴ : Vec K Z
ι : Type ?u.18718
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18745
inst✝ : (i : ι) → Vec K (E i)
f : X → K
hf : IsSmoothLinearMap K f
y' : K
⊢ IsSmoothLinearMap K fun x => y' * f x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HSMul.hSMul.arg_a0.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.19412
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.19418
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.19431
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.19442
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.19453
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.19480
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.19526
inst✝⁴ : Vec K Z
ι : Type ?u.19537
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.19564
inst✝ : (i : ι) → Vec K (E i)
f : X → K
y : Y
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => f x • y
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HSMul.hSMul.arg_a1.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.21676
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.21682
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.21695
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.21706
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.21717
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.21744
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.21790
inst✝⁴ : Vec K Z
ι : Type ?u.21801
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.21828
inst✝ : (i : ι) → Vec K (E i)
c : K
f : X → Y
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => c • f x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HSMul.hSMul.arg_a1.IsSmoothLinearMap_rule_nat
Proof state before:
K✝ : Type ?u.23972
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.23978
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.23991
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.24002
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.24013
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.24040
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.24086
inst✝⁴ : Vec K Z
ι : Type ?u.24097
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.24124
inst✝ : (i : ι) → Vec K (E i)
c : ℕ
f : X → Y
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => c • f x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.HSMul.hSMul.arg_a1.IsSmoothLinearMap_rule_int
Proof state before:
K✝ : Type ?u.25273
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.25279
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.25292
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.25303
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.25314
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.25341
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.25387
inst✝⁴ : Vec K Z
ι : Type ?u.25398
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.25425
inst✝ : (i : ι) → Vec K (E i)
c : ℤ
f : X → Y
hf : IsSmoothLinearMap K f
⊢ IsSmoothLinearMap K fun x => c • f x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.IndexType.sum.arg_f.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.26395
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.26401
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.26414
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.26425
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.26436
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.26463
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.26509
inst✝⁴ : Vec K Z
ι : Type u_4
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.26547
inst✝ : (i : ι) → Vec K (E i)
f : X → ι → Y
hf : ∀ (i : ι), IsSmoothLinearMap K fun x => f x i
⊢ IsSmoothLinearMap K fun x =>  ∑ i, f x i
Tactic:
constructor <;> fun_prop
Proof state after:
no goals