Theorem: shapeProd_nonzero_implies_member_nonzero (MLIR/Util/KDTensor.lean)

State before:
⊢ ∀ (xs : List ℕ) (x : ℕ), List.Mem x xs → shapeProd xs > 0 → x > 0
Tactic:
intros xs x MEM
State after:
xs : List ℕ
x : ℕ
MEM : List.Mem x xs
⊢ shapeProd xs > 0 → x > 0

State before:
xs : List ℕ
x : ℕ
MEM : List.Mem x xs
⊢ shapeProd xs > 0 → x > 0
Tactic:
induction MEM
State after:
case head
xs : List ℕ
x : ℕ
as✝ : List ℕ
⊢ shapeProd (x :: as✝) > 0 → x > 0

case tail
xs : List ℕ
x b✝ : ℕ
as✝ : List ℕ
a✝ : List.Mem x as✝
a_ih✝ : shapeProd as✝ > 0 → x > 0
⊢ shapeProd (b✝ :: as✝) > 0 → x > 0

State before:
xs : List ℕ
x : ℕ
as : List ℕ
⊢ shapeProd (x :: as) > 0 → x > 0
Tactic:
case head as => {
  simp [shapeProd, List.foldr];
  intros H H2;
  apply H;
}
State after:
no goals

State before:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
⊢ shapeProd (b :: bs) > 0 → x > 0
Tactic:
case tail b bs MEM IH => {
  intros H;
  apply IH;
  simp at H;
  rewrite [<- Nat.nonzero_iff_gt_zero] at *;
  simp[H];
}
State after:
no goals

State before:
xs : List ℕ
x : ℕ
as : List ℕ
⊢ shapeProd (x :: as) > 0 → x > 0
Tactic:
simp [shapeProd, List.foldr]
State after:
xs : List ℕ
x : ℕ
as : List ℕ
⊢ 0 < x → 0 < List.foldr (fun x x_1 => x * x_1) 1 as → 0 < x

State before:
xs : List ℕ
x : ℕ
as : List ℕ
⊢ 0 < x → 0 < List.foldr (fun x x_1 => x * x_1) 1 as → 0 < x
Tactic:
intros H H2
State after:
xs : List ℕ
x : ℕ
as : List ℕ
H : 0 < x
H2 : 0 < List.foldr (fun x x_1 => x * x_1) 1 as
⊢ 0 < x

State before:
xs : List ℕ
x : ℕ
as : List ℕ
H : 0 < x
H2 : 0 < List.foldr (fun x x_1 => x * x_1) 1 as
⊢ 0 < x
Tactic:
apply H
State after:
no goals

State before:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
⊢ shapeProd (b :: bs) > 0 → x > 0
Tactic:
intros H
State after:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
H : shapeProd (b :: bs) > 0
⊢ x > 0

State before:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
H : shapeProd (b :: bs) > 0
⊢ x > 0
Tactic:
apply IH
State after:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
H : shapeProd (b :: bs) > 0
⊢ shapeProd bs > 0

State before:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
H : shapeProd (b :: bs) > 0
⊢ shapeProd bs > 0
Tactic:
simp at H
State after:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
H : 0 < b ∧ 0 < shapeProd bs
⊢ shapeProd bs > 0

State before:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
H : 0 < b ∧ 0 < shapeProd bs
⊢ shapeProd bs > 0
Tactic:
rewrite [<- Nat.nonzero_iff_gt_zero] at *
State after:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs ≠ 0 → x > 0
H : 0 < b ∧ 0 < shapeProd bs
⊢ shapeProd bs ≠ 0

State before:
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs ≠ 0 → x > 0
H : 0 < b ∧ 0 < shapeProd bs
⊢ shapeProd bs ≠ 0
Tactic:
simp[H]
State after:
no goals