internlm/Lean-Github huggingface dataset:
Theorem: SciLean.DualBasis.dualProj.arg_x.CDifferentiableAt_rule
Proof state before:
K✝¹ : Type ?u.42308
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.42314
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.42327
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.42338
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.42349
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.42358
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.42374
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.42380
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.42393
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.42404
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.42415
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.42424
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.42537
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.42540
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.42626
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.42629
inst✝ : FinVec IZ K Z
i : IX
x : X
⊢ CDifferentiableAt K (fun x => ℼ' i x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.BasisDuality.toDual.arg_x.CDifferentiable_rule
Proof state before:
K✝¹ : Type ?u.43395
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.43401
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.43414
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.43425
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.43436
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.43445
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.43461
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.43467
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.43480
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.43491
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.43502
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.43511
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.43624
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.43627
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.43713
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.43716
inst✝ : FinVec IZ K Z
⊢ CDifferentiable K fun x => toDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.toDual.arg_x.CDifferentiableAt_rule
Proof state before:
K✝¹ : Type ?u.44041
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.44047
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.44060
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.44071
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.44082
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.44091
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.44107
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.44113
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.44126
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.44137
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.44148
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.44157
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.44270
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.44273
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.44359
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.44362
inst✝ : FinVec IZ K Z
x : X
⊢ CDifferentiableAt K (fun x => toDual x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.BasisDuality.fromDual.arg_x.CDifferentiable_rule
Proof state before:
K✝¹ : Type ?u.44988
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.44994
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.45007
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.45018
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.45029
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.45038
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.45054
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.45060
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.45073
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.45084
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.45095
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.45104
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.45217
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.45220
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.45306
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.45309
inst✝ : FinVec IZ K Z
⊢ CDifferentiable K fun x => fromDual x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.BasisDuality.fromDual.arg_x.CDifferentiableAt_rule
Proof state before:
K✝¹ : Type ?u.45634
inst✝²⁴ : RCLike K✝¹
X✝¹ : Type ?u.45640
inst✝²³ : Vec K✝¹ X✝¹
Y✝¹ : Type ?u.45653
inst✝²² : Vec K✝¹ Y✝¹
Z✝¹ : Type ?u.45664
inst✝²¹ : Vec K✝¹ Z✝¹
ι✝ : Type ?u.45675
inst✝²⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.45684
inst✝¹⁹ : (i : ι✝) → Vec K✝¹ (E✝ i)
K✝ : Type ?u.45700
inst✝¹⁸ : RCLike K✝
X✝ : Type ?u.45706
inst✝¹⁷ : Vec K✝ X✝
Y✝ : Type ?u.45719
inst✝¹⁶ : Vec K✝ Y✝
Z✝ : Type ?u.45730
inst✝¹⁵ : Vec K✝ Z✝
ι : Type ?u.45741
inst✝¹⁴ : IndexType ι
E : ι → Type ?u.45750
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.45863
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.45866
inst✝⁴ : FinVec IY K Y
IZ : Type ?u.45952
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.45955
inst✝ : FinVec IZ K Z
x : X
⊢ CDifferentiableAt K (fun x => fromDual x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.isomorph.id_rule
Proof state before:
α : Type u_2
β : Type ?u.40
γ : Type ?u.43
α' : outParam (Type u_1)
β' : outParam (Type ?u.51)
γ' : outParam (Type ?u.55)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
⊢ (isomorph tag fun x => x) = fun x => x
Tactic:
funext _
Proof state after:
case h
α : Type u_2
β : Type ?u.40
γ : Type ?u.43
α' : outParam (Type u_1)
β' : outParam (Type ?u.51)
γ' : outParam (Type ?u.55)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x✝ : α'
⊢ isomorph tag (fun x => x) x✝ = x✝
Theorem: SciLean.isomorph.id_rule
Proof state before:
case h
α : Type u_2
β : Type ?u.40
γ : Type ?u.43
α' : outParam (Type u_1)
β' : outParam (Type ?u.51)
γ' : outParam (Type ?u.55)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x✝ : α'
⊢ isomorph tag (fun x => x) x✝ = x✝
Tactic:
simp[isomorph]
Proof state after:
no goals
Theorem: SciLean.isomorph.const_rule
Proof state before:
α : Type u_3
β : Type u_4
γ : Type ?u.895
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.907)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
y : β
⊢ (isomorph tag fun x => y) = fun x => (IsomorphicType.equiv tag) y
Tactic:
funext _
Proof state after:
case h
α : Type u_3
β : Type u_4
γ : Type ?u.895
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.907)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
y : β
x✝ : α'
⊢ isomorph tag (fun x => y) x✝ = (IsomorphicType.equiv tag) y
Theorem: SciLean.isomorph.const_rule
Proof state before:
case h
α : Type u_3
β : Type u_4
γ : Type ?u.895
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.907)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
y : β
x✝ : α'
⊢ isomorph tag (fun x => y) x✝ = (IsomorphicType.equiv tag) y
Tactic:
simp[isomorph]
Proof state after:
no goals
Theorem: SciLean.isomorph.comp_rule
Proof state before:
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : β → γ
g : α → β
⊢ (isomorph tag fun x => f (g x)) = fun x => isomorph tag f (isomorph tag g x)
Tactic:
funext _
Proof state after:
case h
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : β → γ
g : α → β
x✝ : α'
⊢ isomorph tag (fun x => f (g x)) x✝ = isomorph tag f (isomorph tag g x✝)
Theorem: SciLean.isomorph.comp_rule
Proof state before:
case h
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : β → γ
g : α → β
x✝ : α'
⊢ isomorph tag (fun x => f (g x)) x✝ = isomorph tag f (isomorph tag g x✝)
Tactic:
unfold isomorph
Proof state after:
case h
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : β → γ
g : α → β
x✝ : α'
⊢ (IsomorphicType.equiv tag) ((fun x => f (g x)) ((IsomorphicType.equiv tag).symm x✝)) =
    (IsomorphicType.equiv tag)
      (f ((IsomorphicType.equiv tag).symm ((IsomorphicType.equiv tag) (g ((IsomorphicType.equiv tag).symm x✝)))))
Theorem: SciLean.isomorph.comp_rule
Proof state before:
case h
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : β → γ
g : α → β
x✝ : α'
⊢ (IsomorphicType.equiv tag) ((fun x => f (g x)) ((IsomorphicType.equiv tag).symm x✝)) =
    (IsomorphicType.equiv tag)
      (f ((IsomorphicType.equiv tag).symm ((IsomorphicType.equiv tag) (g ((IsomorphicType.equiv tag).symm x✝)))))
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.isomorph.let_rule
Proof state before:
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
g : α → β
⊢ (isomorph tag fun x =>
      let y := g x;
      f x y) =
    fun x' =>
    let y' := isomorph tag g x';
    isomorph tag (fun xy => f xy.1 xy.2) (x', y')
Tactic:
funext x'
Proof state after:
case h
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
g : α → β
x' : α'
⊢ isomorph tag
      (fun x =>
        let y := g x;
        f x y)
      x' =
    let y' := isomorph tag g x';
    isomorph tag (fun xy => f xy.1 xy.2) (x', y')
Theorem: SciLean.isomorph.let_rule
Proof state before:
case h
α : Type u_3
β : Type u_5
γ : Type u_4
α' : outParam (Type u_1)
β' : outParam (Type u_6)
γ' : outParam (Type u_2)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
g : α → β
x' : α'
⊢ isomorph tag
      (fun x =>
        let y := g x;
        f x y)
      x' =
    let y' := isomorph tag g x';
    isomorph tag (fun xy => f xy.1 xy.2) (x', y')
Tactic:
simp[isomorph, IsomorphicType.equiv, -isomorph.app]
Proof state after:
no goals
Theorem: SciLean.isomorph.apply_rule
Proof state before:
α : Type u_3
β : Type u_4
γ : Type ?u.13084
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.13096)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x : α
⊢ (isomorph tag fun f => f x) = fun f => f ((IsomorphicType.equiv tag) x)
Tactic:
funext _
Proof state after:
case h
α : Type u_3
β : Type u_4
γ : Type ?u.13084
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.13096)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x : α
x✝ : α' → β'
⊢ isomorph tag (fun f => f x) x✝ = x✝ ((IsomorphicType.equiv tag) x)
Theorem: SciLean.isomorph.apply_rule
Proof state before:
case h
α : Type u_3
β : Type u_4
γ : Type ?u.13084
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.13096)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x : α
x✝ : α' → β'
⊢ isomorph tag (fun f => f x) x✝ = x✝ ((IsomorphicType.equiv tag) x)
Tactic:
simp[isomorph, invIsomorph, IsomorphicType.equiv]
Proof state after:
no goals
Theorem: SciLean.isomorph.pi_rule
Proof state before:
α : Type u_4
β : Type u_5
γ : Type u_6
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
⊢ (isomorph tag fun x y => f x y) = fun x' => isomorph tag (f ((IsomorphicType.equiv tag).symm x'))
Tactic:
funext x'
Proof state after:
case h
α : Type u_4
β : Type u_5
γ : Type u_6
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
x' : α'
⊢ isomorph tag (fun x y => f x y) x' = isomorph tag (f ((IsomorphicType.equiv tag).symm x'))
Theorem: SciLean.isomorph.pi_rule
Proof state before:
case h
α : Type u_4
β : Type u_5
γ : Type u_6
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
x' : α'
⊢ isomorph tag (fun x y => f x y) x' = isomorph tag (f ((IsomorphicType.equiv tag).symm x'))
Tactic:
simp[isomorph, IsomorphicType.equiv]
Proof state after:
no goals
Theorem: Prod.mk.isomorph_rule
Proof state before:
α : Type u_4
β : Type u_6
γ : Type u_5
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β
g : α → γ
⊢ (isomorph tag fun x => (f x, g x)) = fun x' =>
    let y' := isomorph tag f x';
    let z' := isomorph tag g x';
    (y', z')
Tactic:
rfl
Proof state after:
no goals
Theorem: Prod.fst.isomorph_rule
Proof state before:
α : Type u_5
β : Type u_1
γ : Type u_2
α' : outParam (Type u_3)
β' : outParam (Type u_4)
γ' : outParam (Type u_6)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β × γ
⊢ (isomorph tag fun x => (f x).1) = fun x =>
    let f' := isomorph tag f;
    (f' x).1
Tactic:
rfl
Proof state after:
no goals
Theorem: Prod.snd.isomorph_rule
Proof state before:
α : Type u_5
β : Type u_1
γ : Type u_2
α' : outParam (Type u_3)
β' : outParam (Type u_4)
γ' : outParam (Type u_6)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β × γ
⊢ (isomorph tag fun x => (f x).1) = fun x =>
    let f' := isomorph tag f;
    (f' x).1
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Rand.foobar.arg_acc.IsAffineMap
Proof state before:
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
l : List R
⊢ _root_.IsAffineMap ℝ fun acc => foobar l acc
Tactic:
induction l <;> (simp[foobar]; fun_prop)
Proof state after:
no goals
Theorem: SciLean.Rand.foobar.arg_acc.IsAffineMap
Proof state before:
case cons
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
head✝ : R
tail✝ : List R
tail_ih✝ : _root_.IsAffineMap ℝ fun acc => foobar tail✝ acc
⊢ _root_.IsAffineMap ℝ fun acc => foobar (head✝ :: tail✝) acc
Tactic:
simp[foobar]
Proof state after:
case cons
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
head✝ : R
tail✝ : List R
tail_ih✝ : _root_.IsAffineMap ℝ fun acc => foobar tail✝ acc
⊢ _root_.IsAffineMap ℝ fun acc => foobar tail✝ (acc + head✝)
Theorem: SciLean.Rand.foobar.arg_acc.IsAffineMap
Proof state before:
case cons
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
head✝ : R
tail✝ : List R
tail_ih✝ : _root_.IsAffineMap ℝ fun acc => foobar tail✝ acc
⊢ _root_.IsAffineMap ℝ fun acc => foobar tail✝ (acc + head✝)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.isomorph.app
Proof state before:
α : Type u_3
β : Type u_2
γ : Type ?u.587
α' : outParam (Type u_4)
β' : outParam (Type u_1)
γ' : outParam (Type ?u.599)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β
x : α
⊢ (IsomorphicType.equiv tag) (f x) = isomorph tag f ((IsomorphicType.equiv tag) x)
Tactic:
simp[IsomorphicType.equiv, isomorph]
Proof state after:
no goals
Theorem: SciLean.isomorph.ext
Proof state before:
α : Type u_2
β : Type ?u.2581
γ : Type ?u.2584
α' : outParam (Type u_1)
β' : outParam (Type ?u.2592)
γ' : outParam (Type ?u.2596)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
a b : α
⊢ (IsomorphicType.equiv tag) a = (IsomorphicType.equiv tag) b → a = b
Tactic:
simp[IsomorphicType.equiv]
Proof state after:
no goals
Theorem: SciLean.isomorph.funext
Proof state before:
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
⊢ isomorph tag f = isomorph tag g → f = g
Tactic:
intro h
Proof state after:
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
⊢ f = g
Theorem: SciLean.isomorph.funext
Proof state before:
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
⊢ f = g
Tactic:
funext _
Proof state after:
case h
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ f x✝ = g x✝
Theorem: SciLean.isomorph.funext
Proof state before:
case h
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ f x✝ = g x✝
Tactic:
apply ext tag
Proof state after:
case h.a
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ (IsomorphicType.equiv tag) (f x✝) = (IsomorphicType.equiv tag) (g x✝)
Theorem: SciLean.isomorph.funext
Proof state before:
case h.a
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
x✝ : α
⊢ (IsomorphicType.equiv tag) (f x✝) = (IsomorphicType.equiv tag) (g x✝)
Tactic:
simp[app tag,h]
Proof state after:
no goals
Theorem: SciLean.ContCDiffAt.id_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.2100
inst✝³ : Vec K Y
Z : Type ?u.2111
inst✝² : Vec K Z
ι : Type ?u.2122
inst✝¹ : IndexType ι
E : ι → Type ?u.2131
inst✝ : (i : ι) → Vec K (E i)
x : X
⊢ ContCDiffAt K n (fun x => x) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffAt.const_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.2233
inst✝² : Vec K Z
ι : Type ?u.2244
inst✝¹ : IndexType ι
E : ι → Type ?u.2253
inst✝ : (i : ι) → Vec K (E i)
y : Y
x : X
⊢ ContCDiffAt K n (fun x => y) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffAt.comp_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
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.2388
inst✝¹ : IndexType ι
E : ι → Type ?u.2397
inst✝ : (i : ι) → Vec K (E i)
x : X
f : Y → Z
g : X → Y
hf : ContCDiffAt K n f (g x)
hg : ContCDiffAt K n g x
⊢ ContCDiffAt K n (fun x => f (g x)) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffAt.apply_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type ?u.2558
inst✝⁴ : Vec K X
Y : Type ?u.2571
inst✝³ : Vec K Y
Z : Type ?u.2582
inst✝² : Vec K Z
ι : Type u_2
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
i : ι
x : (i : ι) → E i
⊢ ContCDiffAt K n (fun x => x i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiffAt.pi_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.3297
inst✝³ : Vec K Y
Z : Type ?u.3308
inst✝² : Vec K Z
ι : Type u_4
inst✝¹ : IndexType ι
E : ι → Type u_3
inst✝ : (i : ι) → Vec K (E i)
x : X
f : X → (i : ι) → E i
hf : ∀ (i : ι), ContCDiffAt K n (fun x => f x i) x
⊢ ContCDiffAt K n (fun x i => f x i) x
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ContCDiff.id_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.4740
inst✝³ : Vec K Y
Z : Type ?u.4751
inst✝² : Vec K Z
ι : Type ?u.4762
inst✝¹ : IndexType ι
E : ι → Type ?u.4771
inst✝ : (i : ι) → Vec K (E i)
⊢ ContCDiff K n fun x => x
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.4740
inst✝³ : Vec K Y
Z : Type ?u.4751
inst✝² : Vec K Z
ι : Type ?u.4762
inst✝¹ : IndexType ι
E : ι → Type ?u.4771
inst✝ : (i : ι) → Vec K (E i)
x : X
⊢ ContCDiffAt K n (fun x => x) x
Theorem: SciLean.ContCDiff.id_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type ?u.4740
inst✝³ : Vec K Y
Z : Type ?u.4751
inst✝² : Vec K Z
ι : Type ?u.4762
inst✝¹ : IndexType ι
E : ι → Type ?u.4771
inst✝ : (i : ι) → Vec K (E i)
x : X
⊢ ContCDiffAt K n (fun x => x) x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.ContCDiff.const_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.4904
inst✝² : Vec K Z
ι : Type ?u.4915
inst✝¹ : IndexType ι
E : ι → Type ?u.4924
inst✝ : (i : ι) → Vec K (E i)
y : Y
⊢ ContCDiff K n fun x => y
Tactic:
intro x
Proof state after:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.4904
inst✝² : Vec K Z
ι : Type ?u.4915
inst✝¹ : IndexType ι
E : ι → Type ?u.4924
inst✝ : (i : ι) → Vec K (E i)
y : Y
x : X
⊢ ContCDiffAt K n (fun x => y) x
Theorem: SciLean.ContCDiff.const_rule
Proof state before:
K : Type u_1
inst✝⁵ : RCLike K
n : ℕ∞
X : Type u_2
inst✝⁴ : Vec K X
Y : Type u_3
inst✝³ : Vec K Y
Z : Type ?u.4904
inst✝² : Vec K Z
ι : Type ?u.4915
inst✝¹ : IndexType ι
E : ι → Type ?u.4924
inst✝ : (i : ι) → Vec K (E i)
y : Y
x : X
⊢ ContCDiffAt K n (fun x => y) x
Tactic:
fun_prop
Proof state after:
no goals