Theorem: LeanColls.Indexed.set.arg_contelem.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
idx : Idx
⊢ IsLinearMap R fun x =>
    match x with
    | (cont, elem) => set cont idx elem
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
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem

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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem

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
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem

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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
Tactic:
. intros; simp; ext; sorry_proof
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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem

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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
Tactic:
. intros; simp; ext; sorry_proof
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
idx : Idx
⊢ ∀ (x y : Cont × Elem),
    (match x + y with
      | (cont, elem) => set cont idx elem) =
      (match x with
        | (cont, elem) => set cont idx elem) +
        match y with
        | (cont, elem) => set cont idx elem
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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ (match x✝ + y✝ with
    | (cont, elem) => set cont idx elem) =
    (match x✝ with
      | (cont, elem) => set cont idx elem) +
      match y✝ with
      | (cont, elem) => set cont idx elem

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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ (match x✝ + y✝ with
    | (cont, elem) => set cont idx elem) =
    (match x✝ with
      | (cont, elem) => set cont idx elem) +
      match y✝ with
      | (cont, elem) => set cont idx elem
Tactic:
simp
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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2) = set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2

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
idx : Idx
x✝ y✝ : Cont × Elem
⊢ set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2) = set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2
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
idx : Idx
x✝ y✝ : Cont × Elem
i✝ : Idx
⊢ (set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2))[i✝] = (set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2)[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
idx : Idx
x✝ y✝ : Cont × Elem
i✝ : Idx
⊢ (set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2))[i✝] = (set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2)[i✝]
Tactic:
sorry_proof
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
idx : Idx
⊢ ∀ (c : R) (x : Cont × Elem),
    (match c • x with
      | (cont, elem) => set cont idx elem) =
      c •
        match x with
        | (cont, elem) => set cont idx elem
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
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ (match c✝ • x✝ with
    | (cont, elem) => set cont idx elem) =
    c✝ •
      match x✝ with
      | (cont, elem) => set cont idx elem

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
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ (match c✝ • x✝ with
    | (cont, elem) => set cont idx elem) =
    c✝ •
      match x✝ with
      | (cont, elem) => set cont idx elem
Tactic:
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
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ set (c✝ • x✝.1) idx (c✝ • x✝.2) = c✝ • set x✝.1 idx x✝.2

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
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ set (c✝ • x✝.1) idx (c✝ • x✝.2) = c✝ • set x✝.1 idx x✝.2
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
idx : Idx
c✝ : R
x✝ : Cont × Elem
i✝ : Idx
⊢ (set (c✝ • x✝.1) idx (c✝ • x✝.2))[i✝] = (c✝ • set x✝.1 idx x✝.2)[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
idx : Idx
c✝ : R
x✝ : Cont × Elem
i✝ : Idx
⊢ (set (c✝ • x✝.1) idx (c✝ • x✝.2))[i✝] = (c✝ • set x✝.1 idx x✝.2)[i✝]
Tactic:
sorry_proof
State after:
no goals