internlm/Lean-Github huggingface dataset:
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ recComplete.aux ind (succ n) (succ k) hk = recCompleteWF ind (succ k)
Tactic:
dsimp [recComplete.aux]
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = recCompleteWF ind (succ k)
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = recCompleteWF ind (succ k)
Tactic:
unfold recCompleteWF
Proof state after:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = ind (succ k) fun k_1 x => recCompleteWF ind k_1
Theorem: Nat.recComplete_eq
Proof state before:
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = ind (succ k) fun k_1 x => recCompleteWF ind k_1
Tactic:
apply congrArg
Proof state after:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = fun k_1 x => recCompleteWF ind k_1
Theorem: Nat.recComplete_eq
Proof state before:
case h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = fun k_1 x => recCompleteWF ind k_1
Tactic:
funext k hk
Proof state after:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k✝ : Nat
hk✝ : succ k✝ ≤ succ n
k : Nat
hk : k < k✝ + 1
⊢ recComplete.aux ind n k (_ : k ≤ n) = recCompleteWF ind k
Theorem: Nat.recComplete_eq
Proof state before:
case h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k✝ : Nat
hk✝ : succ k✝ ≤ succ n
k : Nat
hk : k < k✝ + 1
⊢ recComplete.aux ind n k (_ : k ≤ n) = recCompleteWF ind k
Tactic:
rw [h_ind]
Proof state after:
no goals
Theorem: Nat.recBase2_div2
Proof state before:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recBase2 zero one div2 (n + 2) = div2 n (recBase2 zero one div2 (n / 2 + 1))
Tactic:
unfold recBase2
Proof state after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recComplete
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recComplete
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))
Theorem: Nat.recBase2_div2
Proof state before:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recComplete
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recComplete
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))
Tactic:
rw [recComplete_eq, recComplete_eq]
Proof state after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recCompleteWF
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recCompleteWF
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))
Theorem: Nat.recBase2_div2
Proof state before:
motive : Nat → Sort u
zero : motive 0
one : motive 1
div2 : (n : Nat) → motive (n / 2 + 1) → motive (n + 2)
n : Nat
⊢ recCompleteWF
      (fun n ind =>
        match n, ind with
        | 0, ind => zero
        | 1, ind => one
        | succ (succ n), ind =>
          let_fun this := (_ : n / 2 + 1 < n + 2);
          div2 n (ind (n / 2 + 1) this))
      (n + 2) =
    div2 n
      (recCompleteWF
        (fun n ind =>
          match n, ind with
          | 0, ind => zero
          | 1, ind => one
          | succ (succ n), ind =>
            let_fun this := (_ : n / 2 + 1 < n + 2);
            div2 n (ind (n / 2 + 1) this))
        (n / 2 + 1))
Tactic:
conv =>
  lhs; unfold recCompleteWF
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
⊢ ∀ {l : List α}, List.forallr p l → ∀ (a : α), a ∈ l → p a
Tactic:
intro l hlp a hMem
Proof state after:
α : Type u
p : α → Prop
l : List α
hlp : List.forallr p l
a : α
hMem : a ∈ l
⊢ p a
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
l : List α
hlp : List.forallr p l
a : α
hMem : a ∈ l
⊢ p a
Tactic:
induction l
Proof state after:
case nil
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a

case cons
α : Type u
p : α → Prop
a head✝ : α
tail✝ : List α
tail_ih✝ : List.forallr p tail✝ → a ∈ tail✝ → p a
hlp : List.forallr p (head✝ :: tail✝)
hMem : a ∈ head✝ :: tail✝
⊢ p a
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a
Tactic:
case nil => cases hMem
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : a ∈ hhead :: htail
⊢ p a
Tactic:
case cons hhead htail h_ind =>
  cases hMem
  case head => cases hlp; assumption
  case tail hMem => apply h_ind ?_ hMem; cases hlp; assumption
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a
Tactic:
cases hMem
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : a ∈ hhead :: htail
⊢ p a
Tactic:
cases hMem
Proof state after:
case head
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a

case tail
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
a✝ : Mem a htail
⊢ p a
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a
Tactic:
case head => cases hlp; assumption
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ p a
Tactic:
case tail hMem => apply h_ind ?_ hMem; cases hlp; assumption
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a
Tactic:
cases hlp
Proof state after:
case cons
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
a✝¹ : p a
a✝ : List.forallr p htail
⊢ p a
Theorem: List.forallr_Mem
Proof state before:
case cons
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
a✝¹ : p a
a✝ : List.forallr p htail
⊢ p a
Tactic:
assumption
Proof state after:
no goals
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ p a
Tactic:
apply h_ind ?_ hMem
Proof state after:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ List.forallr p htail
Theorem: List.forallr_Mem
Proof state before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ List.forallr p htail
Tactic:
cases hlp
Proof state after:
case cons
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hMem : Mem a htail
a✝¹ : p hhead
a✝ : List.forallr p htail
⊢ List.forallr p htail
Theorem: List.forallr_Mem
Proof state before:
case cons
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hMem : Mem a htail
a✝¹ : p hhead
a✝ : List.forallr p htail
⊢ List.forallr p htail
Tactic:
assumption
Proof state after:
no goals
Theorem: Nat.min_zero'
Proof state before:
n : Nat
⊢ min n 0 = 0
Tactic:
rw [Nat.min_def]
Proof state after:
n : Nat
⊢ (if n ≤ 0 then n else 0) = 0
Theorem: Nat.min_zero'
Proof state before:
n : Nat
⊢ (if n ≤ 0 then n else 0) = 0
Tactic:
if h : n ≤ 0
then cases h; exact if_pos Nat.le.refl
else exact if_neg h
Proof state after:
no goals
Theorem: Nat.min_zero'
Proof state before:
n : Nat
h : n ≤ 0
⊢ (if n ≤ 0 then n else 0) = 0
Tactic:
cases h
Proof state after:
case refl

⊢ (if 0 ≤ 0 then 0 else 0) = 0
Theorem: Nat.min_zero'
Proof state before:
case refl

⊢ (if 0 ≤ 0 then 0 else 0) = 0
Tactic:
exact if_pos Nat.le.refl
Proof state after:
no goals
Theorem: Nat.min_zero'
Proof state before:
n : Nat
h : ¬n ≤ 0
⊢ (if n ≤ 0 then n else 0) = 0
Tactic:
exact if_neg h
Proof state after:
no goals
Theorem: Nat.min_eq_right'
Proof state before:
m n : Nat
h : m ≥ n
⊢ min m n = n
Tactic:
rw [Nat.min_def]
Proof state after:
m n : Nat
h : m ≥ n
⊢ (if m ≤ n then m else n) = n
Theorem: Nat.min_eq_right'
Proof state before:
m n : Nat
h : m ≥ n
⊢ (if m ≤ n then m else n) = n
Tactic:
if hmn : m ≤ n then
  have : m = n := Nat.le_antisymm hmn h
  rw [if_pos hmn, this]
else
  rw [if_neg hmn]
Proof state after:
no goals
Theorem: Nat.min_eq_right'
Proof state before:
m n : Nat
h : m ≥ n
hmn : m ≤ n
⊢ (if m ≤ n then m else n) = n
Tactic:
have : m = n := Nat.le_antisymm hmn h
Proof state after:
m n : Nat
h : m ≥ n
hmn : m ≤ n
this : m = n
⊢ (if m ≤ n then m else n) = n
Theorem: Nat.min_eq_right'
Proof state before:
m n : Nat
h : m ≥ n
hmn : m ≤ n
this : m = n
⊢ (if m ≤ n then m else n) = n
Tactic:
rw [if_pos hmn, this]
Proof state after:
no goals
Theorem: Nat.min_eq_right'
Proof state before:
m n : Nat
h : m ≥ n
hmn : ¬m ≤ n
⊢ (if m ≤ n then m else n) = n
Tactic:
rw [if_neg hmn]
Proof state after:
no goals
Theorem: Nat.min_succ_succ'
Proof state before:
m n : Nat
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
if h : m ≤ n then
  rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
else
  have : m ≥ n := Nat.le_of_lt (Nat.gt_of_not_le h)
  rw [Nat.min_eq_right' this, Nat.min_eq_right' (Nat.succ_le_succ this)]
Proof state after:
no goals
Theorem: Nat.min_succ_succ'
Proof state before:
m n : Nat
h : m ≤ n
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
Proof state after:
no goals
Theorem: Nat.min_succ_succ'
Proof state before:
m n : Nat
h : ¬m ≤ n
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
have : m ≥ n := Nat.le_of_lt (Nat.gt_of_not_le h)
Proof state after:
m n : Nat
h : ¬m ≤ n
this : m ≥ n
⊢ min (succ m) (succ n) = succ (min m n)
Theorem: Nat.min_succ_succ'
Proof state before:
m n : Nat
h : ¬m ≤ n
this : m ≥ n
⊢ min (succ m) (succ n) = succ (min m n)
Tactic:
rw [Nat.min_eq_right' this, Nat.min_eq_right' (Nat.succ_le_succ this)]
Proof state after:
no goals
Theorem: Nat.add_sub_assoc'
Proof state before:
m k : Nat
⊢ m ≤ k → ∀ (n : Nat), n + m - k = n - (k - m)
Tactic:
intro hmk n
Proof state after:
m k : Nat
hmk : m ≤ k
n : Nat
⊢ n + m - k = n - (k - m)
Theorem: Nat.add_sub_assoc'
Proof state before:
m k : Nat
hmk : m ≤ k
n : Nat
⊢ n + m - k = n - (k - m)
Tactic:
have : k = (k-m) + m := Eq.symm $ Nat.sub_add_cancel hmk
Proof state after:
m k : Nat
hmk : m ≤ k
n : Nat
this : k = k - m + m
⊢ n + m - k = n - (k - m)
Theorem: Nat.add_sub_assoc'
Proof state before:
m k : Nat
hmk : m ≤ k
n : Nat
this : k = k - m + m
⊢ n + m - k = n - (k - m)
Tactic:
conv => lhs; rw [this, Nat.add_sub_add_right]
Proof state after:
no goals
Theorem: Nat.add_pred
Proof state before:
m n : Nat
⊢ n > 0 → m + pred n = pred (m + n)
Tactic:
intro hn
Proof state after:
m n : Nat
hn : n > 0
⊢ m + pred n = pred (m + n)
Theorem: Nat.add_pred
Proof state before:
m n : Nat
hn : n > 0
⊢ m + pred n = pred (m + n)
Tactic:
cases n
Proof state after:
case zero
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)

case succ
m n✝ : Nat
hn : succ n✝ > 0
⊢ m + pred (succ n✝) = pred (m + succ n✝)
Theorem: Nat.add_pred
Proof state before:
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)
Tactic:
case zero =>
  exact (zero.not_lt_zero hn).elim
Proof state after:
no goals
Theorem: Nat.add_pred
Proof state before:
m n : Nat
hn : succ n > 0
⊢ m + pred (succ n) = pred (m + succ n)
Tactic:
case succ n =>
  simp [Nat.add_succ]
Proof state after:
no goals
Theorem: Nat.add_pred
Proof state before:
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)
Tactic:
exact (zero.not_lt_zero hn).elim
Proof state after:
no goals
Theorem: Nat.add_pred
Proof state before:
m n : Nat
hn : succ n > 0
⊢ m + pred (succ n) = pred (m + succ n)
Tactic:
simp [Nat.add_succ]
Proof state after:
no goals
Theorem: Nat.lt_of_mul_lt_mul_left
Proof state before:
a b c : Nat
⊢ a * b < a * c → b < c
Tactic:
intro h
Proof state after:
a b c : Nat
h : a * b < a * c
⊢ b < c
Theorem: Nat.lt_of_mul_lt_mul_left
Proof state before:
a b c : Nat
h : a * b < a * c
⊢ b < c
Tactic:
apply Nat.lt_of_not_le
Proof state after:
case a
a b c : Nat
h : a * b < a * c
⊢ ¬c ≤ b
Theorem: Nat.lt_of_mul_lt_mul_left
Proof state before:
case a
a b c : Nat
h : a * b < a * c
⊢ ¬c ≤ b
Tactic:
intro hcontra
Proof state after:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
⊢ False
Theorem: Nat.lt_of_mul_lt_mul_left
Proof state before:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
⊢ False
Tactic:
have := Nat.mul_le_mul_left a hcontra
Proof state after:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
this : a * c ≤ a * b
⊢ False
Theorem: Nat.lt_of_mul_lt_mul_left
Proof state before:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
this : a * c ≤ a * b
⊢ False
Tactic:
exact absurd h (Nat.not_lt_of_le this)
Proof state after:
no goals
Theorem: Nat.lt_of_mul_lt_mul_right
Proof state before:
a b c : Nat
⊢ a * c < b * c → a < b
Tactic:
intro h
Proof state after:
a b c : Nat
h : a * c < b * c
⊢ a < b
Theorem: Nat.lt_of_mul_lt_mul_right
Proof state before:
a b c : Nat
h : a * c < b * c
⊢ a < b
Tactic:
apply Nat.lt_of_not_le
Proof state after:
case a
a b c : Nat
h : a * c < b * c
⊢ ¬b ≤ a
Theorem: Nat.lt_of_mul_lt_mul_right
Proof state before:
case a
a b c : Nat
h : a * c < b * c
⊢ ¬b ≤ a
Tactic:
intro hcontra
Proof state after:
case a
a b c : Nat
h : a * c < b * c
hcontra : b ≤ a
⊢ False
Theorem: Nat.lt_of_mul_lt_mul_right
Proof state before:
case a
a b c : Nat
h : a * c < b * c
hcontra : b ≤ a
⊢ False
Tactic:
have := Nat.mul_le_mul_right c hcontra
Proof state after:
case a
a b c : Nat
h : a * c < b * c
hcontra : b ≤ a
this : b * c ≤ a * c
⊢ False
Theorem: Nat.lt_of_mul_lt_mul_right
Proof state before:
case a
a b c : Nat
h : a * c < b * c
hcontra : b ≤ a
this : b * c ≤ a * c
⊢ False
Tactic:
exact absurd h (Nat.not_lt_of_le this)
Proof state after:
no goals
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
⊢ a ≤ b → a / c ≤ b / c
Tactic:
intro hab
Proof state after:
a b c : Nat
hab : a ≤ b
⊢ a / c ≤ b / c
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
⊢ a / c ≤ b / c
Tactic:
cases Nat.lt_or_ge (b/c) (a/c)
Proof state after:
case inl
a b c : Nat
hab : a ≤ b
h✝ : b / c < a / c
⊢ a / c ≤ b / c

case inr
a b c : Nat
hab : a ≤ b
h✝ : b / c ≥ a / c
⊢ a / c ≤ b / c
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hge : b / c ≥ a / c
⊢ a / c ≤ b / c
Tactic:
case inr hge => exact hge
Proof state after:
no goals
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ a / c ≤ b / c
Tactic:
case inl hlt =>
  have : c > 0 := (Nat.lt_or_ge 0 c).elim id $ by
    intro h; cases h; rw [Nat.div_zero, Nat.div_zero] at hlt; cases hlt
  have := (Nat.div_lt_iff_lt_mul ‹c>0›).mp hlt
  have := calc
    b < a/c*c := this
    _ ≤ a := Nat.div_mul_le_self a c
    _ ≤ b := hab
  exact absurd this (Nat.lt_irrefl b)
Proof state after:
no goals
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hge : b / c ≥ a / c
⊢ a / c ≤ b / c
Tactic:
exact hge
Proof state after:
no goals
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ a / c ≤ b / c
Tactic:
have : c > 0 := (Nat.lt_or_ge 0 c).elim id $ by
  intro h; cases h; rw [Nat.div_zero, Nat.div_zero] at hlt; cases hlt
Proof state after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this : c > 0
⊢ a / c ≤ b / c
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this : c > 0
⊢ a / c ≤ b / c
Tactic:
have := (Nat.div_lt_iff_lt_mul ‹c>0›).mp hlt
Proof state after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝ : c > 0
this : b < a / c * c
⊢ a / c ≤ b / c
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝ : c > 0
this : b < a / c * c
⊢ a / c ≤ b / c
Tactic:
have := calc
  b < a/c*c := this
  _ ≤ a := Nat.div_mul_le_self a c
  _ ≤ b := hab
Proof state after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝¹ : c > 0
this✝ : b < a / c * c
this : b < b
⊢ a / c ≤ b / c
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this✝¹ : c > 0
this✝ : b < a / c * c
this : b < b
⊢ a / c ≤ b / c
Tactic:
exact absurd this (Nat.lt_irrefl b)
Proof state after:
no goals
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ 0 ≥ c → c > 0
Tactic:
intro h
Proof state after:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
h : 0 ≥ c
⊢ c > 0
Theorem: Nat.div_le_div
Proof state before:
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
h : 0 ≥ c
⊢ c > 0
Tactic:
cases h
Proof state after:
case refl
a b : Nat
hab : a ≤ b
hlt : b / 0 < a / 0
⊢ 0 > 0
Theorem: Nat.div_le_div
Proof state before:
case refl
a b : Nat
hab : a ≤ b
hlt : b / 0 < a / 0
⊢ 0 > 0
Tactic:
rw [Nat.div_zero, Nat.div_zero] at hlt
Proof state after:
case refl
a b : Nat
hab : a ≤ b
hlt : 0 < 0
⊢ 0 > 0
Theorem: Nat.div_le_div
Proof state before:
case refl
a b : Nat
hab : a ≤ b
hlt : 0 < 0
⊢ 0 > 0
Tactic:
cases hlt
Proof state after:
no goals
Theorem: Nat.mul_add_div_left
Proof state before:
y z x : Nat
⊢ x > 0 → (x * y + z) / x = y + z / x
Tactic:
intro h
Proof state after:
y z x : Nat
h : x > 0
⊢ (x * y + z) / x = y + z / x
Theorem: Nat.mul_add_div_left
Proof state before:
y z x : Nat
h : x > 0
⊢ (x * y + z) / x = y + z / x
Tactic:
rw [Nat.add_comm, Nat.add_mul_div_left z y h, Nat.add_comm]
Proof state after:
no goals
Theorem: Nat.mul_add_div_right
Proof state before:
x z y : Nat
⊢ y > 0 → (x * y + z) / y = x + z / y
Tactic:
intro h
Proof state after:
x z y : Nat
h : y > 0
⊢ (x * y + z) / y = x + z / y
Theorem: Nat.mul_add_div_right
Proof state before:
x z y : Nat
h : y > 0
⊢ (x * y + z) / y = x + z / y
Tactic:
rw [Nat.add_comm, Nat.add_mul_div_right z x h, Nat.add_comm]
Proof state after:
no goals
Theorem: Nat.mod_mul_mod
Proof state before:
a b n : Nat
⊢ a * b % n = (n * (a / n) + a % n) * b % n
Tactic:
conv => lhs; rw [←Nat.div_add_mod a n]
Proof state after:
no goals
Theorem: Nat.mod_mul_mod
Proof state before:
a b n : Nat
⊢ (n * (a / n) + a % n) * b % n = (n * (a / n * b) + a % n * b) % n
Tactic:
rw [Nat.right_distrib, Nat.mul_assoc]
Proof state after:
no goals
Theorem: Nat.mod_mul_mod
Proof state before:
a b n : Nat
⊢ (n * (a / n * b) + a % n * b) % n = a % n * b % n
Tactic:
rw [Nat.add_comm,Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: Nat.mod_mod_le
Proof state before:
a m n : Nat
⊢ m > 0 → m ≤ n → a % m % n = a % m
Tactic:
intro hm hle
Proof state after:
a m n : Nat
hm : m > 0
hle : m ≤ n
⊢ a % m % n = a % m
Theorem: Nat.mod_mod_le
Proof state before:
a m n : Nat
hm : m > 0
hle : m ≤ n
⊢ a % m % n = a % m
Tactic:
have : a % m < n := Trans.trans (Nat.mod_lt a hm) hle
Proof state after:
a m n : Nat
hm : m > 0
hle : m ≤ n
this : a % m < n
⊢ a % m % n = a % m
Theorem: Nat.mod_mod_le
Proof state before:
a m n : Nat
hm : m > 0
hle : m ≤ n
this : a % m < n
⊢ a % m % n = a % m
Tactic:
rw [Nat.mod_eq_of_lt this]
Proof state after:
no goals
Theorem: Nat.mod_mul_mod_left
Proof state before:
a m n : Nat
⊢ a % (m * n) % m = a % m
Tactic:
conv =>
  rhs;
  rw [←Nat.div_add_mod a (m*n), Nat.add_comm, Nat.mul_assoc]
  simp
Proof state after:
no goals
Theorem: Nat.mod_mul_mod_right
Proof state before:
a m n : Nat
⊢ a % (m * n) % n = a % n
Tactic:
rw [Nat.mul_comm, mod_mul_mod_left]
Proof state after:
no goals
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
⊢ l % (m * n) / m = l / m % n
Tactic:
cases m.eq_zero_or_pos
Proof state after:
case inl
l m n : Nat
h✝ : m = 0
⊢ l % (m * n) / m = l / m % n

case inr
l m n : Nat
h✝ : m > 0
⊢ l % (m * n) / m = l / m % n
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inl hm =>
  cases hm; simp
Proof state after:
no goals
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inr hm =>
cases n.eq_zero_or_pos
case inl hn =>
  cases hn; simp [Nat.mod_zero]
case inr hn =>
  conv =>
    rhs;
    rw [←Nat.div_add_mod l (m*n)]
    rw [Nat.add_comm, Nat.mul_assoc, Nat.add_mul_div_left _ _ hm]
    rw [Nat.add_mul_mod_self_left]
  apply (Nat.mod_eq_of_lt ?_).symm
  apply (div_lt_iff_lt_mul hm).mpr
  rw [Nat.mul_comm]
  exact Nat.mod_lt l (Nat.mul_pos hn hm)
Proof state after:
no goals
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
cases hm
Proof state after:
case refl
l n : Nat
⊢ l % (0 * n) / 0 = l / 0 % n
Theorem: Nat.mod_mul_div_left
Proof state before:
case refl
l n : Nat
⊢ l % (0 * n) / 0 = l / 0 % n
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
cases n.eq_zero_or_pos
Proof state after:
case inl
l m n : Nat
hm : m > 0
h✝ : n = 0
⊢ l % (m * n) / m = l / m % n

case inr
l m n : Nat
hm : m > 0
h✝ : n > 0
⊢ l % (m * n) / m = l / m % n