internlm/Lean-Github huggingface dataset:
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
dec : Decidable c
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
⊢ IsSmoothLinearMap K fun x => if c then t x else e x
Tactic:
induction dec
Proof state after:
case isFalse
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h✝ : ¬c
⊢ IsSmoothLinearMap K fun x => if c then t x else e x

case isTrue
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h✝ : c
⊢ IsSmoothLinearMap K fun x => if c then t x else e x
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : c
⊢ IsSmoothLinearMap K fun x => if c then t x else e x
Tactic:
case isTrue h  => simp[h]; fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : ¬c
⊢ IsSmoothLinearMap K fun x => if c then t x else e x
Tactic:
case isFalse h => simp[h]; fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : c
⊢ IsSmoothLinearMap K fun x => if c then t x else e x
Tactic:
simp[h]
Proof state after:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : c
⊢ IsSmoothLinearMap K fun x => t x
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : c
⊢ IsSmoothLinearMap K fun x => t x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : ¬c
⊢ IsSmoothLinearMap K fun x => if c then t x else e x
Tactic:
simp[h]
Proof state after:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : ¬c
⊢ IsSmoothLinearMap K fun x => e x
Theorem: SciLean.IsSmoothLinearMap.ite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.28553
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.28559
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.28572
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.28583
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.28594
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.28621
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.28667
inst✝⁴ : Vec K Z
ι : Type ?u.28678
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.28705
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t e : X → Y
ht : IsSmoothLinearMap K t
he : IsSmoothLinearMap K e
h : ¬c
⊢ IsSmoothLinearMap K fun x => e x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
dec : Decidable c
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
induction dec
Proof state after:
case isFalse
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h✝ : ¬c
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x

case isTrue
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h✝ : c
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : c
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
case isTrue h  => simp[h]; apply ht
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : ¬c
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
case isFalse h => simp[h]; apply he
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : c
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
simp[h]
Proof state after:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : c
⊢ IsSmoothLinearMap K fun x => t ⋯ x
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : c
⊢ IsSmoothLinearMap K fun x => t ⋯ x
Tactic:
apply ht
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : ¬c
⊢ IsSmoothLinearMap K fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
simp[h]
Proof state after:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : ¬c
⊢ IsSmoothLinearMap K fun x => e ⋯ x
Theorem: SciLean.IsSmoothLinearMap.dite.arg_te.IsSmoothLinearMap_rule
Proof state before:
K✝ : Type ?u.29058
inst✝¹⁵ : RCLike K✝
X✝ : Type ?u.29064
inst✝¹⁴ : Vec K✝ X✝
Y✝ : Type ?u.29077
inst✝¹³ : Vec K✝ Y✝
Z✝ : Type ?u.29088
inst✝¹² : Vec K✝ Z✝
ι✝ : Type ?u.29099
inst✝¹¹ : IndexType ι✝
inst✝¹⁰ : LawfulIndexType ι✝
inst✝⁹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.29126
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.29172
inst✝⁴ : Vec K Z
ι : Type ?u.29183
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.29210
inst✝ : (i : ι) → Vec K (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsSmoothLinearMap K (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsSmoothLinearMap K (e p)
h : ¬c
⊢ IsSmoothLinearMap K fun x => e ⋯ x
Tactic:
apply he
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.SciLean.Basis.proj.arg_x.IsSmoothLinearMap_rule
Proof state before:
K✝¹ : Type ?u.30060
inst✝²⁸ : RCLike K✝¹
X✝¹ : Type ?u.30066
inst✝²⁷ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.30079
inst✝²⁶ : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.30090
inst✝²⁵ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.30101
inst✝²⁴ : IndexType ι✝
inst✝²³ : LawfulIndexType ι✝
inst✝²² : DecidableEq ι✝
E✝ : ι✝ → Type ?u.30128
inst✝²¹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.30144
inst✝²⁰ : RCLike K✝
X✝ : Type ?u.30150
inst✝¹⁹ : Vec K✝ X✝
Y✝ : Type ?u.30163
inst✝¹⁸ : Vec K✝ Y✝
Z✝ : Type ?u.30174
inst✝¹⁷ : Vec K✝ Z✝
ι : Type ?u.30185
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : ι → Type ?u.30212
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.30329
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.30332
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.30422
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.30425
inst✝ : FinVec IZ K Z
i : IX
⊢ IsSmoothLinearMap K fun x => ℼ i x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.SciLean.DualBasis.dualProj.arg_x.IsSmoothLinearMap_rule
Proof state before:
K✝¹ : Type ?u.31139
inst✝²⁸ : RCLike K✝¹
X✝¹ : Type ?u.31145
inst✝²⁷ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.31158
inst✝²⁶ : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.31169
inst✝²⁵ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.31180
inst✝²⁴ : IndexType ι✝
inst✝²³ : LawfulIndexType ι✝
inst✝²² : DecidableEq ι✝
E✝ : ι✝ → Type ?u.31207
inst✝²¹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.31223
inst✝²⁰ : RCLike K✝
X✝ : Type ?u.31229
inst✝¹⁹ : Vec K✝ X✝
Y✝ : Type ?u.31242
inst✝¹⁸ : Vec K✝ Y✝
Z✝ : Type ?u.31253
inst✝¹⁷ : Vec K✝ Z✝
ι : Type ?u.31264
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : ι → Type ?u.31291
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.31408
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.31411
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.31501
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.31504
inst✝ : FinVec IZ K Z
i : IX
⊢ IsSmoothLinearMap K fun x => ℼ' i x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.SciLean.BasisDuality.toDual.arg_x.IsSmoothLinearMap_rule
Proof state before:
K✝¹ : Type ?u.32218
inst✝²⁸ : RCLike K✝¹
X✝¹ : Type ?u.32224
inst✝²⁷ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.32237
inst✝²⁶ : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.32248
inst✝²⁵ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.32259
inst✝²⁴ : IndexType ι✝
inst✝²³ : LawfulIndexType ι✝
inst✝²² : DecidableEq ι✝
E✝ : ι✝ → Type ?u.32286
inst✝²¹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.32302
inst✝²⁰ : RCLike K✝
X✝ : Type ?u.32308
inst✝¹⁹ : Vec K✝ X✝
Y✝ : Type ?u.32321
inst✝¹⁸ : Vec K✝ Y✝
Z✝ : Type ?u.32332
inst✝¹⁷ : Vec K✝ Z✝
ι : Type ?u.32343
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : ι → Type ?u.32370
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.32487
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.32490
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.32580
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.32583
inst✝ : FinVec IZ K Z
⊢ IsSmoothLinearMap K fun x => BasisDuality.toDual x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: SciLean.IsSmoothLinearMap.SciLean.BasisDuality.fromDual.arg_x.IsSmoothLinearMap_rule
Proof state before:
K✝¹ : Type ?u.33189
inst✝²⁸ : RCLike K✝¹
X✝¹ : Type ?u.33195
inst✝²⁷ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.33208
inst✝²⁶ : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.33219
inst✝²⁵ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.33230
inst✝²⁴ : IndexType ι✝
inst✝²³ : LawfulIndexType ι✝
inst✝²² : DecidableEq ι✝
E✝ : ι✝ → Type ?u.33257
inst✝²¹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.33273
inst✝²⁰ : RCLike K✝
X✝ : Type ?u.33279
inst✝¹⁹ : Vec K✝ X✝
Y✝ : Type ?u.33292
inst✝¹⁸ : Vec K✝ Y✝
Z✝ : Type ?u.33303
inst✝¹⁷ : Vec K✝ Z✝
ι : Type ?u.33314
inst✝¹⁶ : IndexType ι
inst✝¹⁵ : LawfulIndexType ι
inst✝¹⁴ : DecidableEq ι
E : ι → Type ?u.33341
inst✝¹³ : (i : ι) → Vec K✝ (E i)
K : Type u_1
inst✝¹² : RCLike K
IX : Type u_3
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type ?u.33458
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.33461
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.33551
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.33554
inst✝ : FinVec IZ K Z
⊢ IsSmoothLinearMap K fun x => BasisDuality.fromDual x
Tactic:
constructor <;> fun_prop
Proof state after:
no goals
Theorem: circleParam.arg_θ.HasAdjDiff_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ HasAdjDiff R circleParam
Tactic:
unfold circleParam
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ HasAdjDiff R fun θ => (cos θ, sin θ)
Theorem: circleParam.arg_θ.HasAdjDiff_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ HasAdjDiff R fun θ => (cos θ, sin θ)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: circleParam.arg_θ.jacobian_rule
Proof state before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ jacobian R circleParam = 1
Tactic:
unfold circleParam jacobian
Proof state after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let dg := ∂ (θ:=x), (cos θ, sin θ);
      let dg' := semiAdjoint R dg;
      sqrt (det R (dg' ∘ dg))) =
    1