internlm/Lean-Github huggingface dataset:
Theorem: modify.arg_f.revDerivM_rule
Proof state before:
case h.h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : SemiInnerProductSpace K S
X : Type
inst✝² : SemiInnerProductSpace K X
Y : Type ?u.264984
inst✝¹ : SemiInnerProductSpace K Y
Z : Type ?u.264995
inst✝ : SemiInnerProductSpace K Z
f : X → S → S
ha0 : HasAdjDiff K fun xs => f xs.1 xs.2
x✝¹ : X
x✝ : S
⊢ pure ((PUnit.unit, fun dx ds => pure ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 ds)), f x✝¹ x✝) =
    pure
      (((), fun x =>
          StateT.bind StateT.get fun __do_lift =>
            StateT.bind (StateT.set ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 __do_lift).2) fun x =>
              StateT.pure ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 __do_lift).1),
        f x✝¹ x✝)
Tactic:
congr
Proof state after:
case h.h.e_a.e_fst.e_snd
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : SemiInnerProductSpace K S
X : Type
inst✝² : SemiInnerProductSpace K X
Y : Type ?u.264984
inst✝¹ : SemiInnerProductSpace K Y
Z : Type ?u.264995
inst✝ : SemiInnerProductSpace K Z
f : X → S → S
ha0 : HasAdjDiff K fun xs => f xs.1 xs.2
x✝¹ : X
x✝ : S
⊢ (fun dx ds => pure ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 ds)) = fun x =>
    StateT.bind StateT.get fun __do_lift =>
      StateT.bind (StateT.set ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 __do_lift).2) fun x =>
        StateT.pure ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 __do_lift).1
Theorem: modify.arg_f.revDerivM_rule
Proof state before:
case h.h.e_a.e_fst.e_snd
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : SemiInnerProductSpace K S
X : Type
inst✝² : SemiInnerProductSpace K X
Y : Type ?u.264984
inst✝¹ : SemiInnerProductSpace K Y
Z : Type ?u.264995
inst✝ : SemiInnerProductSpace K Z
f : X → S → S
ha0 : HasAdjDiff K fun xs => f xs.1 xs.2
x✝¹ : X
x✝ : S
⊢ (fun dx ds => pure ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 ds)) = fun x =>
    StateT.bind StateT.get fun __do_lift =>
      StateT.bind (StateT.set ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 __do_lift).2) fun x =>
        StateT.pure ((revDeriv K (fun x => f x.1 x.2) (x✝¹, x✝)).2 __do_lift).1
Tactic:
funext
Proof state after:
case h.h.e_a.e_fst.e_snd.h.h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : SemiInnerProductSpace K S
X : Type
inst✝² : SemiInnerProductSpace K X
Y : Type ?u.264984
inst✝¹ : SemiInnerProductSpace K Y
Z : Type ?u.264995
inst✝ : SemiInnerProductSpace K Z
f : X → S → S
ha0 : HasAdjDiff K fun xs => f xs.1 xs.2
x✝³ : X
x✝² : S
x✝¹ : PUnit.{1}
x✝ : S
⊢ pure ((revDeriv K (fun x => f x.1 x.2) (x✝³, x✝²)).2 x✝) =
    StateT.bind StateT.get
      (fun __do_lift =>
        StateT.bind (StateT.set ((revDeriv K (fun x => f x.1 x.2) (x✝³, x✝²)).2 __do_lift).2) fun x =>
          StateT.pure ((revDeriv K (fun x => f x.1 x.2) (x✝³, x✝²)).2 __do_lift).1)
      x✝
Theorem: modify.arg_f.revDerivM_rule
Proof state before:
case h.h.e_a.e_fst.e_snd.h.h
K : Type
inst✝⁹ : RCLike K
m : Type → Type
m' : outParam (Type → Type)
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
S : Type
inst✝³ : SemiInnerProductSpace K S
X : Type
inst✝² : SemiInnerProductSpace K X
Y : Type ?u.264984
inst✝¹ : SemiInnerProductSpace K Y
Z : Type ?u.264995
inst✝ : SemiInnerProductSpace K Z
f : X → S → S
ha0 : HasAdjDiff K fun xs => f xs.1 xs.2
x✝³ : X
x✝² : S
x✝¹ : PUnit.{1}
x✝ : S
⊢ pure ((revDeriv K (fun x => f x.1 x.2) (x✝³, x✝²)).2 x✝) =
    StateT.bind StateT.get
      (fun __do_lift =>
        StateT.bind (StateT.set ((revDeriv K (fun x => f x.1 x.2) (x✝³, x✝²)).2 __do_lift).2) fun x =>
          StateT.pure ((revDeriv K (fun x => f x.1 x.2) (x✝³, x✝²)).2 __do_lift).1)
      x✝
Tactic:
simp[StateT.bind,StateT.pure,StateT.get,StateT.set]
Proof state after:
no goals
Theorem: Set.preimage_const'
Proof state before:
α : Type u_2
β : Type u_1
γ : Type ?u.57
b : β
s : Set β
⊢ (fun x => b) ⁻¹' s = if b ∈ s then univ else ∅
Tactic:
apply preimage_const
Proof state after:
no goals
Theorem: Set.HAdd.hAdd.arg_a0.preimage_rule_Ioo
Proof state before:
α : Type ?u.756
β : Type ?u.759
γ : Type ?u.762
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x + x') ⁻¹' Ioo a b = Ioo (a - x') (b - x')
Tactic:
ext
Proof state after:
case h
α : Type ?u.756
β : Type ?u.759
γ : Type ?u.762
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x + x') ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a - x') (b - x')
Theorem: Set.HAdd.hAdd.arg_a0.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.756
β : Type ?u.759
γ : Type ?u.762
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x + x') ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a - x') (b - x')
Tactic:
simp
Proof state after:
case h
α : Type ?u.756
β : Type ?u.759
γ : Type ?u.762
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x✝ + x' ∧ x✝ + x' < b ↔ a - x' < x✝ ∧ x✝ < b - x'
Theorem: Set.HAdd.hAdd.arg_a0.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.756
β : Type ?u.759
γ : Type ?u.762
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x✝ + x' ∧ x✝ + x' < b ↔ a - x' < x✝ ∧ x✝ < b - x'
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Set.HAdd.hAdd.arg_a1.preimage_rule_Ioo
Proof state before:
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x' + x) ⁻¹' Ioo a b = Ioo (a - x') (b - x')
Tactic:
ext
Proof state after:
case h
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' + x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a - x') (b - x')
Theorem: Set.HAdd.hAdd.arg_a1.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' + x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a - x') (b - x')
Tactic:
simp
Proof state after:
case h
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x' + x✝ ∧ x' + x✝ < b ↔ a - x' < x✝ ∧ x✝ < b - x'
Theorem: Set.HAdd.hAdd.arg_a1.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.15024
β : Type ?u.15027
γ : Type ?u.15030
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x' + x✝ ∧ x' + x✝ < b ↔ a - x' < x✝ ∧ x✝ < b - x'
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Set.HSub.hSub.arg_a0.preimage_rule_Ioo
Proof state before:
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x - x') ⁻¹' Ioo a b = Ioo (a + x') (b + x')
Tactic:
ext
Proof state after:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x - x') ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a + x') (b + x')
Theorem: Set.HSub.hSub.arg_a0.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x - x') ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (a + x') (b + x')
Tactic:
simp
Proof state after:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x✝ - x' ∧ x✝ - x' < b ↔ a + x' < x✝ ∧ x✝ < b + x'
Theorem: Set.HSub.hSub.arg_a0.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.28921
β : Type ?u.28924
γ : Type ?u.28927
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x✝ - x' ∧ x✝ - x' < b ↔ a + x' < x✝ ∧ x✝ < b + x'
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Set.HSub.hSub.arg_a1.preimage_rule_Ioo
Proof state before:
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b : R
⊢ (fun x => x' - x) ⁻¹' Ioo a b = Ioo (x' - b) (x' - a)
Tactic:
ext
Proof state after:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' - x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (x' - b) (x' - a)
Theorem: Set.HSub.hSub.arg_a1.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ x✝ ∈ (fun x => x' - x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (x' - b) (x' - a)
Tactic:
simp
Proof state after:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x' - x✝ ∧ x' - x✝ < b ↔ x' - b < x✝ ∧ x✝ < x' - a
Theorem: Set.HSub.hSub.arg_a1.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.44212
β : Type ?u.44215
γ : Type ?u.44218
R : Type u_1
inst✝ : RealScalar R
x' a b x✝ : R
⊢ a < x' - x✝ ∧ x' - x✝ < b ↔ x' - b < x✝ ∧ x✝ < x' - a
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Set.Neg.neg.arg_a1.preimage_rule_Ioo
Proof state before:
α : Type ?u.57741
β : Type ?u.57744
γ : Type ?u.57747
R : Type u_1
inst✝ : RealScalar R
a b : R
⊢ (fun x => -x) ⁻¹' Ioo a b = Ioo (-b) (-a)
Tactic:
ext
Proof state after:
case h
α : Type ?u.57741
β : Type ?u.57744
γ : Type ?u.57747
R : Type u_1
inst✝ : RealScalar R
a b x✝ : R
⊢ x✝ ∈ (fun x => -x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (-b) (-a)
Theorem: Set.Neg.neg.arg_a1.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.57741
β : Type ?u.57744
γ : Type ?u.57747
R : Type u_1
inst✝ : RealScalar R
a b x✝ : R
⊢ x✝ ∈ (fun x => -x) ⁻¹' Ioo a b ↔ x✝ ∈ Ioo (-b) (-a)
Tactic:
simp
Proof state after:
case h
α : Type ?u.57741
β : Type ?u.57744
γ : Type ?u.57747
R : Type u_1
inst✝ : RealScalar R
a b x✝ : R
⊢ a < -x✝ ∧ -x✝ < b ↔ -b < x✝ ∧ x✝ < -a
Theorem: Set.Neg.neg.arg_a1.preimage_rule_Ioo
Proof state before:
case h
α : Type ?u.57741
β : Type ?u.57744
γ : Type ?u.57747
R : Type u_1
inst✝ : RealScalar R
a b x✝ : R
⊢ a < -x✝ ∧ -x✝ < b ↔ -b < x✝ ∧ x✝ < -a
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ConvIf.convIf.id
Proof state before:
α : Sort u_1
P : Prop
inst : Decidable P
a : α
⊢ a = convIf P inst (fun x => a) fun x => a
Tactic:
simp[convIf]
Proof state after:
no goals
Theorem: SciLean.toMatrix.id_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.3131
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.3216
inst✝ : FinVec IZ K Z
⊢ (toMatrix K fun x => x) = fun i j => if i = j then 1 else 0
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.3131
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.3216
inst✝ : FinVec IZ K Z
⊢ (fun i j => ℼ i ((fun x => x) ⅇ j)) = fun i j => if i = j then 1 else 0
Theorem: SciLean.toMatrix.id_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type ?u.3131
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.3216
inst✝ : FinVec IZ K Z
⊢ (fun i j => ℼ i ((fun x => x) ⅇ j)) = fun i j => if i = j then 1 else 0
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.toMatrix.const_zero_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.5477
inst✝ : FinVec IZ K Z
⊢ (toMatrix K fun x => 0) = fun i j => 0
Tactic:
unfold toMatrix
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.5477
inst✝ : FinVec IZ K Z
⊢ (fun i j => ℼ i ((fun x => 0) ⅇ j)) = fun i j => 0
Theorem: SciLean.toMatrix.const_zero_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type u_2
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type ?u.5477
inst✝ : FinVec IZ K Z
⊢ (fun i j => ℼ i ((fun x => 0) ⅇ j)) = fun i j => 0
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.toMatrix.comp_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (toMatrix K fun x => f (g x)) = mulMat (toMatrix K f) (toMatrix K g)
Tactic:
unfold toMatrix mulMat
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f (g x)) ⅇ j)) = fun i j =>
     ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j
Theorem: SciLean.toMatrix.comp_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
⊢ (fun i j => ℼ i ((fun x => f (g x)) ⅇ j)) = fun i j =>
     ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j
Tactic:
funext i j
Proof state after:
case h.h
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢ ℼ i ((fun x => f (g x)) ⅇ j) = ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j
Theorem: SciLean.toMatrix.comp_rule
Proof state before:
case h.h
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢ ℼ i ((fun x => f (g x)) ⅇ j) = ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j
Tactic:
symm
Proof state after:
case h.h
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢  ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j = ℼ i ((fun x => f (g x)) ⅇ j)
Theorem: SciLean.toMatrix.comp_rule
Proof state before:
case h.h
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢  ∑ k, (fun i j => ℼ i (f ⅇ j)) i k * (fun i j => ℼ i (g ⅇ j)) k j = ℼ i ((fun x => f (g x)) ⅇ j)
Tactic:
calc ∑ k, ℼ i (f ⅇ k) * ℼ k (g ⅇ j)
  _ = ℼ i (f (∑ k, ℼ k (g ⅇ j) • ⅇ k)) := by sorry_proof
  _ = ℼ i (f (g ⅇ j)) := by sorry_proof
Proof state after:
no goals
Theorem: SciLean.toMatrix.comp_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢  ∑ k, ℼ i (f ⅇ k) * ℼ k (g ⅇ j) = ℼ i (f ( ∑ k, ℼ k (g ⅇ j) • ⅇ k))
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.toMatrix.comp_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_2
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type u_1
inst✝ : FinVec IZ K Z
f : Y → Z
g : X → Y
hf : IsLinearMap K f
hg : IsLinearMap K g
i : IZ
j : IX
⊢ ℼ i (f ( ∑ k, ℼ k (g ⅇ j) • ⅇ k)) = ℼ i (f (g ⅇ j))
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.toMatrix.apply_rule
Proof state before:
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
⊢ (toMatrix K fun f => f i) = fun ix x =>
    match x with
    | (j, jx) => if j = i ∧ jx = ix then 1 else 0
Tactic:
funext ix (j,jx)
Proof state after:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ toMatrix K (fun f => f i) ix (j, jx) =
    match (j, jx) with
    | (j, jx) => if j = i ∧ jx = ix then 1 else 0
Theorem: SciLean.toMatrix.apply_rule
Proof state before:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ toMatrix K (fun f => f i) ix (j, jx) =
    match (j, jx) with
    | (j, jx) => if j = i ∧ jx = ix then 1 else 0
Tactic:
simp[toMatrix,Basis.basis,Basis.proj]
Proof state after:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ ℼ ix (if j = i then ⅇ jx else 0) = if j = i ∧ jx = ix then 1 else 0
Theorem: SciLean.toMatrix.apply_rule
Proof state before:
case h.h
K : Type
inst✝¹⁵ : RCLike K
IX : Type
inst✝¹⁴ : IndexType IX
inst✝¹³ : LawfulIndexType IX
inst✝¹² : DecidableEq IX
X : Type
inst✝¹¹ : FinVec IX K X
IY : Type
inst✝¹⁰ : IndexType IY
inst✝⁹ : LawfulIndexType IY
inst✝⁸ : DecidableEq IY
Y : Type ?u.17243
inst✝⁷ : FinVec IY K Y
IZ : Type
inst✝⁶ : IndexType IZ
inst✝⁵ : LawfulIndexType IZ
inst✝⁴ : DecidableEq IZ
Z : Type ?u.17328
inst✝³ : FinVec IZ K Z
ι : Type
inst✝² : IndexType ι
inst✝¹ : LawfulIndexType ι
inst✝ : DecidableEq ι
i : ι
ix : IX
j : ι
jx : IX
⊢ ℼ ix (if j = i then ⅇ jx else 0) = if j = i ∧ jx = ix then 1 else 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prod.mk.arg_fstsnd.toMatrix_rule
Proof state before:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_2 u_3)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_2 u_3)
inst✝ : FinVec IZ K Z
g : X → Y
f : X → Z
⊢ (toMatrix K fun x => (g x, f x)) = fun i jx =>
    match i with
    | Sum.inl iy => toMatrix K g iy jx
    | Sum.inr iz => toMatrix K f iz jx
Tactic:
simp[toMatrix,Basis.basis,Basis.proj]
Proof state after:
K : Type
inst✝¹² : RCLike K
IX : Type
inst✝¹¹ : IndexType IX
inst✝¹⁰ : LawfulIndexType IX
inst✝⁹ : DecidableEq IX
X : Type u_1
inst✝⁸ : FinVec IX K X
IY : Type
inst✝⁷ : IndexType IY
inst✝⁶ : LawfulIndexType IY
inst✝⁵ : DecidableEq IY
Y : Type (max u_2 u_3)
inst✝⁴ : FinVec IY K Y
IZ : Type
inst✝³ : IndexType IZ
inst✝² : LawfulIndexType IZ
inst✝¹ : DecidableEq IZ
Z : Type (max u_2 u_3)
inst✝ : FinVec IZ K Z
g : X → Y
f : X → Z
⊢ (toMatrix K fun x => (g x, f x)) = fun i jx =>
    match i with
    | Sum.inl iy => ℼ iy (g ⅇ jx)
    | Sum.inr iz => ℼ iz (f ⅇ jx)