Theorem: DimList.dim_known_prod_refines (MLIR/Semantics/TensorElem.lean)

State before:
S : List ℕ
D : DimList
⊢ known D = true → shapeRefines S D = true → shapeProd S = prod D
Tactic:
intros Hknown
State after:
S : List ℕ
D : DimList
Hknown : known D = true
⊢ shapeRefines S D = true → shapeProd S = prod D

State before:
S : List ℕ
D : DimList
Hknown : known D = true
⊢ shapeRefines S D = true → shapeProd S = prod D
Tactic:
revert S
State after:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → shapeProd S = prod D

State before:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → shapeProd S = prod D
Tactic:
induction D <;> intros S Hrefines <;> simp
State after:
case nil
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ shapeProd S = 1

case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → ∀ {S : List ℕ}, shapeRefines S tail✝ = true → shapeProd S = prod tail✝
Hknown : known (head✝ :: tail✝) = true
S : List ℕ
Hrefines : shapeRefines S (head✝ :: tail✝) = true
⊢ shapeProd S = prod (head✝ :: tail✝)

State before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ shapeProd S = 1
Tactic:
case nil =>
  cases S; simp; simp at Hrefines
State after:
no goals

State before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ shapeProd S = prod (head :: tail)
Tactic:
case cons head tail ih =>
  cases S; simp at Hrefines
  cases head <;> simp at *
  rw [←Hrefines.1, ←ih Hknown Hrefines.2]
State after:
no goals

State before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ shapeProd S = 1
Tactic:
cases S
State after:
case nil
Hknown : known [] = true
Hrefines : shapeRefines [] [] = true
⊢ shapeProd [] = 1

case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ shapeProd (head✝ :: tail✝) = 1

State before:
case nil
Hknown : known [] = true
Hrefines : shapeRefines [] [] = true
⊢ shapeProd [] = 1

case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ shapeProd (head✝ :: tail✝) = 1
Tactic:
simp
State after:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ shapeProd (head✝ :: tail✝) = 1

State before:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ shapeProd (head✝ :: tail✝) = 1
Tactic:
simp at Hrefines
State after:
no goals

State before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ shapeProd S = prod (head :: tail)
Tactic:
cases S
State after:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ shapeProd [] = prod (head :: tail)

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)

State before:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ shapeProd [] = prod (head :: tail)

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)
Tactic:
simp at Hrefines
State after:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)

State before:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ shapeProd (head✝ :: tail✝) = prod (head :: tail)
Tactic:
cases head <;> simp at *
State after:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ head✝ * shapeProd tail✝ = a✝ * prod tail

State before:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → shapeProd S = prod tail
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ head✝ * shapeProd tail✝ = a✝ * prod tail
Tactic:
rw [←Hrefines.1, ←ih Hknown Hrefines.2]
State after:
no goals