Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute (MLIR/Dialects/LinalgSemantics.lean)

State before:
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ Tensor1D.fill (Tensor1D.extract t extractlen) fillval = Tensor1D.extract (Tensor1D.fill t fillval) extractlen
Tactic:
simp [Tensor1D.fill, Tensor1D.extract]
State after:
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.replicate (min extractlen t.size0) fillval = List.take extractlen (List.replicate t.size0 fillval)

State before:
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.replicate (min extractlen t.size0) fillval = List.take extractlen (List.replicate t.size0 fillval)
Tactic:
apply List.extF
State after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ ∀ (n : ℕ) (h : n < List.length (List.replicate (min extractlen t.size0) fillval)),
    List.getF (List.replicate (min extractlen t.size0) fillval) n h =
      List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
        (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))

State before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ ∀ (n : ℕ) (h : n < List.length (List.replicate (min extractlen t.size0) fillval)),
    List.getF (List.replicate (min extractlen t.size0) fillval) n h =
      List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
        (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
intros n h
State after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
      (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))

State before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
      (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
simp
State after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))

State before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
simp at h
State after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h✝ : n < List.length (List.replicate (min extractlen t.size0) fillval)
h : n < extractlen ∧ n < t.size0
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h✝ =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))

State before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h✝ : n < List.length (List.replicate (min extractlen t.size0) fillval)
h : n < extractlen ∧ n < t.size0
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h✝ =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
sorry
State after:
case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))

State before:
case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
sorry
State after:
no goals