internlm/Lean-Github huggingface dataset:
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n✝ : ℕ
hn : ∀ p > n✝, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
n : ℕ
⊢ n ∈ s.erase 3 → n.Prime
Tactic:
simp [← hs n]
Proof state after:
n✝ : ℕ
hn : ∀ p > n✝, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
n : ℕ
⊢ ¬n = 3 → n.Prime → n % 4 = 3 → n.Prime
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n✝ : ℕ
hn : ∀ p > n✝, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
n : ℕ
⊢ ¬n = 3 → n.Prime → n % 4 = 3 → n.Prime
Tactic:
tauto
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∣ 4 * ∏ i ∈ s.erase 3, i
Tactic:
apply dvd_trans _ (dvd_mul_left _ _)
Proof state after:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∣ ∏ i ∈ s.erase 3, i
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∣ ∏ i ∈ s.erase 3, i
Tactic:
apply dvd_prod_of_mem
Proof state after:
case ha
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∈ s.erase 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case ha
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∈ s.erase 3
Tactic:
simp
Proof state after:
case ha
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ ¬p = 3 ∧ p ∈ s
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case ha
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ ¬p = 3 ∧ p ∈ s
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i ∈ s.erase 3, i
⊢ p ∣ 3
Tactic:
convert Nat.dvd_sub' pdvd this
Proof state after:
case h.e'_4
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i ∈ s.erase 3, i
⊢ 3 = 4 * ∏ i ∈ s.erase 3, i + 3 - 4 * ∏ i ∈ s.erase 3, i
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h.e'_4
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i ∈ s.erase 3, i
⊢ 3 = 4 * ∏ i ∈ s.erase 3, i + 3 - 4 * ∏ i ∈ s.erase 3, i
Tactic:
simp
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i ∈ s.erase 3, i
this : p ∣ 3
⊢ p = 3
Tactic:
apply pp.eq_of_dvd_of_prime Nat.prime_three this
Proof state after:
no goals
Theorem: C03S04.aux
Proof state before:
x y : ℝ
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S04.auxαα
Proof state before:
x y : ℝ
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 = 0
Tactic:
linarith [pow_two_nonneg x, pow_two_nonneg y]
Proof state after:
no goals
Theorem: C03S04.not_monotone_iff
Proof state before:
f : ℝ → ℝ
⊢ ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y
Tactic:
rw [Monotone]
Proof state after:
f : ℝ → ℝ
⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y
Theorem: C03S04.not_monotone_iff
Proof state before:
f : ℝ → ℝ
⊢ (¬∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b) ↔ ∃ x y, x ≤ y ∧ f x > f y
Tactic:
push_neg
Proof state after:
f : ℝ → ℝ
⊢ (∃ a b, a ≤ b ∧ f b < f a) ↔ ∃ x y, x ≤ y ∧ f x > f y
Theorem: C03S04.not_monotone_iff
Proof state before:
f : ℝ → ℝ
⊢ (∃ a b, a ≤ b ∧ f b < f a) ↔ ∃ x y, x ≤ y ∧ f x > f y
Tactic:
rfl
Proof state after:
no goals
Theorem: inv_mul_cancel_left
Proof state before:
G : Type
inv : G → G
mul : G → G → G
one : G
assocMul : ∀ (a b c : G), mul a (mul b c) = mul (mul a b) c
invLeft : ∀ (a : G), mul (inv a) a = one
mulOne : ∀ (a : G), mul a one = a
oneMul : ∀ (a : G), mul one a = a
invRight : ∀ (a : G), mul a (inv a) = one
x y : G
⊢ mul (inv x) (mul x y) = y
Tactic:
simp [assocMul, invLeft, mulOne, oneMul, invRight]
Proof state after:
no goals
Theorem: mul_inv_cancel_left
Proof state before:
G : Type
inv : G → G
mul : G → G → G
one : G
assocMul : ∀ (a b c : G), mul a (mul b c) = mul (mul a b) c
invLeft : ∀ (a : G), mul (inv a) a = one
mulOne : ∀ (a : G), mul a one = a
oneMul : ∀ (a : G), mul one a = a
invRight : ∀ (a : G), mul a (inv a) = one
x y : G
⊢ mul x (mul (inv x) y) = y
Tactic:
simp [assocMul, invLeft, mulOne, oneMul, invRight]
Proof state after:
no goals
Theorem: Test.append_assoc
Proof state before:
α : Type u_1
as bs cs : List α
⊢ as ++ bs ++ cs = as ++ (bs ++ cs)
Tactic:
induction as with
| nil => eggxplosion [append_nil, append_cons]
| cons a as ih => eggxplosion [ih, append_nil, append_cons]
Proof state after:
no goals
Theorem: Test.reverseAux_eq_append
Proof state before:
α : Type u_1
as bs : List α
⊢ reverseAux as bs = reverseAux as [] ++ bs
Tactic:
induction as generalizing bs with
| nil => eggxplosion [reverseAux_nil, reverseAux_cons]
| cons a as ih =>
  eggxplosion [reverseAux_nil, reverseAux_cons, append_assoc]
Proof state after:
no goals
Theorem: Test.reverse_append
Proof state before:
α : Type u_1
as bs : List α
⊢ List.reverse (as ++ bs) = List.reverse bs ++ List.reverse as
Tactic:
induction as generalizing bs with
| nil => eggxplosion []
| cons a as ih => eggxplosion [ih, append_assoc]
Proof state after:
no goals
Theorem: Test.all_deforestation
Proof state before:
α : Sort u_1
⊢ ∀ (p : α → Bool) (xs : List α), all p xs = all' p xs
Tactic:
intros p xs
Proof state after:
α : Sort u_1
p : α → Bool
xs : List α
⊢ all p xs = all' p xs
Theorem: Test.all_deforestation
Proof state before:
α : Sort u_1
p : α → Bool
xs : List α
⊢ all p xs = all' p xs
Tactic:
induction xs with
| nil => simp [all, all', List.foldr, List.map]
| cons a as ih => simp [all, all', List.foldr, List.map, ih]
Proof state after:
no goals
Theorem: Test.all_deforestation
Proof state before:
case nil
α : Sort u_1
p : α → Bool
⊢ all p [] = all' p []
Tactic:
simp [all, all', List.foldr, List.map]
Proof state after:
no goals
Theorem: Test.all_deforestation
Proof state before:
case cons
α : Sort u_1
p : α → Bool
a : α
as : List α
ih : all p as = all' p as
⊢ all p (a::as) = all' p (a::as)
Tactic:
simp [all, all', List.foldr, List.map, ih]
Proof state after:
case cons
α : Sort u_1
p : α → Bool
a : α
as : List α
ih : all p as = all' p as
⊢ (p a && List.foldr and true (List.map p as)) = (p a && all' p as)
Theorem: Nat.lt_mul_cancel_left
Proof state before:
a b x : ℕ
H : a < b
XNEQ0 : 0 < x
⊢ a * x < b * x
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: transpose_index_twice_is_id
Proof state before:
n m : ℕ
ix : TensorIndex2D n m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose ix) = ix
Tactic:
cases ix
Proof state after:
case mk
n m ix0✝ ix1✝ : ℕ
IX0✝ : ix0✝ < n
IX1✝ : ix1✝ < m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose { ix0 := ix0✝, ix1 := ix1✝, IX0 := IX0✝, IX1 := IX1✝ }) =
    { ix0 := ix0✝, ix1 := ix1✝, IX0 := IX0✝, IX1 := IX1✝ }
Theorem: transpose_index_twice_is_id
Proof state before:
n m ix0 ix1 : ℕ
IX0 : ix0 < n
IX1 : ix1 < m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }) =
    { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }
Tactic:
case mk ix0 ix1 IX0 IX1 => {
  simp[TensorIndex2D.transpose];
}
Proof state after:
no goals
Theorem: transpose_index_twice_is_id
Proof state before:
n m ix0 ix1 : ℕ
IX0 : ix0 < n
IX1 : ix1 < m
⊢ TensorIndex2D.transpose (TensorIndex2D.transpose { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }) =
    { ix0 := ix0, ix1 := ix1, IX0 := IX0, IX1 := IX1 }
Tactic:
simp[TensorIndex2D.transpose]
Proof state after:
no goals
Theorem: transpose_twice_is_id
Proof state before:
t : Tensor2D
⊢ Tensor2D.transpose (Tensor2D.transpose t) = t
Tactic:
cases t
Proof state after:
case mk
size0✝ size1✝ : ℕ
data✝ : TensorIndex2D size0✝ size1✝ → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0✝, size1 := size1✝, data := data✝ }) =
    { size0 := size0✝, size1 := size1✝, data := data✝ }
Theorem: transpose_twice_is_id
Proof state before:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0, size1 := size1, data := data }) =
    { size0 := size0, size1 := size1, data := data }
Tactic:
case mk size0 size1 data => {
 simp[Tensor2D.transpose];
 simp[transpose_index_twice_is_id];
}
Proof state after:
no goals
Theorem: transpose_twice_is_id
Proof state before:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0, size1 := size1, data := data }) =
    { size0 := size0, size1 := size1, data := data }
Tactic:
simp[Tensor2D.transpose]
Proof state after:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ (fun ix => data (TensorIndex2D.transpose (TensorIndex2D.transpose ix))) = data
Theorem: transpose_twice_is_id
Proof state before:
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ (fun ix => data (TensorIndex2D.transpose (TensorIndex2D.transpose ix))) = data
Tactic:
simp[transpose_index_twice_is_id]
Proof state after:
no goals
Theorem: shape_prod_nil
Proof state before:
l : List ℕ
⊢ shapeProd (0 :: l) = 0
Tactic:
induction l <;> simp [shapeProd, List.foldr]
Proof state after:
no goals
Theorem: shapeProd.cons_unfold
Proof state before:
⊢ ∀ (x : ℕ) (xs : List ℕ), shapeProd (x :: xs) = x * shapeProd xs
Tactic:
intros x xs
Proof state after:
x : ℕ
xs : List ℕ
⊢ shapeProd (x :: xs) = x * shapeProd xs
Theorem: shapeProd.cons_unfold
Proof state before:
x : ℕ
xs : List ℕ
⊢ shapeProd (x :: xs) = x * shapeProd xs
Tactic:
simp [shapeProd, List.foldr]
Proof state after:
no goals
Theorem: TensorFlatIndex.bound_non_zero
Proof state before:
bound : ℕ
flat : TensorFlatIndex bound
⊢ bound ≠ 0
Tactic:
intros BOUND
Proof state after:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
⊢ False
Theorem: TensorFlatIndex.bound_non_zero
Proof state before:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
⊢ False
Tactic:
have H_INBOUND := flat.h_ix_inbound
Proof state after:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
H_INBOUND : flat.ix < bound
⊢ False
Theorem: TensorFlatIndex.bound_non_zero
Proof state before:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
H_INBOUND : flat.ix < bound
⊢ False
Tactic:
simp [BOUND] at H_INBOUND
Proof state after:
no goals
Theorem: TensorFlatIndex.bound_zero_absurd
Proof state before:
flat : TensorFlatIndex 0
⊢ False
Tactic:
have H_INBOUND := flat.h_ix_inbound
Proof state after:
flat : TensorFlatIndex 0
H_INBOUND : flat.ix < 0
⊢ False
Theorem: TensorFlatIndex.bound_zero_absurd
Proof state before:
flat : TensorFlatIndex 0
H_INBOUND : flat.ix < 0
⊢ False
Tactic:
simp [Nat.not_lt_zero] at H_INBOUND
Proof state after:
no goals
Theorem: Nat.succ_gt_zero
Proof state before:
n : ℕ
⊢ succ n > 0
Tactic:
simp [GT.gt]
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
⊢ ∀ (n : ℕ), n ≠ 0 ↔ n > 0
Tactic:
intros n
Proof state after:
n : ℕ
⊢ n ≠ 0 ↔ n > 0
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
⊢ n ≠ 0 ↔ n > 0
Tactic:
constructor
Proof state after:
case mp
n : ℕ
⊢ n ≠ 0 → n > 0

case mpr
n : ℕ
⊢ n > 0 → n ≠ 0
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
⊢ n ≠ 0 → n > 0
Tactic:
case mp => {
intros NEQ_0;
cases n;
case zero => {
  contradiction;
}
case succ n' => { simp [Nat.succ_gt_zero]; }
}
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
⊢ n > 0 → n ≠ 0
Tactic:
case mpr => {
 intros GT_ZERO;
 cases n;
 case zero => {
   simp at GT_ZERO;
 }
 case succ n' => { simp; }
}
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
⊢ n ≠ 0 → n > 0
Tactic:
intros NEQ_0
Proof state after:
n : ℕ
NEQ_0 : n ≠ 0
⊢ n > 0
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
NEQ_0 : n ≠ 0
⊢ n > 0
Tactic:
cases n
Proof state after:
case zero
NEQ_0 : zero ≠ 0
⊢ zero > 0

case succ
n✝ : ℕ
NEQ_0 : succ n✝ ≠ 0
⊢ succ n✝ > 0
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
NEQ_0 : zero ≠ 0
⊢ zero > 0
Tactic:
case zero => {
  contradiction;
}
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n' : ℕ
NEQ_0 : succ n' ≠ 0
⊢ succ n' > 0
Tactic:
case succ n' => { simp [Nat.succ_gt_zero]; }
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
NEQ_0 : zero ≠ 0
⊢ zero > 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n' : ℕ
NEQ_0 : succ n' ≠ 0
⊢ succ n' > 0
Tactic:
simp [Nat.succ_gt_zero]
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
⊢ n > 0 → n ≠ 0
Tactic:
intros GT_ZERO
Proof state after:
n : ℕ
GT_ZERO : n > 0
⊢ n ≠ 0
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n : ℕ
GT_ZERO : n > 0
⊢ n ≠ 0
Tactic:
cases n
Proof state after:
case zero
GT_ZERO : zero > 0
⊢ zero ≠ 0

case succ
n✝ : ℕ
GT_ZERO : succ n✝ > 0
⊢ succ n✝ ≠ 0
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
GT_ZERO : zero > 0
⊢ zero ≠ 0
Tactic:
case zero => {
  simp at GT_ZERO;
}
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n' : ℕ
GT_ZERO : succ n' > 0
⊢ succ n' ≠ 0
Tactic:
case succ n' => { simp; }
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
GT_ZERO : zero > 0
⊢ zero ≠ 0
Tactic:
simp at GT_ZERO
Proof state after:
no goals
Theorem: Nat.nonzero_iff_gt_zero
Proof state before:
n' : ℕ
GT_ZERO : succ n' > 0
⊢ succ n' ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
bound : ℕ
flat : TensorFlatIndex bound
⊢ bound > 0
Tactic:
have BOUND_NONZERO: bound ≠ 0 := TensorFlatIndex.bound_non_zero flat
Proof state after:
bound : ℕ
flat : TensorFlatIndex bound
BOUND_NONZERO : bound ≠ 0
⊢ bound > 0
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
bound : ℕ
flat : TensorFlatIndex bound
BOUND_NONZERO : bound ≠ 0
⊢ bound > 0
Tactic:
cases bound
Proof state after:
case zero
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0

case succ
n✝ : ℕ
flat : TensorFlatIndex (Nat.succ n✝)
BOUND_NONZERO : Nat.succ n✝ ≠ 0
⊢ Nat.succ n✝ > 0
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0
Tactic:
case zero => {
  simp [Nat.zero, BOUND_NONZERO];
  contradiction;
}
Proof state after:
no goals
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
bound' : ℕ
flat : TensorFlatIndex (Nat.succ bound')
BOUND_NONZERO : Nat.succ bound' ≠ 0
⊢ Nat.succ bound' > 0
Tactic:
case succ bound' => {
  apply Nat.succ_gt_zero;
}
Proof state after:
no goals
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0
Tactic:
simp [Nat.zero, BOUND_NONZERO]
Proof state after:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ False
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: TensorFlatIndex.bound_gt_zero
Proof state before:
bound' : ℕ
flat : TensorFlatIndex (Nat.succ bound')
BOUND_NONZERO : Nat.succ bound' ≠ 0
⊢ Nat.succ bound' > 0
Tactic:
apply Nat.succ_gt_zero
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_left_nonzero
Proof state before:
⊢ ∀ (a b : ℕ), a * b ≠ 0 → a ≠ 0
Tactic:
intros a b NEQ
Proof state after:
a b : ℕ
NEQ : a * b ≠ 0
⊢ a ≠ 0
Theorem: Nat.mul_nonzero_implies_left_nonzero
Proof state before:
a b : ℕ
NEQ : a * b ≠ 0
⊢ a ≠ 0
Tactic:
induction a
Proof state after:
case zero
b : ℕ
NEQ : zero * b ≠ 0
⊢ zero ≠ 0

case succ
b n✝ : ℕ
n_ih✝ : n✝ * b ≠ 0 → n✝ ≠ 0
NEQ : succ n✝ * b ≠ 0
⊢ succ n✝ ≠ 0
Theorem: Nat.mul_nonzero_implies_left_nonzero
Proof state before:
b : ℕ
NEQ : zero * b ≠ 0
⊢ zero ≠ 0
Tactic:
case zero => {
 simp at NEQ;
}
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_left_nonzero
Proof state before:
b a' : ℕ
IH : a' * b ≠ 0 → a' ≠ 0
NEQ : succ a' * b ≠ 0
⊢ succ a' ≠ 0
Tactic:
case succ a' IH => {
  apply Nat.succ_ne_zero;
}
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_left_nonzero
Proof state before:
b : ℕ
NEQ : zero * b ≠ 0
⊢ zero ≠ 0
Tactic:
simp at NEQ
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_left_nonzero
Proof state before:
b a' : ℕ
IH : a' * b ≠ 0 → a' ≠ 0
NEQ : succ a' * b ≠ 0
⊢ succ a' ≠ 0
Tactic:
apply Nat.succ_ne_zero
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
⊢ ∀ (a b : ℕ), a * b ≠ 0 → b ≠ 0
Tactic:
intros a b NEQ
Proof state after:
a b : ℕ
NEQ : a * b ≠ 0
⊢ b ≠ 0
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
a b : ℕ
NEQ : a * b ≠ 0
⊢ b ≠ 0
Tactic:
induction a
Proof state after:
case zero
b : ℕ
NEQ : zero * b ≠ 0
⊢ b ≠ 0

case succ
b n✝ : ℕ
n_ih✝ : n✝ * b ≠ 0 → b ≠ 0
NEQ : succ n✝ * b ≠ 0
⊢ b ≠ 0
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
b : ℕ
NEQ : zero * b ≠ 0
⊢ b ≠ 0
Tactic:
case zero => {
 simp at NEQ;
}
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
b a' : ℕ
IH : a' * b ≠ 0 → b ≠ 0
NEQ : succ a' * b ≠ 0
⊢ b ≠ 0
Tactic:
case succ a' IH => {
  induction b;
  case zero => {
   simp at NEQ;
  }
  case succ b' IH => {
   apply Nat.succ_ne_zero;
  }
}
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
b : ℕ
NEQ : zero * b ≠ 0
⊢ b ≠ 0
Tactic:
simp at NEQ
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
b a' : ℕ
IH : a' * b ≠ 0 → b ≠ 0
NEQ : succ a' * b ≠ 0
⊢ b ≠ 0
Tactic:
induction b
Proof state after:
case zero
a' : ℕ
IH : a' * zero ≠ 0 → zero ≠ 0
NEQ : succ a' * zero ≠ 0
⊢ zero ≠ 0

case succ
a' n✝ : ℕ
n_ih✝ : (a' * n✝ ≠ 0 → n✝ ≠ 0) → succ a' * n✝ ≠ 0 → n✝ ≠ 0
IH : a' * succ n✝ ≠ 0 → succ n✝ ≠ 0
NEQ : succ a' * succ n✝ ≠ 0
⊢ succ n✝ ≠ 0
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
a' : ℕ
IH : a' * zero ≠ 0 → zero ≠ 0
NEQ : succ a' * zero ≠ 0
⊢ zero ≠ 0
Tactic:
case zero => {
 simp at NEQ;
}
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
a' b' : ℕ
IH✝ : (a' * b' ≠ 0 → b' ≠ 0) → succ a' * b' ≠ 0 → b' ≠ 0
IH : a' * succ b' ≠ 0 → succ b' ≠ 0
NEQ : succ a' * succ b' ≠ 0
⊢ succ b' ≠ 0
Tactic:
case succ b' IH => {
 apply Nat.succ_ne_zero;
}
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
a' : ℕ
IH : a' * zero ≠ 0 → zero ≠ 0
NEQ : succ a' * zero ≠ 0
⊢ zero ≠ 0
Tactic:
simp at NEQ
Proof state after:
no goals
Theorem: Nat.mul_nonzero_implies_right_nonzero
Proof state before:
a' b' : ℕ
IH✝ : (a' * b' ≠ 0 → b' ≠ 0) → succ a' * b' ≠ 0 → b' ≠ 0
IH : a' * succ b' ≠ 0 → succ b' ≠ 0
NEQ : succ a' * succ b' ≠ 0
⊢ succ b' ≠ 0
Tactic:
apply Nat.succ_ne_zero
Proof state after:
no goals
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof state before:
⊢ ∀ (xs : List ℕ) (x : ℕ), List.Mem x xs → shapeProd xs > 0 → x > 0
Tactic:
intros xs x MEM
Proof state after:
xs : List ℕ
x : ℕ
MEM : List.Mem x xs
⊢ shapeProd xs > 0 → x > 0
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof state before:
xs : List ℕ
x : ℕ
MEM : List.Mem x xs
⊢ shapeProd xs > 0 → x > 0
Tactic:
induction MEM
Proof 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
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof 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;
}
Proof state after:
no goals
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
⊢ 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];
}
Proof state after:
no goals
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof state before:
xs : List ℕ
x : ℕ
as : List ℕ
⊢ shapeProd (x :: as) > 0 → x > 0
Tactic:
simp [shapeProd, List.foldr]
Proof state after:
xs : List ℕ
x : ℕ
as : List ℕ
⊢ 0 < x → 0 < List.foldr (fun x x_1 => x * x_1) 1 as → 0 < x
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof 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
Proof 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
Theorem: shapeProd_nonzero_implies_member_nonzero
Proof 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
Proof state after:
no goals
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
⊢ shapeProd (b :: bs) > 0 → x > 0
Tactic:
intros H
Proof 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
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 : shapeProd (b :: bs) > 0
⊢ x > 0
Tactic:
apply IH
Proof 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
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 : shapeProd (b :: bs) > 0
⊢ shapeProd bs > 0
Tactic:
simp at H
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