internlm/Lean-Github huggingface dataset:
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
RHS : { ix := getIx, h_ix_inbound := GETIX } = { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) }
⊢ getF (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs)) getIx
      (_ : getIx < length (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs))) =
    (getF xs getIx GETIX, { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) })
Tactic:
apply List.zip_flat_index_go_get (xs := xs) (ix := 0) (bound := List.length xs) (deltaIx := getIx) (GETIX := GETIX)
Proof state after:
no goals
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ 0 + getIx < length xs
Tactic:
simp
Proof state after:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs
Tactic:
apply GETIX
Proof state after:
no goals
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ { ix := getIx, h_ix_inbound := GETIX } = { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) }
Tactic:
simp
Proof state after:
no goals
Theorem: List.mapM_loop_map
Proof state before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
results : List β
⊢ (∀ (a : α), fM a = pure (f a)) → mapM.loop fM l results = pure (reverse results ++ map f l)
Tactic:
intros h
Proof state after:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
results : List β
h : ∀ (a : α), fM a = pure (f a)
⊢ mapM.loop fM l results = pure (reverse results ++ map f l)
Theorem: List.mapM_loop_map
Proof state before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
results : List β
h : ∀ (a : α), fM a = pure (f a)
⊢ mapM.loop fM l results = pure (reverse results ++ map f l)
Tactic:
revert results
Proof state after:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
⊢ ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
Theorem: List.mapM_loop_map
Proof state before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
⊢ ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
Tactic:
induction l with
| nil => intros results; simp [map];
| cons a l ih =>
    intros results
    simp [mapM.loop, map, h, ih, reverse_cons, append_assoc]
Proof state after:
no goals
Theorem: List.mapM_loop_map
Proof state before:
case nil
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
⊢ ∀ (results : List β), mapM.loop fM [] results = pure (reverse results ++ map f [])
Tactic:
intros results
Proof state after:
case nil
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
results : List β
⊢ mapM.loop fM [] results = pure (reverse results ++ map f [])
Theorem: List.mapM_loop_map
Proof state before:
case nil
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
results : List β
⊢ mapM.loop fM [] results = pure (reverse results ++ map f [])
Tactic:
simp [map]
Proof state after:
no goals
Theorem: List.mapM_loop_map
Proof state before:
case cons
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
a : α
l : List α
ih : ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
⊢ ∀ (results : List β), mapM.loop fM (a :: l) results = pure (reverse results ++ map f (a :: l))
Tactic:
intros results
Proof state after:
case cons
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
a : α
l : List α
ih : ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
results : List β
⊢ mapM.loop fM (a :: l) results = pure (reverse results ++ map f (a :: l))
Theorem: List.mapM_loop_map
Proof state before:
case cons
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
f : α → β
fM : α → M β
h : ∀ (a : α), fM a = pure (f a)
a : α
l : List α
ih : ∀ (results : List β), mapM.loop fM l results = pure (reverse results ++ map f l)
results : List β
⊢ mapM.loop fM (a :: l) results = pure (reverse results ++ map f (a :: l))
Tactic:
simp [mapM.loop, map, h, ih, reverse_cons, append_assoc]
Proof state after:
no goals
Theorem: List.mapM_map
Proof state before:
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
⊢ (∀ (a : α), fM a = pure (f a)) → mapM fM l = pure (map f l)
Tactic:
apply List.mapM_loop_map
Proof state after:
no goals
Theorem: Tensor1D.mapM_map
Proof state before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
⊢ (∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)) →
    mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)
Tactic:
intros h
Proof state after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)
Theorem: Tensor1D.mapM_map
Proof state before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)
Tactic:
unfold mapWithFlatIndex
Proof state after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }
Theorem: Tensor1D.mapM_map
Proof state before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }
Tactic:
unfold mapMWithFlatIndex
Proof state after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ←
        List.mapM
            (fun x =>
              match x with
              | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data)
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }
Theorem: Tensor1D.mapM_map
Proof state before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ←
        List.mapM
            (fun x =>
              match x with
              | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data)
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }
Tactic:
rw [List.mapM_map]
Proof state after:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ← pure (List.map ?f (List.zipFlatIndex v.data))
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }

case f
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ FinInt 32 × TensorFlatIndex (List.length v.data) → FinInt 32

case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (?f a)
Theorem: Tensor1D.mapM_map
Proof state before:
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ (do
      let data ← pure (List.map ?f (List.zipFlatIndex v.data))
      let temp : Tensor1D :=
        { size0 := List.length data, data := data, h_data_size := (_ : List.length data = List.length data) }
      pure temp) =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }

case f
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ FinInt 32 × TensorFlatIndex (List.length v.data) → FinInt 32

case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (?f a)
Tactic:
. simp [v.h_data_size]; rfl
Proof state after:
case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (f ((_ : List.length v.data = v.size0) ▸ a.snd) a.fst)
Theorem: Tensor1D.mapM_map
Proof state before:
case a
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (f ((_ : List.length v.data = v.size0) ▸ a.snd) a.fst)
Tactic:
. intros a; cases a; simp [h]
Proof state after:
no goals
Theorem: testSuccess
Proof state before:
⊢ Nat → ∀ (bint : Int), Nat → ∀ (dint : Int), Int → bint = dint
Tactic:
intros a b c d e
Proof state after:
a : Nat
b : Int
c : Nat
d e : Int
⊢ b = d
Theorem: testGoalNotEqualityMustFail
Proof state before:
⊢ Nat → Int → Nat → Nat
Tactic:
intros a b c
Proof state after:
a : Nat
b : Int
c : Nat
⊢ Nat
Theorem: Int.sub_add_assoc
Proof state before:
n m k : ℤ
⊢ n - m + k = n + (k - m)
Tactic:
simp [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm (-m) k]
Proof state after:
no goals
Theorem: Int.sub_assoc
Proof state before:
n m k : ℤ
⊢ n - m - k = n - k - m
Tactic:
simp [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm (-m) (-k)]
Proof state after:
no goals
Theorem: Int.add_sub
Proof state before:
n m : ℤ
⊢ n + (m - n) = m
Tactic:
rw [Int.sub_eq_add_neg, Int.add_comm m (-n), ←Int.add_assoc,
    Int.add_right_neg, Int.zero_add]
Proof state after:
no goals
Theorem: Int.sub_add_dist
Proof state before:
n m p : ℤ
⊢ n - (m + p) = n - m - p
Tactic:
rw [Int.sub_eq_add_neg, Int.neg_add, ←Int.add_assoc,
    ←Int.sub_eq_add_neg, ←Int.sub_eq_add_neg]
Proof state after:
no goals
Theorem: Int.mul_two
Proof state before:
n : ℤ
⊢ n * 2 = n + n
Tactic:
have h: (2:Int) = 1 + 1 := rfl
Proof state after:
n : ℤ
h : 2 = 1 + 1
⊢ n * 2 = n + n
Theorem: Int.mul_two
Proof state before:
n : ℤ
h : 2 = 1 + 1
⊢ n * 2 = n + n
Tactic:
rw [h]
Proof state after:
n : ℤ
h : 2 = 1 + 1
⊢ n * (1 + 1) = n + n
Theorem: Int.mul_two
Proof state before:
n : ℤ
h : 2 = 1 + 1
⊢ n * (1 + 1) = n + n
Tactic:
rw [Int.mul_add]
Proof state after:
n : ℤ
h : 2 = 1 + 1
⊢ n * 1 + n * 1 = n + n
Theorem: Int.mul_two
Proof state before:
n : ℤ
h : 2 = 1 + 1
⊢ n * 1 + n * 1 = n + n
Tactic:
simp [Int.mul_one]
Proof state after:
no goals
Theorem: Int.pow_zero
Proof state before:
n : ℤ
⊢ n ^ 0 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.pow_succ
Proof state before:
n : ℤ
m : ℕ
⊢ n ^ (m + 1) = n ^ m * n
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.two_pow_ge
Proof state before:
n : ℕ
⊢ 2 ^ n ≥ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.two_pow_pos
Proof state before:
n : ℕ
⊢ 2 ^ n > 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.one_le_two_pow
Proof state before:
n : ℕ
⊢ 1 ≤ 2 ^ n
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.one_lt_two_pow
Proof state before:
n : ℕ
⊢ n > 0 → 1 < 2 ^ n
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.mod_bounds
Proof state before:
a b : ℤ
⊢ a ≥ 0 → a < b → a % b = a
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.mod_mod
Proof state before:
a b : ℤ
⊢ a % b % b = a % b
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.mod_ge_neg
Proof state before:
a b : ℤ
⊢ a % b ≥ -b
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.mod_ge
Proof state before:
a b : ℤ
⊢ a ≥ 0 → a % b ≥ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.mod_lt
Proof state before:
a b : ℤ
⊢ b > 0 → a % b < b
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.add_mod_right
Proof state before:
x z : ℤ
⊢ z > 0 → x ≥ 0 → (x + z) % z = x % z
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.add_mod_left
Proof state before:
x z : ℤ
⊢ z > 0 → x ≥ 0 → (z + x) % z = x % z
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.ge_zero_eq_nonneg
Proof state before:
n : ℤ
⊢ n ≥ 0 ↔ NonNeg n
Tactic:
simp [GE.ge, LE.le, Int.le]
Proof state after:
no goals
Theorem: Int.zero_ge_neg
Proof state before:
n : ℤ
⊢ n ≥ 0 → 0 ≥ -n
Tactic:
simp [GE.ge, LE.le, Int.le, Int.neg_neg]
Proof state after:
no goals
Theorem: Int.add_ge_zero
Proof state before:
n m : ℤ
⊢ n ≥ 0 → m ≥ 0 → n + m ≥ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.le_succ
Proof state before:
n : ℤ
⊢ n ≤ n + 1
Tactic:
suffices NonNeg 1 by simp [LE.le, Int.le, add_sub_assoc, add_sub]; trivial
Proof state after:
n : ℤ
⊢ NonNeg 1
Theorem: Int.le_succ
Proof state before:
n : ℤ
⊢ NonNeg 1
Tactic:
constructor
Proof state after:
no goals
Theorem: Int.le_succ
Proof state before:
n : ℤ
this : NonNeg 1
⊢ n ≤ n + 1
Tactic:
simp [LE.le, Int.le, add_sub_assoc, add_sub]
Proof state after:
n : ℤ
this : NonNeg 1
⊢ NonNeg 1
Theorem: Int.le_succ
Proof state before:
n : ℤ
this : NonNeg 1
⊢ NonNeg 1
Tactic:
trivial
Proof state after:
no goals
Theorem: Int.succ_le_succ
Proof state before:
n m : ℤ
⊢ n ≤ m → n + 1 ≤ m + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.ge_trans
Proof state before:
n k m : ℤ
⊢ n ≥ m → m ≥ k → n ≥ k
Tactic:
simp [GE.ge]
Proof state after:
n k m : ℤ
⊢ m ≤ n → k ≤ m → k ≤ n
Theorem: Int.ge_trans
Proof state before:
n k m : ℤ
⊢ m ≤ n → k ≤ m → k ≤ n
Tactic:
intros h₁ h₂
Proof state after:
n k m : ℤ
h₁ : m ≤ n
h₂ : k ≤ m
⊢ k ≤ n
Theorem: Int.ge_trans
Proof state before:
n k m : ℤ
h₁ : m ≤ n
h₂ : k ≤ m
⊢ k ≤ n
Tactic:
apply le_trans h₂ h₁
Proof state after:
no goals
Theorem: Int.lt_add_right
Proof state before:
n m : ℤ
⊢ m > 0 → n < n + m
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.mul_ge_zero
Proof state before:
n m : ℤ
⊢ n ≥ 0 → m ≥ 0 → n * m ≥ 0
Tactic:
rw [Int.ge_zero_eq_nonneg, Int.ge_zero_eq_nonneg, Int.ge_zero_eq_nonneg]
Proof state after:
n m : ℤ
⊢ NonNeg n → NonNeg m → NonNeg (n * m)
Theorem: Int.mul_ge_zero
Proof state before:
n m : ℤ
⊢ NonNeg n → NonNeg m → NonNeg (n * m)
Tactic:
intros hn hm
Proof state after:
n m : ℤ
hn : NonNeg n
hm : NonNeg m
⊢ NonNeg (n * m)
Theorem: Int.mul_ge_zero
Proof state before:
n m : ℤ
hn : NonNeg n
hm : NonNeg m
⊢ NonNeg (n * m)
Tactic:
cases hn
Proof state after:
case mk
m : ℤ
hm : NonNeg m
n✝ : ℕ
⊢ NonNeg (ofNat n✝ * m)
Theorem: Int.mul_ge_zero
Proof state before:
case mk
m : ℤ
hm : NonNeg m
n✝ : ℕ
⊢ NonNeg (ofNat n✝ * m)
Tactic:
cases hm
Proof state after:
case mk.mk
n✝¹ n✝ : ℕ
⊢ NonNeg (ofNat n✝¹ * ofNat n✝)
Theorem: Int.mul_ge_zero
Proof state before:
case mk.mk
n✝¹ n✝ : ℕ
⊢ NonNeg (ofNat n✝¹ * ofNat n✝)
Tactic:
constructor
Proof state after:
no goals
Theorem: Int.mul_gt_zero
Proof state before:
n m : ℤ
⊢ n > 0 → m > 0 → n * m > 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.pow_ge_zero
Proof state before:
n : ℤ
m : ℕ
⊢ n ≥ 0 → n ^ m ≥ 0
Tactic:
revert n
Proof state after:
m : ℕ
⊢ ∀ (n : ℤ), n ≥ 0 → n ^ m ≥ 0
Theorem: Int.pow_ge_zero
Proof state before:
m : ℕ
⊢ ∀ (n : ℤ), n ≥ 0 → n ^ m ≥ 0
Tactic:
induction m <;> intros n h <;> simp
Proof state after:
case succ
n✝ : ℕ
n_ih✝ : ∀ (n : ℤ), n ≥ 0 → n ^ n✝ ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ Nat.succ n✝
Theorem: Int.pow_ge_zero
Proof state before:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ Nat.succ acc
Tactic:
case succ acc ih =>
  simp [pow_succ]; apply mul_ge_zero (ih _ h) h
Proof state after:
no goals
Theorem: Int.pow_ge_zero
Proof state before:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ Nat.succ acc
Tactic:
simp [pow_succ]
Proof state after:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ acc * n
Theorem: Int.pow_ge_zero
Proof state before:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ acc * n
Tactic:
apply mul_ge_zero (ih _ h) h
Proof state after:
no goals
Theorem: Int.pow_gt_zero
Proof state before:
n : ℤ
m : ℕ
⊢ n > 0 → n ^ m > 0
Tactic:
revert n
Proof state after:
m : ℕ
⊢ ∀ (n : ℤ), n > 0 → n ^ m > 0
Theorem: Int.pow_gt_zero
Proof state before:
m : ℕ
⊢ ∀ (n : ℤ), n > 0 → n ^ m > 0
Tactic:
induction m <;> intros n h <;> simp
Proof state after:
case succ
n✝ : ℕ
n_ih✝ : ∀ (n : ℤ), n > 0 → n ^ n✝ > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ Nat.succ n✝
Theorem: Int.pow_gt_zero
Proof state before:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ Nat.succ acc
Tactic:
case succ acc ih =>
  simp [pow_succ]; apply mul_gt_zero (ih _ h) h
Proof state after:
no goals
Theorem: Int.pow_gt_zero
Proof state before:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ Nat.succ acc
Tactic:
simp [pow_succ]
Proof state after:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ acc * n
Theorem: Int.pow_gt_zero
Proof state before:
acc : ℕ
ih : ∀ (n : ℤ), n > 0 → n ^ acc > 0
n : ℤ
h : n > 0
⊢ 0 < n ^ acc * n
Tactic:
apply mul_gt_zero (ih _ h) h
Proof state after:
no goals
Theorem: Int.lt_add_lt_left
Proof state before:
n m k : ℤ
⊢ n < m → k + n < k + m
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.ge_add_ge_right
Proof state before:
n m k : ℤ
⊢ n ≥ m → n + k ≥ m + k
Tactic:
sorry
Proof state after:
no goals
Theorem: Nat.minus_plus_one
Proof state before:
a : ℕ
h : a > 0
⊢ a - 1 + 1 = a
Tactic:
cases a
Proof state after:
case zero
h : zero > 0
⊢ zero - 1 + 1 = zero

case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝