Theorem: LeanColls.Indexed.ofFn.arg_f.IsLinearMap_rule_simple (SciLean/Data/ArrayType/Properties.lean)

State before:
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ IsLinearMap R fun f => ofFn f
Tactic:
constructor
State after:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (x y : Idx → Elem), ofFn (x + y) = ofFn x + ofFn y

case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x

State before:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (x y : Idx → Elem), ofFn (x + y) = ofFn x + ofFn y

case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Tactic:
. intros; ext; simp
State after:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x

State before:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Tactic:
. intros; ext; simp
State after:
no goals

State before:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (x y : Idx → Elem), ofFn (x + y) = ofFn x + ofFn y
Tactic:
intros
State after:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
⊢ ofFn (x✝ + y✝) = ofFn x✝ + ofFn y✝

State before:
case map_add
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
⊢ ofFn (x✝ + y✝) = ofFn x✝ + ofFn y✝
Tactic:
ext
State after:
case map_add.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (x✝ + y✝))[i✝] = (ofFn x✝ + ofFn y✝)[i✝]

State before:
case map_add.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
x✝ y✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (x✝ + y✝))[i✝] = (ofFn x✝ + ofFn y✝)[i✝]
Tactic:
simp
State after:
no goals

State before:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
⊢ ∀ (c : R) (x : Idx → Elem), ofFn (c • x) = c • ofFn x
Tactic:
intros
State after:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
⊢ ofFn (c✝ • x✝) = c✝ • ofFn x✝

State before:
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
⊢ ofFn (c✝ • x✝) = c✝ • ofFn x✝
Tactic:
ext
State after:
case map_smul.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (c✝ • x✝))[i✝] = (c✝ • ofFn x✝)[i✝]

State before:
case map_smul.a
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
c✝ : R
x✝ : Idx → Elem
i✝ : Idx
⊢ (ofFn (c✝ • x✝))[i✝] = (c✝ • ofFn x✝)[i✝]
Tactic:
simp
State after:
no goals