internlm/Lean-Github huggingface dataset:
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
case inl hn =>
  cases hn; simp [Nat.mod_zero]
Proof state after:
no goals
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
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
hn : n = 0
⊢ l % (m * n) / m = l / m % n
Tactic:
cases hn
Proof state after:
case refl
l m : Nat
hm : m > 0
⊢ l % (m * 0) / m = l / m % 0
Theorem: Nat.mod_mul_div_left
Proof state before:
case refl
l m : Nat
hm : m > 0
⊢ l % (m * 0) / m = l / m % 0
Tactic:
simp [Nat.mod_zero]
Proof state after:
no goals
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l / m % n
Tactic:
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]
Proof state after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l % (m * n) / m % n
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m = l % (m * n) / m % n
Tactic:
apply (Nat.mod_eq_of_lt ?_).symm
Proof state after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m < n
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) / m < n
Tactic:
apply (div_lt_iff_lt_mul hm).mpr
Proof state after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) < n * m
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (m * n) < n * m
Tactic:
rw [Nat.mul_comm]
Proof state after:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (n * m) < n * m
Theorem: Nat.mod_mul_div_left
Proof state before:
l m n : Nat
hm : m > 0
hn : n > 0
⊢ l % (n * m) < n * m
Tactic:
exact Nat.mod_lt l (Nat.mul_pos hn hm)
Proof state after:
no goals
Theorem: Nat.mod_mul_div_right
Proof state before:
l m n : Nat
⊢ l % (m * n) / n = l / n % m
Tactic:
rw [Nat.mul_comm, mod_mul_div_left]
Proof state after:
no goals
Theorem: Nat.mul_sub_mod_left
Proof state before:
l m n : Nat
⊢ m > 0 → l ≥ n → (l * m - n) % l = (l - n) % l
Tactic:
intro hm hln
Proof state after:
l m n : Nat
hm : m > 0
hln : l ≥ n
⊢ (l * m - n) % l = (l - n) % l
Theorem: Nat.mul_sub_mod_left
Proof state before:
l m n : Nat
hm : m > 0
hln : l ≥ n
⊢ (l * m - n) % l = (l - n) % l
Tactic:
cases hm
Proof state after:
case refl
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l

case step
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l
Theorem: Nat.mul_sub_mod_left
Proof state before:
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l
Tactic:
case refl => rw [Nat.mul_one]
Proof state after:
no goals
Theorem: Nat.mul_sub_mod_left
Proof state before:
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l
Tactic:
case step _ _ =>
  rw [mul_succ, Nat.add_sub_assoc hln, Nat.add_comm, Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: Nat.mul_sub_mod_left
Proof state before:
l n : Nat
hln : l ≥ n
⊢ (l * succ 0 - n) % l = (l - n) % l
Tactic:
rw [Nat.mul_one]
Proof state after:
no goals
Theorem: Nat.mul_sub_mod_left
Proof state before:
l n : Nat
hln : l ≥ n
m✝ : Nat
a✝ : Nat.le (succ 0) m✝
⊢ (l * succ m✝ - n) % l = (l - n) % l
Tactic:
rw [mul_succ, Nat.add_sub_assoc hln, Nat.add_comm, Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: Nat.mul_sub_mod_right
Proof state before:
l m n : Nat
⊢ l > 0 → m ≥ n → (l * m - n) % m = (m - n) % m
Tactic:
intro hl hmn
Proof state after:
l m n : Nat
hl : l > 0
hmn : m ≥ n
⊢ (l * m - n) % m = (m - n) % m
Theorem: Nat.mul_sub_mod_right
Proof state before:
l m n : Nat
hl : l > 0
hmn : m ≥ n
⊢ (l * m - n) % m = (m - n) % m
Tactic:
rw [Nat.mul_comm, mul_sub_mod_left hl hmn]
Proof state after:
no goals
Theorem: Nat.exp_lt_pow
Proof state before:
n i : Nat
⊢ n ≥ 2 → i < n ^ i
Tactic:
intro h
Proof state after:
n i : Nat
h : n ≥ 2
⊢ i < n ^ i
Theorem: Nat.exp_lt_pow
Proof state before:
n i : Nat
h : n ≥ 2
⊢ i < n ^ i
Tactic:
induction i
Proof state after:
case zero
n : Nat
h : n ≥ 2
⊢ zero < n ^ zero

case succ
n : Nat
h : n ≥ 2
n✝ : Nat
n_ih✝ : n✝ < n ^ n✝
⊢ succ n✝ < n ^ succ n✝
Theorem: Nat.exp_lt_pow
Proof state before:
n : Nat
h : n ≥ 2
⊢ zero < n ^ zero
Tactic:
case zero => exact Nat.le.refl
Proof state after:
no goals
Theorem: Nat.exp_lt_pow
Proof state before:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
⊢ succ i < n ^ succ i
Tactic:
case succ i h_ind =>
have : n^i > 0 := Nat.pos_pow_of_pos i (Nat.lt_of_succ_lt h)
calc
  i+1 < n^i + 1 := succ_lt_succ h_ind
  _   ≤ n^i + n^i := Nat.add_le_add_left this _
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left _ h
  _   = n^(i+1) := rfl
Proof state after:
no goals
Theorem: Nat.exp_lt_pow
Proof state before:
n : Nat
h : n ≥ 2
⊢ zero < n ^ zero
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: Nat.exp_lt_pow
Proof state before:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
⊢ succ i < n ^ succ i
Tactic:
have : n^i > 0 := Nat.pos_pow_of_pos i (Nat.lt_of_succ_lt h)
Proof state after:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
this : n ^ i > 0
⊢ succ i < n ^ succ i
Theorem: Nat.exp_lt_pow
Proof state before:
n : Nat
h : n ≥ 2
i : Nat
h_ind : i < n ^ i
this : n ^ i > 0
⊢ succ i < n ^ succ i
Tactic:
calc
  i+1 < n^i + 1 := succ_lt_succ h_ind
  _   ≤ n^i + n^i := Nat.add_le_add_left this _
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left _ h
  _   = n^(i+1) := rfl
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_right
Proof state before:
n i j : Nat
⊢ n ≥ 2 → i < j → n ^ i < n ^ j
Tactic:
intro hn hij
Proof state after:
n i j : Nat
hn : n ≥ 2
hij : i < j
⊢ n ^ i < n ^ j
Theorem: Nat.pow_lt_pow_right
Proof state before:
n i j : Nat
hn : n ≥ 2
hij : i < j
⊢ n ^ i < n ^ j
Tactic:
induction hij
Proof state after:
case refl
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i

case step
n i j : Nat
hn : n ≥ 2
m✝ : Nat
a✝ : Nat.le (succ i) m✝
a_ih✝ : n ^ i < n ^ m✝
⊢ n ^ i < n ^ succ m✝
Theorem: Nat.pow_lt_pow_right
Proof state before:
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i
Tactic:
case refl => calc
  n^i < n^i + n^i := Nat.lt_add_of_pos_left (Nat.pos_pow_of_pos i (trans (Nat.zero_lt_succ 1) hn))
  _   = n^i*2 := (Nat.mul_two _).symm
  _   ≤ n^i*n := Nat.mul_le_mul_left (n^i) hn
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_right
Proof state before:
n i j✝ : Nat
hn : n ≥ 2
j : Nat
a✝ : Nat.le (succ i) j
h_ind : n ^ i < n ^ j
⊢ n ^ i < n ^ succ j
Tactic:
case step j _ h_ind => calc
  n^i < n^j := h_ind
  _   ≤ n^j + n^j := Nat.le_add_left _ _
  _   = n^j*2 := (Nat.mul_two _).symm
  _   ≤ n^j*n := Nat.mul_le_mul_left _ hn
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_right
Proof state before:
n i j : Nat
hn : n ≥ 2
⊢ n ^ i < n ^ succ i
Tactic:
calc
n^i < n^i + n^i := Nat.lt_add_of_pos_left (Nat.pos_pow_of_pos i (trans (Nat.zero_lt_succ 1) hn))
_   = n^i*2 := (Nat.mul_two _).symm
_   ≤ n^i*n := Nat.mul_le_mul_left (n^i) hn
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_right
Proof state before:
n i j✝ : Nat
hn : n ≥ 2
j : Nat
a✝ : Nat.le (succ i) j
h_ind : n ^ i < n ^ j
⊢ n ^ i < n ^ succ j
Tactic:
calc
n^i < n^j := h_ind
_   ≤ n^j + n^j := Nat.le_add_left _ _
_   = n^j*2 := (Nat.mul_two _).symm
_   ≤ n^j*n := Nat.mul_le_mul_left _ hn
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_left
Proof state before:
m n i : Nat
⊢ m < n → i > 0 → m ^ i < n ^ i
Tactic:
intro hmn hi
Proof state after:
m n i : Nat
hmn : m < n
hi : i > 0
⊢ m ^ i < n ^ i
Theorem: Nat.pow_lt_pow_left
Proof state before:
m n i : Nat
hmn : m < n
hi : i > 0
⊢ m ^ i < n ^ i
Tactic:
cases i
Proof state after:
case zero
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero

case succ
m n : Nat
hmn : m < n
n✝ : Nat
hi : succ n✝ > 0
⊢ m ^ succ n✝ < n ^ succ n✝
Theorem: Nat.pow_lt_pow_left
Proof state before:
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero
Tactic:
case zero => cases hi
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_left
Proof state before:
m n : Nat
hmn : m < n
i : Nat
hi : succ i > 0
⊢ m ^ succ i < n ^ succ i
Tactic:
case succ i => calc
  m^i.succ = m^i * m := rfl
  _        ≤ n^i * m := Nat.mul_le_mul_right m (Nat.pow_le_pow_of_le_left (Nat.le_of_lt hmn) i)
  _        < n^i * n := Nat.mul_lt_mul_of_pos_left hmn (Nat.pos_pow_of_pos i (trans m.zero_le hmn))
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_left
Proof state before:
m n : Nat
hmn : m < n
hi : zero > 0
⊢ m ^ zero < n ^ zero
Tactic:
cases hi
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_left
Proof state before:
m n : Nat
hmn : m < n
i : Nat
hi : succ i > 0
⊢ m ^ succ i < n ^ succ i
Tactic:
calc
m^i.succ = m^i * m := rfl
_        ≤ n^i * m := Nat.mul_le_mul_right m (Nat.pow_le_pow_of_le_left (Nat.le_of_lt hmn) i)
_        < n^i * n := Nat.mul_lt_mul_of_pos_left hmn (Nat.pos_pow_of_pos i (trans m.zero_le hmn))
Proof state after:
no goals
Theorem: Nat.compare_lt
Proof state before:
m n : Nat
⊢ m < n → compare m n = Ordering.lt
Tactic:
intro h
Proof state after:
m n : Nat
h : m < n
⊢ compare m n = Ordering.lt
Theorem: Nat.compare_lt
Proof state before:
m n : Nat
h : m < n
⊢ compare m n = Ordering.lt
Tactic:
simp [compare, instOrdNat, compareOfLessAndEq]
Proof state after:
m n : Nat
h : m < n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.lt
Theorem: Nat.compare_lt
Proof state before:
m n : Nat
h : m < n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
rw [if_pos h]
Proof state after:
no goals
Theorem: Nat.compare_eq
Proof state before:
m n : Nat
⊢ m = n → compare m n = Ordering.eq
Tactic:
intro h
Proof state after:
m n : Nat
h : m = n
⊢ compare m n = Ordering.eq
Theorem: Nat.compare_eq
Proof state before:
m n : Nat
h : m = n
⊢ compare m n = Ordering.eq
Tactic:
cases h
Proof state after:
case refl
m : Nat
⊢ compare m m = Ordering.eq
Theorem: Nat.compare_eq
Proof state before:
case refl
m : Nat
⊢ compare m m = Ordering.eq
Tactic:
simp [compare, instOrdNat, compareOfLessAndEq]
Proof state after:
no goals
Theorem: Nat.compare_gt
Proof state before:
m n : Nat
⊢ m > n → compare m n = Ordering.gt
Tactic:
intro h
Proof state after:
m n : Nat
h : m > n
⊢ compare m n = Ordering.gt
Theorem: Nat.compare_gt
Proof state before:
m n : Nat
h : m > n
⊢ compare m n = Ordering.gt
Tactic:
simp [compare, instOrdNat, compareOfLessAndEq]
Proof state after:
m n : Nat
h : m > n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.gt
Theorem: Nat.compare_gt
Proof state before:
m n : Nat
h : m > n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.gt
Tactic:
rw [if_neg (Nat.lt_asymm h), if_neg (Nat.ne_of_lt h).symm]
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
⊢ (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
Tactic:
induction n
Proof state after:
case zero
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i

case succ
p : Nat → Prop
inst✝ : DecidablePred p
n✝ : Nat
n_ih✝ : (∃ i, i < n✝ ∧ p i) ∨ ∀ (i : Nat), i < n✝ → ¬p i
⊢ (∃ i, i < succ n✝ ∧ p i) ∨ ∀ (i : Nat), i < succ n✝ → ¬p i
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i
Tactic:
case zero => exact Or.inr (λ _ h => by cases h)
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h_ind : (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
case succ n h_ind =>
  cases h_ind
  case inl hex =>
    cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
  case inr hall =>
    if hpn : p n
    then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
    else
      apply Or.inr
      intro i hi
      cases hi
      case refl => exact hpn
      case step hstep => exact hall i hstep
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i
Tactic:
exact Or.inr (λ _ h => by cases h)
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
x✝ : Nat
h : x✝ < zero
⊢ ¬p x✝
Tactic:
cases h
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h_ind : (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
cases h_ind
Proof state after:
case inl
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h✝ : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i

case inr
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h✝ : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hex : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
case inl hex =>
  cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
case inr hall =>
  if hpn : p n
  then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
  else
    apply Or.inr
    intro i hi
    cases hi
    case refl => exact hpn
    case step hstep => exact hall i hstep
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hex : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
case intro
p : Nat → Prop
inst✝ : DecidablePred p
n i : Nat
hi : i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
if hpn : p n
then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
else
  apply Or.inr
  intro i hi
  cases hi
  case refl => exact hpn
  case step hstep => exact hall i hstep
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : p n
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
apply Or.inr
Proof state after:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ∀ (i : Nat), i < succ n → ¬p i
Theorem: Nat.exists_or_forall_not
Proof state before:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
intro i hi
Proof state after:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hi : i < succ n
⊢ ¬p i
Theorem: Nat.exists_or_forall_not
Proof state before:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hi : i < succ n
⊢ ¬p i
Tactic:
cases hi
Proof state after:
case h.refl
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ¬p n

case h.step
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
a✝ : Nat.le (succ i) n
⊢ ¬p i
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ¬p n
Tactic:
case refl => exact hpn
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hstep : Nat.le (succ i) n
⊢ ¬p i
Tactic:
case step hstep => exact hall i hstep
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ¬p n
Tactic:
exact hpn
Proof state after:
no goals
Theorem: Nat.exists_or_forall_not
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hstep : Nat.le (succ i) n
⊢ ¬p i
Tactic:
exact hall i hstep
Proof state after:
no goals
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM f init (n + 1) = do
    let x ← f 0 init
    foldM (f ∘ succ) x n
Tactic:
unfold foldM
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM.loop f (n + 1) (n + 1) init = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM.loop f (n + 1) (n + 1) init = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Tactic:
conv =>
  lhs; unfold foldM.loop
  simp only [Nat.add_eq, Nat.add_zero, Nat.add_sub_cancel_left, Nat.sub_self]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ f 0 init >>= foldM.loop f (n + 1) n = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ f 0 init >>= foldM.loop f (n + 1) n = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Tactic:
suffices ∀ k, k ≤ n → foldM.loop f (n+1) k = foldM.loop (f ∘ succ) n k
  by rw [this n .refl]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
Tactic:
intro k hk
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
hk : k ≤ n
⊢ foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
hk : k ≤ n
⊢ foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
Tactic:
induction k
Proof state after:
case zero
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
hk : zero ≤ n
⊢ foldM.loop f (n + 1) zero = foldM.loop (f ∘ succ) n zero

case succ
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n n✝ : Nat
n_ih✝ : n✝ ≤ n → foldM.loop f (n + 1) n✝ = foldM.loop (f ∘ succ) n n✝
hk : succ n✝ ≤ n
⊢ foldM.loop f (n + 1) (succ n✝) = foldM.loop (f ∘ succ) n (succ n✝)
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
hk : zero ≤ n
⊢ foldM.loop f (n + 1) zero = foldM.loop (f ∘ succ) n zero
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ foldM.loop f (n + 1) (succ k) = foldM.loop (f ∘ succ) n (succ k)
Tactic:
case succ k h_ind =>
  dsimp [foldM.loop]
  have := calc
    n+1-k-1 = n.succ - k.succ := by simp only [Nat.sub_sub]
    _       = n-k := Nat.succ_sub_succ ..
  have := calc
    succ (n-k-1) = n-k-1+1 := rfl
    _            = n-k := Nat.sub_add_cancel (Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ hk))
  rw [‹n+1-k-1=n-k›, ‹succ (n-k-1)=n-k›]
  rw [h_ind (Nat.le_of_succ_le hk)]
Proof state after:
no goals
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
this : ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
⊢ f 0 init >>= foldM.loop f (n + 1) n = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Tactic:
rw [this n .refl]
Proof state after:
no goals
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
hk : zero ≤ n
⊢ foldM.loop f (n + 1) zero = foldM.loop (f ∘ succ) n zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ foldM.loop f (n + 1) (succ k) = foldM.loop (f ∘ succ) n (succ k)
Tactic:
dsimp [foldM.loop]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Tactic:
have := calc
  n+1-k-1 = n.succ - k.succ := by simp only [Nat.sub_sub]
  _       = n-k := Nat.succ_sub_succ ..
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this : n + 1 - k - 1 = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Theorem: Nat.foldM_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this : n + 1 - k - 1 = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Tactic:
have := calc
  succ (n-k-1) = n-k-1+1 := rfl
  _            = n-k := Nat.sub_add_cancel (Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ hk))
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k