awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ count p (nth p n) = n
have zero : ∀ (hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))), count p (nth p 0) = 0
Tactic: induction n with
  | zero => exact count_nth_zero _
  | succ k ihk =>
    rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]
    simp
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
zero : ∀ (hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))), count p (nth p 0) = 0
⊢ count p (nth p n) = n
have succ : ∀ (k : ℕ) (ihk : ∀ (hn : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))), count p (nth p k) = k)
  (hn : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))), count p (nth p (k + 1)) = k + 1
Tactic: induction n with
  | zero => exact count_nth_zero _
  | succ k ihk =>
    rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]
    simp
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ count p (nth p n + 1) = n + 1
have rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
Tactic: rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
⊢ count p (nth p n + 1) = n + 1
have rw₁ : (n + if p (nth p n) then 1 else 0) = n + 1
Tactic: rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
rw₁ : (n + if p (nth p n) then 1 else 0) = n + 1
⊢ count p (nth p n + 1) = n + 1
have rw₂ : n + 1 = n + 1
Tactic: rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
⊢ count p (nth p n + 1) = n + 1
have rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
Tactic: rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
⊢ count p (nth p n + 1) = n + 1
have rw₁ : (n + if p (nth p n) then 1 else 0) = n + 1
Tactic: rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
rw₁ : (n + if p (nth p n) then 1 else 0) = n + 1
⊢ count p (nth p n + 1) = n + 1
have rw₂ : n + 1 = n + 1
Tactic: rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n
have refine : count p (nth p k) < count p n
Tactic: refine (count_monotone p).reflect_lt ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
⊢ count p (nth p k) < count p n
have rwa : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))
Tactic: rwa [count_nth]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
⊢ count p n = 0 ↔ n ≤ nth p 0
have rw : count p n = 0 ↔ n ≤ Nat.find (p := p) h
Tactic: rw [nth_zero_of_exists h, le_find_iff h, Nat.count_iff_forall_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
rw : count p n = 0 ↔ n ≤ Nat.find (p := p) h
⊢ count p n = 0 ↔ n ≤ nth p 0
have rw₁ : count p n = 0 ↔ ∀ m < n, ¬p m
Tactic: rw [nth_zero_of_exists h, le_find_iff h, Nat.count_iff_forall_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
rw : count p n = 0 ↔ n ≤ Nat.find (p := p) h
rw₁ : count p n = 0 ↔ ∀ m < n, ¬p m
⊢ count p n = 0 ↔ n ≤ nth p 0
have rw₂ : (∀ m < n, ¬p m) ↔ ∀ m < n, ¬p m
Tactic: rw [nth_zero_of_exists h, le_find_iff h, Nat.count_iff_forall_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i}
have refine : Eq (α := Set ℕ) {x : ℕ | p x ∧ ∀ k < count p n, nth p k < x} {i : ℕ | p i ∧ n ≤ i}
Tactic: refine (nth_eq_sInf _ _).trans (congr_arg sInf ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ Eq (α := Set ℕ) {x : ℕ | p x ∧ ∀ k < count p n, nth p k < x} {i : ℕ | p i ∧ n ≤ i}
have refine : ∀ (a : ℕ) (hpa : p a), (∀ k < count p n, nth p k < a) ↔ n ≤ a
Tactic: refine Set.ext fun a => and_congr_right fun hpa => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a
have refine : ∀ (h : ∀ k < count p n, nth p k < a) (ha : a < n), False
Tactic: refine ⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
⊢ False
have hn : nth p (count p a) < a
Tactic: have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : nth p (count p a) < a
⊢ False
have rwa : ∀ (hn : a < a), False
Tactic: rwa [nth_count hpa, lt_self_iff_false] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : nth p (count p a) < a
rwa : ∀ (hn : a < a), False
⊢ False
have rwa₁ : ∀ (hn : False), False
Tactic: rwa [nth_count hpa, lt_self_iff_false] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
⊢ nth p n = n
have nth_rw : nth p (count p n) = n
Tactic: nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
nth_rw : nth p (count p n) = n
⊢ nth p n = n
have nth_rw₁ : n = n
Tactic: nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
⊢ nth p n = n
have classical : nth p (count p n) = n
Tactic: classical nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
classical : nth p (count p n) = n
⊢ nth p n = n
have classical₁ : n = n
Tactic: classical nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
hn' : n' ∈ setOf p
⊢ n' ∈ (↑(range n) : Set ℕ)
have contrapose! : ∀ (hp : n' ∉ (↑(range n) : Set ℕ)), ∃ n' ≥ n, p n'
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ nth p n = 0
have this : setOf p ⊆ (↑(range n) : Set ℕ)
Tactic: have : setOf p ⊆ Finset.range n := by
    intro n' hn'
    contrapose! hp
    exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
⊢ nth p n = 0
have rw : #(sorry.toFinset (s := setOf p)) ≤ n
Tactic: rw [nth_of_card_le ((finite_toSet _).subset this)]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
⊢ #(⋯.toFinset (s := setOf p)) ≤ n
have refine : sorry.toFinset (s := setOf p) ⊆ range n
Tactic: refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (hypothesis)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)
have hk : p k
Tactic: have hk : p k := Nat.find_spec H
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (goal)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)
have suffices : 0 < k
Tactic: suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (goal)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
⊢ 0 < k
have by_contra! : ∀ (contra : k ≤ 0), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (hypothesis)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
contra : k ≤ 0
⊢ False
have contra₁ : k = 0
Tactic: rw [le_zero_eq] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (goal)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
let let₁ let₂ : ∃ (n : ℕ), ¬p n ∧ p (n + 1)
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)
have let₃ : let k := Nat.find (p := p) H;
∀ (hk : p k), ∃ (n : ℕ), ¬p n ∧ p (n + 1)
Tactic: classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (goal)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
let let₁ let₂ : ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₃ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), ∃ (n : ℕ), ¬p n ∧ p (n + 1)
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)
have let₄ : let k := Nat.find (p := p) H;
∀ (hk : p k), 0 < k
Tactic: classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (goal)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
let let₁ let₂ : ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₃ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₄ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), 0 < k
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)
have let₅ : let k := Nat.find (p := p) H;
∀ (hk : p k) (contra : k ≤ 0), False
Tactic: classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)
-- Lean 4 proof step from Mathlib.Data.Nat.Order.Lemmas (goal)
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
let let₁ let₂ : ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₃ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₄ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), 0 < k
let₅ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k) (contra : k ≤ 0), False
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)
have let₆ : let k := Nat.find (p := p) H;
∀ (hk : p k) (contra : k = 0), False
Tactic: classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
n : ℕ
⊢ n.pred = n.ppred.getD 0
have zero : pred 0 = (ppred 0).getD 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
n : ℕ
zero : pred 0 = (ppred 0).getD 0
⊢ n.pred = n.ppred.getD 0
have succ : ∀ (n : ℕ), (n + 1).pred = (n + 1).ppred.getD 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
⊢ (m - n).ppred.getD 0 = (m.psub (n + 1)).getD 0
have rw : ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0
Tactic: rw [sub_eq_psub m n, psub]
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0
have none : (ppred (Option.getD none 0)).getD 0 = (none >>= ppred).getD 0
Tactic: cases psub m n
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
none : (ppred (Option.getD Option.none 0)).getD 0 = (Option.none >>= ppred).getD 0
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0
have some : ∀ (val : ℕ), ((some val).getD 0).ppred.getD 0 = (some val >>= ppred).getD 0
Tactic: cases psub m n
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m : ℕ
⊢ ppred 0 = some m ↔ m.succ = 0
have mp : ppred 0 = some m → m.succ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m : ℕ
mp : ppred 0 = some m → m.succ = 0
⊢ ppred 0 = some m ↔ m.succ = 0
have mpr : m.succ = 0 → ppred 0 = some m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
⊢ (n + 1).ppred = some m ↔ m.succ = n + 1
have mp : (n + 1).ppred = some m → m.succ = n + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
mp : (n + 1).ppred = some m → m.succ = n + 1
⊢ (n + 1).ppred = some m ↔ m.succ = n + 1
have mpr : m.succ = n + 1 → (n + 1).ppred = some m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (hypothesis)
Goal:
m n : ℕ
h : (n + 1).ppred = some m
⊢ m.succ = n + 1
have val_eq : n = m
Tactic: injection h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (hypothesis)
Goal:
m n : ℕ
h : m.succ = n + 1
⊢ (n + 1).ppred = some m
have n_eq : m = n
Tactic: injection h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
val_eq : n = m
⊢ m.succ = n + 1
have mp : n.succ = n + 1
Tactic: subst m
Cleared hypotheses: m, val_eq
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
n_eq : m = n
⊢ (n + 1).ppred = some m
have mpr : (n + 1).ppred = some n
Tactic: subst m
Cleared hypotheses: m, n_eq
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
n : ℕ
⊢ (n + 1).ppred = none ↔ n + 1 = 0
have mp : (n + 1).ppred = none → n + 1 = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
n : ℕ
mp : (n + 1).ppred = none → n + 1 = 0
⊢ (n + 1).ppred = none ↔ n + 1 = 0
have mpr : n + 1 = 0 → (n + 1).ppred = none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n k : ℕ
⊢ m.psub (n + 1) = some k ↔ k + (n + 1) = m
have apply : (∃ (a : ℕ), m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m
Tactic: apply Option.bind_eq_some_iff.trans
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n k : ℕ
⊢ (∃ (a : ℕ), m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m
have simp : (∃ (a : ℕ), a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m
Tactic: simp only [psub_eq_some, ppred_eq_some]
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
⊢ m.psub n = none ↔ m < n
have none : ∀ (s : m.psub n = none), Eq (α := Option ℕ) none none ↔ m < n
Tactic: rcases s : psub m n
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
none : ∀ (s : m.psub n = Option.none), Eq (α := Option ℕ) Option.none Option.none ↔ m < n
⊢ m.psub n = Option.none ↔ m < n
have some : ∀ (val : ℕ) (s : m.psub n = some val), some val = Option.none ↔ m < n
Tactic: rcases s : psub m n
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
s : m.psub n = none
⊢ Eq (α := Option ℕ) none none ↔ m < n
have none : m < n
Tactic: simp only [true_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
s : m.psub n = none
⊢ m < n
have none : ∀ (h : n ≤ m), False
Tactic: refine lt_of_not_ge fun h => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
s : m.psub n = none
h : n ≤ m
⊢ False
have none : ∀ (k : ℕ) (e : n + k = m), False
Tactic: obtain ⟨k, e⟩ := le.dest h
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n k : ℕ
⊢ m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k
have zero : m.psub (n + 0) = do
  let __do_lift ← m.psub n
  __do_lift.psub 0
Tactic: induction k with
    | zero => simp
    | succ n ih => simp only [ih, add_succ, psub_succ, bind_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n k : ℕ
zero :
  m.psub (n + 0) = do
    let __do_lift ← m.psub n
    __do_lift.psub 0
⊢ m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k
have succ : ∀ (n_1 : ℕ)
  (ih :
    m.psub (n + n_1) = do
      let __do_lift ← m.psub n
      __do_lift.psub n_1),
  m.psub (n + (n_1 + 1)) = do
    let __do_lift ← m.psub n
    __do_lift.psub (n_1 + 1)
Tactic: induction k with
    | zero => simp
    | succ n ih => simp only [ih, add_succ, psub_succ, bind_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = m.psub n
have pos : ∀ (h : n ≤ m), some (m - n) = m.psub n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.PSub (goal)
Goal:
m n : ℕ
pos : ∀ (h : n ≤ m), some (m - n) = m.psub n
⊢ (if n ≤ m then some (m - n) else none) = m.psub n
have neg : ∀ (h : ¬n ≤ m), none = m.psub n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
n : ℕ
s : ℕ := n.sqrt
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n
have sm : s * s + (n - s * s) = n
Tactic: have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n
have pos : ∀ (h : n - n.sqrt * n.sqrt < n.sqrt), pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
pos : ∀ (h : n - n.sqrt * n.sqrt < n.sqrt), pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n
have neg : ∀ (h : ¬n - n.sqrt * n.sqrt < n.sqrt),
  pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + (s + s)
have rw : n ≤ s * s + s + s
Tactic: rw [← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n
have hl : n - s * s - s ≤ s
Tactic: have hl : n - s * s - s ≤ s := Nat.sub_le_iff_le_add.2
      (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
have pos : ∀ (h : a < b), unpair (b * b + a) = (a, b)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b : ℕ
pos : ∀ (h : a < b), unpair (b * b + a) = (a, b)
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
have neg : ∀ (h : ¬a < b), unpair (a * a + a + b) = (a, b)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)
have be : (b * b + a).sqrt = b
Tactic: have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b : ℕ
h : ¬a < b
⊢ (a * a + (a + b)).sqrt = a
have h₁ : a + b ≤ a + a
Tactic: rw [sqrt_add_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
have ae : (a * a + (a + b)).sqrt = a
Tactic: have ae : sqrt (a * a + (a + b)) = a := by
      rw [sqrt_add_eq]
      exact Nat.add_le_add_left (le_of_not_gt h) _
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
have pos : ∀ (h : n - s * s < s),
  (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
Tactic: by_cases h : n - s * s < s
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
pos :
  ∀ (h : n - s * s < s),
    (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 <
      n
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
have neg : ∀ (h : ¬n - s * s < s),
  (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
Tactic: by_cases h : n - s * s < s
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
have pos : n - n.sqrt * n.sqrt < n
Tactic: simp only [h, ↓reduceIte, gt_iff_lt, s]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
have neg : n.sqrt < n
Tactic: simp only [h, ↓reduceIte, gt_iff_lt, s]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n
have h₁ : s ≤ n - s * s
Tactic: simp only [not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
⊢ n.sqrt < n
have s0 : 0 < s
Tactic: have s0 : 0 < s := sqrt_pos.2 n1
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b : ℕ
⊢ b ≤ pair a b
have pos : ∀ (h : a < b), b ≤ pair a b
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b : ℕ
pos : ∀ (h : a < b), b ≤ pair a b
⊢ b ≤ pair a b
have neg : ∀ (h : ¬a < b), b ≤ pair a b
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b
have pos : ∀ (h₁ : a₁ < b), pair a₁ b < pair a₂ b
Tactic: by_cases h₁ : a₁ < b