internlm/Lean-Github huggingface dataset:
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) s = true
Tactic:
rw [Hs]
Proof state after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H
s_tail : List ℕ
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
rw [Hs] at H
Proof state after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H✝
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
H' : ∃ tail, s = List.length l :: tail := inferredShape_list_to_cons H✝
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
Hs : s = List.length l :: s_tail
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
clear Hs H'
Proof state after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
let H' := inferredShape_list H
Proof state after:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
H' : List.length l = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (List.all l fun x => decide (inferredShape x = some s)) = true → (List.all l fun x => hasShape x s) = true
s : List ℕ
H✝ : inferredShape (nested l) = some s
s_tail : List ℕ
H : inferredShape (nested l) = some (List.length l :: s_tail)
H' : List.length l = List.length l ∧ (List.all l fun x => decide (inferredShape x = some s_tail)) = true :=
  inferredShape_list H
⊢ hasShape (nested l) (List.length l :: s_tail) = true
Tactic:
simp [hasShape, motive_2 _ H'.2]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (s : List ℕ), inferredShape empty = some s → hasShape empty s = true
Tactic:
simp [inferredShape]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (s : List ℕ),
    (List.all [] fun x => decide (inferredShape x = some s)) = true → (List.all [] fun x => hasShape x s) = true
Tactic:
intros s H
Proof state after:
e : TensorElem
s : List ℕ
H : (List.all [] fun x => decide (inferredShape x = some s)) = true
⊢ (List.all [] fun x => hasShape x s) = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
s : List ℕ
H : (List.all [] fun x => decide (inferredShape x = some s)) = true
⊢ (List.all [] fun x => hasShape x s) = true
Tactic:
simp [List.all_nil]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e : TensorElem
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true) →
      (∀ (s : List ℕ),
          (List.all tail fun x => decide (inferredShape x = some s)) = true →
            (List.all tail fun x => hasShape x s) = true) →
        ∀ (s : List ℕ),
          (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true →
            (List.all (head :: tail) fun x => hasShape x s) = true
Tactic:
intros head tail motive_1 ih s H
Proof state after:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
ih :
  ∀ (s : List ℕ),
    (List.all tail fun x => decide (inferredShape x = some s)) = true → (List.all tail fun x => hasShape x s) = true
s : List ℕ
H : (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true
⊢ (List.all (head :: tail) fun x => hasShape x s) = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
ih :
  ∀ (s : List ℕ),
    (List.all tail fun x => decide (inferredShape x = some s)) = true → (List.all tail fun x => hasShape x s) = true
s : List ℕ
H : (List.all (head :: tail) fun x => decide (inferredShape x = some s)) = true
⊢ (List.all (head :: tail) fun x => hasShape x s) = true
Tactic:
simp [List.all_cons] at *
Proof state after:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ hasShape head s = true ∧ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ hasShape head s = true ∧ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Tactic:
simp [motive_1 _ H.1, ih _ H.2]
Proof state after:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Theorem: MLIR.AST.TensorElem.hasShape_inferredShape
Proof state before:
e head : TensorElem
tail : List TensorElem
motive_1 : ∀ (s : List ℕ), inferredShape head = some s → hasShape head s = true
s : List ℕ
ih :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → inferredShape x = some s) → ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
H : inferredShape head = some s ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s
⊢ ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Tactic:
sorry
Proof state after:
no goals
Theorem: DimList.dim_lift_refines
Proof state before:
S : List ℕ
⊢ shapeRefines S (List.map Dimension.Known S) = true
Tactic:
induction S <;> simp
Proof state after:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
⊢ shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
Theorem: DimList.dim_lift_refines
Proof state before:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
⊢ shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
Tactic:
assumption
Proof state after:
no goals
Theorem: DimList.dim_known_project_refines
Proof state before:
D : DimList
⊢ known D = true → shapeRefines (project D) D = true
Tactic:
intros h <;> induction D <;> simp
Proof state after:
case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → shapeRefines (project tail✝) tail✝ = true
h : known (head✝ :: tail✝) = true
⊢ shapeRefines (project (head✝ :: tail✝)) (head✝ :: tail✝) = true
Theorem: DimList.dim_known_project_refines
Proof state before:
head : Dimension
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
h : known (head :: tail) = true
⊢ shapeRefines (project (head :: tail)) (head :: tail) = true
Tactic:
case cons head tail ih =>
  cases head <;> simp at *; apply (ih h)
Proof state after:
no goals
Theorem: DimList.dim_known_project_refines
Proof state before:
head : Dimension
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
h : known (head :: tail) = true
⊢ shapeRefines (project (head :: tail)) (head :: tail) = true
Tactic:
cases head <;> simp at *
Proof state after:
case Known
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
a✝ : ℕ
h : known tail = true
⊢ shapeRefines (project tail) tail = true
Theorem: DimList.dim_known_project_refines
Proof state before:
case Known
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
a✝ : ℕ
h : known tail = true
⊢ shapeRefines (project tail) tail = true
Tactic:
apply (ih h)
Proof state after:
no goals
Theorem: DimList.dim_known_refines_inv
Proof state before:
D : DimList
S : List ℕ
⊢ known D = true → shapeRefines S D = true → D = List.map Dimension.Known S
Tactic:
intros Hknown
Proof state after:
D : DimList
S : List ℕ
Hknown : known D = true
⊢ shapeRefines S D = true → D = List.map Dimension.Known S
Theorem: DimList.dim_known_refines_inv
Proof state before:
D : DimList
S : List ℕ
Hknown : known D = true
⊢ shapeRefines S D = true → D = List.map Dimension.Known S
Tactic:
revert S
Proof state after:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → D = List.map Dimension.Known S
Theorem: DimList.dim_known_refines_inv
Proof state before:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → D = List.map Dimension.Known S
Tactic:
induction D <;> intros S Hrefines
Proof state after:
case nil
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ [] = List.map Dimension.Known S

case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → ∀ {S : List ℕ}, shapeRefines S tail✝ = true → tail✝ = List.map Dimension.Known S
Hknown : known (head✝ :: tail✝) = true
S : List ℕ
Hrefines : shapeRefines S (head✝ :: tail✝) = true
⊢ head✝ :: tail✝ = List.map Dimension.Known S
Theorem: DimList.dim_known_refines_inv
Proof state before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ [] = List.map Dimension.Known S
Tactic:
case nil =>
  cases S; simp [List.map]; simp at Hrefines
Proof state after:
no goals
Theorem: DimList.dim_known_refines_inv
Proof state before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known S
Tactic:
case cons head tail ih =>
  cases S; simp at Hrefines
  simp [List.map]; cases head <;> simp at *
  rw [Hrefines.1, ←ih Hknown]; apply Hrefines.2
Proof state after:
no goals
Theorem: DimList.dim_known_refines_inv
Proof state before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ [] = List.map Dimension.Known S
Tactic:
cases S
Proof state after:
case nil
Hknown : known [] = true
Hrefines : shapeRefines [] [] = true
⊢ [] = List.map Dimension.Known []

case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)
Theorem: DimList.dim_known_refines_inv
Proof state before:
case nil
Hknown : known [] = true
Hrefines : shapeRefines [] [] = true
⊢ [] = List.map Dimension.Known []

case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp [List.map]
Proof state after:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)
Theorem: DimList.dim_known_refines_inv
Proof state before:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp at Hrefines
Proof state after:
no goals
Theorem: DimList.dim_known_refines_inv
Proof state before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known S
Tactic:
cases S
Proof state after:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known []

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
Theorem: DimList.dim_known_refines_inv
Proof state before:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known []

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp at Hrefines
Proof state after:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
Theorem: DimList.dim_known_refines_inv
Proof state before:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp [List.map]
Proof state after:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝
Theorem: DimList.dim_known_refines_inv
Proof state before:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝
Tactic:
cases head <;> simp at *
Proof state after:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ Dimension.Known a✝ :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝
Theorem: DimList.dim_known_refines_inv
Proof state before:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ Dimension.Known a✝ :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝
Tactic:
rw [Hrefines.1, ←ih Hknown]
Proof state after:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ shapeRefines tail✝ tail = true
Theorem: DimList.dim_known_refines_inv
Proof state before:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ shapeRefines tail✝ tail = true
Tactic:
apply Hrefines.2
Proof state after:
no goals
Theorem: DimList.dim_known_project_eq
Proof state before:
S : List ℕ
D : DimList
⊢ known D = true → shapeRefines S D = true → project D = S
Tactic:
intros Hknown Hrefines
Proof state after:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project D = S
Theorem: DimList.dim_known_project_eq
Proof state before:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project D = S
Tactic:
rw [dim_known_refines_inv Hknown Hrefines]
Proof state after:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project (List.map Dimension.Known S) = S
Theorem: DimList.dim_known_project_eq
Proof state before:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project (List.map Dimension.Known S) = S
Tactic:
clear D Hknown Hrefines
Proof state after:
S : List ℕ
⊢ project (List.map Dimension.Known S) = S
Theorem: DimList.dim_known_project_eq
Proof state before:
S : List ℕ
⊢ project (List.map Dimension.Known S) = S
Tactic:
induction S <;> simp
Proof state after:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : project (List.map Dimension.Known tail✝) = tail✝
⊢ project (List.map Dimension.Known tail✝) = tail✝
Theorem: DimList.dim_known_project_eq
Proof state before:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : project (List.map Dimension.Known tail✝) = tail✝
⊢ project (List.map Dimension.Known tail✝) = tail✝
Tactic:
assumption
Proof state after:
no goals
Theorem: DimList.dim_known_prod_refines
Proof state before:
S : List ℕ
D : DimList
⊢ known D = true → shapeRefines S D = true → shapeProd S = prod D
Tactic:
intros Hknown
Proof state after:
S : List ℕ
D : DimList
Hknown : known D = true
⊢ shapeRefines S D = true → shapeProd S = prod D
Theorem: DimList.dim_known_prod_refines
Proof state before:
S : List ℕ
D : DimList
Hknown : known D = true
⊢ shapeRefines S D = true → shapeProd S = prod D
Tactic:
revert S
Proof state after:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → shapeProd S = prod D
Theorem: DimList.dim_known_prod_refines
Proof 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
Proof 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✝)
Theorem: DimList.dim_known_prod_refines
Proof state before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ shapeProd S = 1
Tactic:
case nil =>
  cases S; simp; simp at Hrefines
Proof state after:
no goals
Theorem: DimList.dim_known_prod_refines
Proof 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]
Proof state after:
no goals
Theorem: DimList.dim_known_prod_refines
Proof state before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ shapeProd S = 1
Tactic:
cases S
Proof 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
Theorem: DimList.dim_known_prod_refines
Proof 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
Proof state after:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ shapeProd (head✝ :: tail✝) = 1
Theorem: DimList.dim_known_prod_refines
Proof state before:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ shapeProd (head✝ :: tail✝) = 1
Tactic:
simp at Hrefines
Proof state after:
no goals