internlm/Lean-Github huggingface dataset:
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof 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 *
Proof 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
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof 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]
Proof state after:
no goals
Theorem: TensorFlatIndex.shapeProd_member_nonzero
Proof state before:
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
⊢ n > 0
Tactic:
have PROD_NONZERO: shapeProd shape > 0 := flat.bound_gt_zero
Proof state after:
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ n > 0
Theorem: TensorFlatIndex.shapeProd_member_nonzero
Proof state before:
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ n > 0
Tactic:
apply shapeProd_nonzero_implies_member_nonzero
Proof state after:
case MEM
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List.Mem n ?xs

case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd ?xs > 0

case xs
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List ℕ
Theorem: TensorFlatIndex.shapeProd_member_nonzero
Proof state before:
case MEM
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List.Mem n ?xs

case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd ?xs > 0

case xs
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List ℕ
Tactic:
exact MEMBER
Proof state after:
case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd shape > 0
Theorem: TensorFlatIndex.shapeProd_member_nonzero
Proof state before:
case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd shape > 0
Tactic:
exact PROD_NONZERO
Proof state after:
no goals
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n / modulus * modulus = n
Tactic:
have MULTIPLE: n = 0 + (n / modulus) * modulus := by {
  rewrite [<- MODZERO];
  rewrite [Nat.mul_comm];
  simp [Nat.mod_add_div];
}
Proof state after:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = 0 + n / modulus * modulus
⊢ n / modulus * modulus = n
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = 0 + n / modulus * modulus
⊢ n / modulus * modulus = n
Tactic:
simp at MULTIPLE
Proof state after:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n / modulus * modulus = n
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n / modulus * modulus = n
Tactic:
rewrite [<- MULTIPLE]
Proof state after:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n = n
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
MULTIPLE : n = n / modulus * modulus
⊢ n = n
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = 0 + n / modulus * modulus
Tactic:
rewrite [<- MODZERO]
Proof state after:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + n / modulus * modulus
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + n / modulus * modulus
Tactic:
rewrite [Nat.mul_comm]
Proof state after:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + modulus * (n / modulus)
Theorem: Nat.mod_zero_implies_div_mul_equal
Proof state before:
n modulus : ℕ
MODZERO : n % modulus = 0
⊢ n = n % modulus + modulus * (n / modulus)
Tactic:
simp [Nat.mod_add_div]
Proof state after:
no goals
Theorem: Nat.mul_cancel_right
Proof state before:
n m : ℕ
MODZERO : n % m = 0
⊢ n / m * m = n
Tactic:
rewrite [Nat.mod_zero_implies_div_mul_equal n m MODZERO]
Proof state after:
n m : ℕ
MODZERO : n % m = 0
⊢ n = n
Theorem: Nat.mul_cancel_right
Proof state before:
n m : ℕ
MODZERO : n % m = 0
⊢ n = n
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.div_lt_if_mod
Proof state before:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix / modulus < bound / modulus
Tactic:
rewrite [Nat.div_lt_iff_lt_mul, Nat.mul_cancel_right]
Proof state after:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix < bound

case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Theorem: Nat.div_lt_if_mod
Proof state before:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix < bound

case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Tactic:
apply IX
Proof state after:
case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Theorem: Nat.div_lt_if_mod
Proof state before:
case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Tactic:
apply DIV
Proof state after:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Theorem: Nat.div_lt_if_mod
Proof state before:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Tactic:
apply MODULUS
Proof state after:
no goals
Theorem: Nat.le_pred_if_lt
Proof state before:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ pred n
Tactic:
cases n
Proof state after:
case zero
x : ℕ
X_LT_N : x < zero
⊢ x ≤ pred zero

case succ
x n✝ : ℕ
X_LT_N : x < succ n✝
⊢ x ≤ pred (succ n✝)
Theorem: Nat.le_pred_if_lt
Proof state before:
x : ℕ
X_LT_N : x < zero
⊢ x ≤ pred zero
Tactic:
case zero => { simp [Nat.not_lt_zero] at X_LT_N; }
Proof state after:
no goals
Theorem: Nat.le_pred_if_lt
Proof state before:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ pred (succ n')
Tactic:
case succ n' => {
 rewrite [Nat.pred_succ];
 apply Nat.le_of_lt_succ;
 exact X_LT_N;
}
Proof state after:
no goals
Theorem: Nat.le_pred_if_lt
Proof state before:
x : ℕ
X_LT_N : x < zero
⊢ x ≤ pred zero
Tactic:
simp [Nat.not_lt_zero] at X_LT_N
Proof state after:
no goals
Theorem: Nat.le_pred_if_lt
Proof state before:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ pred (succ n')
Tactic:
rewrite [Nat.pred_succ]
Proof state after:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ n'
Theorem: Nat.le_pred_if_lt
Proof state before:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ n'
Tactic:
apply Nat.le_of_lt_succ
Proof state after:
case a
x n' : ℕ
X_LT_N : x < succ n'
⊢ x < succ n'
Theorem: Nat.le_pred_if_lt
Proof state before:
case a
x n' : ℕ
X_LT_N : x < succ n'
⊢ x < succ n'
Tactic:
exact X_LT_N
Proof state after:
no goals
Theorem: Nat.le_one_minus_if_lt
Proof state before:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ pred n
Tactic:
rewrite [<- Nat.sub_one]
Proof state after:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ n - 1
Theorem: Nat.le_one_minus_if_lt
Proof state before:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ n - 1
Tactic:
apply Nat.le_pred_if_lt
Proof state after:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < Nat.sub n 0
Theorem: Nat.le_one_minus_if_lt
Proof state before:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < Nat.sub n 0
Tactic:
simp
Proof state after:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < n
Theorem: Nat.le_one_minus_if_lt
Proof state before:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < n
Tactic:
exact X_LT_N
Proof state after:
no goals
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
LE : x ≤ pred n
⊢ x * y ≤ n * y - y
Tactic:
cases H:n
Proof state after:
case zero
x y n : ℕ
LE : x ≤ pred n
H : n = zero
⊢ x * y ≤ zero * y - y

case succ
x y n : ℕ
LE : x ≤ pred n
n✝ : ℕ
H : n = succ n✝
⊢ x * y ≤ succ n✝ * y - y
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
LE : x ≤ pred n
H : n = zero
⊢ x * y ≤ zero * y - y
Tactic:
case zero => {
rewrite [H] at LE;
simp at LE;
rewrite [LE];
simp;
}
Proof state after:
no goals
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
LE : x ≤ pred n
n' : ℕ
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
case succ n' => {
simp at LE;
rewrite [H] at LE;
simp at LE;
sorry; }
Proof state after:
no goals
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
LE : x ≤ pred n
H : n = zero
⊢ x * y ≤ zero * y - y
Tactic:
rewrite [H] at LE
Proof state after:
x y n : ℕ
LE : x ≤ pred zero
H : n = zero
⊢ x * y ≤ zero * y - y
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
LE : x ≤ pred zero
H : n = zero
⊢ x * y ≤ zero * y - y
Tactic:
simp at LE
Proof state after:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ x * y ≤ zero * y - y
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ x * y ≤ zero * y - y
Tactic:
rewrite [LE]
Proof state after:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ 0 * y ≤ zero * y - y
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ 0 * y ≤ zero * y - y
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.le_mul_pred
Proof state before:
x y n : ℕ
LE : x ≤ pred n
n' : ℕ
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
rewrite [H] at LE
Proof state after:
x y n n' : ℕ
LE : x ≤ pred (succ n')
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Theorem: Nat.le_mul_pred
Proof state before:
x y n n' : ℕ
LE : x ≤ pred (succ n')
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
simp at LE
Proof state after:
x y n n' : ℕ
LE : x ≤ n'
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Theorem: Nat.le_mul_pred
Proof state before:
x y n n' : ℕ
LE : x ≤ n'
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
sorry
Proof state after:
no goals
Theorem: List.NonEmpty.empty_absurd
Proof state before:
α : Type
CONTRA : NonEmpty []
⊢ False
Tactic:
cases CONTRA
Proof state after:
no goals
Theorem: TensorIndex'.empty_dims_is_empty
Proof state before:
index : TensorIndex' []
⊢ index = Empty
Tactic:
cases index
Proof state after:
case Empty

⊢ Empty = Empty
Theorem: TensorIndex'.empty_dims_is_empty
Proof state before:
case Empty

⊢ Empty = Empty
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.lt_iff_gt
Proof state before:
⊢ ∀ (a b : ℕ), a < b ↔ b > a
Tactic:
intros a b
Proof state after:
a b : ℕ
⊢ a < b ↔ b > a
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
⊢ a < b ↔ b > a
Tactic:
constructor
Proof state after:
case mp
a b : ℕ
⊢ a < b → b > a

case mpr
a b : ℕ
⊢ b > a → a < b
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
⊢ a < b → b > a
Tactic:
case mp => {
   intros A_LT_B;
   simp [GT.gt]; exact A_LT_B;
}
Proof state after:
no goals
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
⊢ b > a → a < b
Tactic:
case mpr => {
  intros B_GT_A;
  simp [GT.gt] at B_GT_A;
  exact B_GT_A;
}
Proof state after:
no goals
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
⊢ a < b → b > a
Tactic:
intros A_LT_B
Proof state after:
a b : ℕ
A_LT_B : a < b
⊢ b > a
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
A_LT_B : a < b
⊢ b > a
Tactic:
simp [GT.gt]
Proof state after:
a b : ℕ
A_LT_B : a < b
⊢ a < b
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
A_LT_B : a < b
⊢ a < b
Tactic:
exact A_LT_B
Proof state after:
no goals
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
⊢ b > a → a < b
Tactic:
intros B_GT_A
Proof state after:
a b : ℕ
B_GT_A : b > a
⊢ a < b
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
B_GT_A : b > a
⊢ a < b
Tactic:
simp [GT.gt] at B_GT_A
Proof state after:
a b : ℕ
B_GT_A : a < b
⊢ a < b
Theorem: Nat.lt_iff_gt
Proof state before:
a b : ℕ
B_GT_A : a < b
⊢ a < b
Tactic:
exact B_GT_A
Proof state after:
no goals
Theorem: shapeProd_cons_prod
Proof state before:
x y : ℕ
zs : List ℕ
⊢ shapeProd (x :: y :: zs) = shapeProd (x * y :: zs)
Tactic:
simp [Nat.mul_assoc]
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
⊢ ∀ (a b : ℕ), a ≠ 0 → b ≠ 0 → a * b ≠ 0
Tactic:
intros a
Proof state after:
a : ℕ
⊢ ∀ (b : ℕ), a ≠ 0 → b ≠ 0 → a * b ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a : ℕ
⊢ ∀ (b : ℕ), a ≠ 0 → b ≠ 0 → a * b ≠ 0
Tactic:
induction a
Proof state after:
case zero

⊢ ∀ (b : ℕ), zero ≠ 0 → b ≠ 0 → zero * b ≠ 0

case succ
n✝ : ℕ
n_ih✝ : ∀ (b : ℕ), n✝ ≠ 0 → b ≠ 0 → n✝ * b ≠ 0
⊢ ∀ (b : ℕ), succ n✝ ≠ 0 → b ≠ 0 → succ n✝ * b ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
⊢ ∀ (b : ℕ), zero ≠ 0 → b ≠ 0 → zero * b ≠ 0
Tactic:
case zero => {
  intros b A_NEQ_ZERO; simp [A_NEQ_ZERO]; contradiction;
}
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ ∀ (b : ℕ), succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
Tactic:
case succ a' IH => {
  intros b;
  induction b;
  case zero => {
     intros A B;
     simp at B;
  }
  case succ b' IH' => {
   intros A B;
   simp [Nat.mul];
 }
}
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
⊢ ∀ (b : ℕ), zero ≠ 0 → b ≠ 0 → zero * b ≠ 0
Tactic:
intros b A_NEQ_ZERO
Proof state after:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ b ≠ 0 → zero * b ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ b ≠ 0 → zero * b ≠ 0
Tactic:
simp [A_NEQ_ZERO]
Proof state after:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ 0 < b → False
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ 0 < b → False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ ∀ (b : ℕ), succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
Tactic:
intros b
Proof state after:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b : ℕ
⊢ succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b : ℕ
⊢ succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
Tactic:
induction b
Proof state after:
case zero
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ succ a' ≠ 0 → zero ≠ 0 → succ a' * zero ≠ 0

case succ
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
n✝ : ℕ
n_ih✝ : succ a' ≠ 0 → n✝ ≠ 0 → succ a' * n✝ ≠ 0
⊢ succ a' ≠ 0 → succ n✝ ≠ 0 → succ a' * succ n✝ ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ succ a' ≠ 0 → zero ≠ 0 → succ a' * zero ≠ 0
Tactic:
case zero => {
   intros A B;
   simp at B;
}
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
⊢ succ a' ≠ 0 → succ b' ≠ 0 → succ a' * succ b' ≠ 0
Tactic:
case succ b' IH' => {
 intros A B;
 simp [Nat.mul];
}
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ succ a' ≠ 0 → zero ≠ 0 → succ a' * zero ≠ 0
Tactic:
intros A B
Proof state after:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
A : succ a' ≠ 0
B : zero ≠ 0
⊢ succ a' * zero ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
A : succ a' ≠ 0
B : zero ≠ 0
⊢ succ a' * zero ≠ 0
Tactic:
simp at B
Proof state after:
no goals
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
⊢ succ a' ≠ 0 → succ b' ≠ 0 → succ a' * succ b' ≠ 0
Tactic:
intros A B
Proof state after:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
A : succ a' ≠ 0
B : succ b' ≠ 0
⊢ succ a' * succ b' ≠ 0
Theorem: Nat.mul_of_nonzero_is_nonzero
Proof state before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
A : succ a' ≠ 0
B : succ b' ≠ 0
⊢ succ a' * succ b' ≠ 0
Tactic:
simp [Nat.mul]
Proof state after:
no goals
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + List.length xs = bound), List.length xs = List.length (zipFlatIndexGo xs ix bound H)
Tactic:
induction xs
Proof state after:
case nil
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + List.length [] = bound), List.length [] = List.length (zipFlatIndexGo [] ix bound H)

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (ix bound : ℕ) (H : ix + List.length tail✝ = bound),
    List.length tail✝ = List.length (zipFlatIndexGo tail✝ ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (head✝ :: tail✝) = bound),
    List.length (head✝ :: tail✝) = List.length (zipFlatIndexGo (head✝ :: tail✝) ix bound H)
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + List.length [] = bound), List.length [] = List.length (zipFlatIndexGo [] ix bound H)
Tactic:
case nil => {
  intros; unfold zipFlatIndexGo; rfl;
}
Proof state after:
no goals
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (x :: xs') = bound),
    List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Tactic:
case cons x xs' IND => {
  intros ix bound H;
  simp [zipFlatIndexGo];
  apply IND;
}
Proof state after:
no goals
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + List.length [] = bound), List.length [] = List.length (zipFlatIndexGo [] ix bound H)
Tactic:
intros
Proof state after:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length (zipFlatIndexGo [] ix✝ bound✝ H✝)
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length (zipFlatIndexGo [] ix✝ bound✝ H✝)
Tactic:
unfold zipFlatIndexGo
Proof state after:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length []
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length []
Tactic:
rfl
Proof state after:
no goals
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (x :: xs') = bound),
    List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Tactic:
intros ix bound H
Proof state after:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Tactic:
simp [zipFlatIndexGo]
Proof state after:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length xs' = List.length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + List.length xs' = bound))
Theorem: zip_flat_index_go_length
Proof state before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length xs' = List.length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + List.length xs' = bound))
Tactic:
apply IND
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof state before:
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < bound
Tactic:
rewrite [<- H]
Proof state after:
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < ix + length xs
Theorem: List.zip_flat_index_go_get
Proof state before:
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < ix + length xs
Tactic:
simp [Nat.add_lt_add_left, GETIX]
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof state before:
α : Type u_1
⊢ ∀ (xs : List α) (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
intros xs
Proof state after:
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Theorem: List.zip_flat_index_go_get
Proof state before:
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
induction xs
Proof state after:
case nil
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + length [] = bound) (deltaIx : ℕ) (GETIX : deltaIx < length []),
    getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
      (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (ix bound : ℕ) (H : ix + length tail✝ = bound) (deltaIx : ℕ) (GETIX : deltaIx < length tail✝),
    getF (zipFlatIndexGo tail✝ ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo tail✝ ix bound H)) =
      (getF tail✝ deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
⊢ ∀ (ix bound : ℕ) (H : ix + length (head✝ :: tail✝) = bound) (deltaIx : ℕ) (GETIX : deltaIx < length (head✝ :: tail✝)),
    getF (zipFlatIndexGo (head✝ :: tail✝) ix bound H) deltaIx
        (_ : deltaIx < length (zipFlatIndexGo (head✝ :: tail✝) ix bound H)) =
      (getF (head✝ :: tail✝) deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })