Theorem: BubbleUpExtractSlice.bubble_up_extract_slice (MLIR/Dialects/LinalgSemantics.lean)

State before:
M : Type → Type
len : ℕ
MM : Monad M
LM : LawfulMonad M
t : Tensor1D
f : FinInt 32 → M (FinInt 32)
⊢ (fun s => Tensor1D.extract s len) <$> Tensor1D.mapM t f = Tensor1D.mapM (Tensor1D.extract t len) f
Tactic:
cases t
State after:
case mk
M : Type → Type
len : ℕ
MM : Monad M
LM : LawfulMonad M
f : FinInt 32 → M (FinInt 32)
size0✝ : ℕ
data✝ : List (FinInt 32)
h_data_size✝ : List.length data✝ = size0✝
⊢ (fun s => Tensor1D.extract s len) <$>
      Tensor1D.mapM { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } f =
    Tensor1D.mapM (Tensor1D.extract { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } len) f

State before:
case mk
M : Type → Type
len : ℕ
MM : Monad M
LM : LawfulMonad M
f : FinInt 32 → M (FinInt 32)
size0✝ : ℕ
data✝ : List (FinInt 32)
h_data_size✝ : List.length data✝ = size0✝
⊢ (fun s => Tensor1D.extract s len) <$>
      Tensor1D.mapM { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } f =
    Tensor1D.mapM (Tensor1D.extract { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } len) f
Tactic:
sorry
State after:
no goals