awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
l : List α
hl : ∀ (x : α), x ∈ l → p x
succ :
  ∀ (hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
    (pmap (P := p) f [] hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (insertIdx [] (n + 1) a) ⋯
⊢ (pmap (P := p) f l hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (l.insertIdx (n + 1) a) ⋯
have succ₁ : ∀ (head : α) (tail : List α) (hl : ∀ (x : α), x ∈ head :: tail → p x),
  (pmap (P := p) f (head :: tail) hl).insertIdx (n + 1) (f a ha) =
    pmap (P := p) f ((head :: tail).insertIdx (n + 1) a) sorry
Tactic: cases l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
a : α
n : ℕ
hl : ∀ (x : α), x ∈ l → p x
ha : p a
⊢ (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
have zero : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
  (pmap (P := p) f l hl).insertIdx 0 (f a ha) = pmap (P := p) f (l.insertIdx 0 a) sorry
Tactic: induction n generalizing l with
  | zero => cases l <;> simp
  | succ n ihn => cases l <;> simp_all
Cleared hypotheses: l, n, hl
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
a : α
n : ℕ
hl : ∀ (x : α), x ∈ l → p x
ha : p a
zero :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx 0 (f a ha) = pmap (P := p) f (l.insertIdx 0 a) ⋯
⊢ (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
have succ : ∀ (n : ℕ)
  (ihn :
    ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
      (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) sorry)
  {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
  (pmap (P := p) f l hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (l.insertIdx (n + 1) a) sorry
Tactic: induction n generalizing l with
  | zero => cases l <;> simp
  | succ n ihn => cases l <;> simp_all
Cleared hypotheses: l, n, hl
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n_1 : ℕ
a : α
as : List α
h : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
n : ℕ
⊢ (pmap (P := p) f (a :: as) h).eraseIdx (n + 1) = pmap (P := p) f ((a :: as).eraseIdx (n + 1)) ⋯
have rw : ∀ (h_1 : p a ∧ ∀ (x : α), x ∈ as → p x) (n : ℕ),
  (pmap (P := p) f (a :: as) h).eraseIdx (n + 1) = pmap (P := p) f ((a :: as).eraseIdx (n + 1)) sorry
Tactic: rw [forall_mem_cons] at h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
⊢ n < (l.insertIdx n x).length
have rwa : n < l.length + 1
Tactic: rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < (l.insertIdx n x).length
have rwa : n + k + 1 < l.length + 1
Tactic: rwa [length_insertIdx_of_le_length (by lia), Nat.succ_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n : ℕ
⊢ Ico 0 n = range n
have rw : range' 0 (n - 0) = range n
Tactic: rw [Ico, Nat.sub_zero, range_eq_range']
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n : ℕ
rw : range' 0 (n - 0) = range n
⊢ Ico 0 n = range n
have rw₁ : range' 0 n = range n
Tactic: rw [Ico, Nat.sub_zero, range_eq_range']
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n : ℕ
rw : range' 0 (n - 0) = range n
rw₁ : range' 0 n = range n
⊢ Ico 0 n = range n
have rw₂ : range' 0 n = range' 0 n
Tactic: rw [Ico, Nat.sub_zero, range_eq_range']
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m
have suffices : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
Tactic: suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
⊢ map (fun (x : ℕ) ↦ k + x) (Ico n m) = Ico (n + k) (m + k)
have rw : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = Ico (n + k) (m + k)
Tactic: rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
rw : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = Ico (n + k) (m + k)
⊢ map (fun (x : ℕ) ↦ k + x) (Ico n m) = Ico (n + k) (m + k)
have rw₁ : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = range' (n + k) (m + k - (n + k))
Tactic: rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
rw : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = Ico (n + k) (m + k)
rw₁ : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = range' (n + k) (m + k - (n + k))
⊢ map (fun (x : ℕ) ↦ k + x) (Ico n m) = Ico (n + k) (m + k)
have rw₂ : range' (k + n) (m - n) = range' (n + k) (m + k - (n + k))
Tactic: rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
rw : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = Ico (n + k) (m + k)
rw₁ : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = range' (n + k) (m + k - (n + k))
rw₂ : range' (k + n) (m - n) = range' (n + k) (m + k - (n + k))
⊢ map (fun (x : ℕ) ↦ k + x) (Ico n m) = Ico (n + k) (m + k)
have rw₃ : range' (k + n) (m - n) = range' (n + k) (m - n)
Tactic: rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
rw : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = Ico (n + k) (m + k)
rw₁ : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = range' (n + k) (m + k - (n + k))
rw₂ : range' (k + n) (m - n) = range' (n + k) (m + k - (n + k))
rw₃ : range' (k + n) (m - n) = range' (n + k) (m - n)
⊢ map (fun (x : ℕ) ↦ k + x) (Ico n m) = Ico (n + k) (m + k)
have rw₄ : range' (k + n) (m - n) = range' (k + n) (m - n)
Tactic: rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
h₁ : k ≤ n
⊢ map (fun (x : ℕ) ↦ x - k) (Ico n m) = Ico (n - k) (m - k)
have rw : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = Ico (n - k) (m - k)
Tactic: rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
h₁ : k ≤ n
rw : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = Ico (n - k) (m - k)
⊢ map (fun (x : ℕ) ↦ x - k) (Ico n m) = Ico (n - k) (m - k)
have rw₁ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - k - (n - k))
Tactic: rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
h₁ : k ≤ n
rw : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = Ico (n - k) (m - k)
rw₁ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - k - (n - k))
⊢ map (fun (x : ℕ) ↦ x - k) (Ico n m) = Ico (n - k) (m - k)
have rw₂ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - n)
Tactic: rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m k : ℕ
h₁ : k ≤ n
rw : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = Ico (n - k) (m - k)
rw₁ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - k - (n - k))
rw₂ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - n)
⊢ map (fun (x : ℕ) ↦ x - k) (Ico n m) = Ico (n - k) (m - k)
have rw₃ : range' (n - k) (m - n) = range' (n - k) (m - n)
Tactic: rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : Ico n m = []
⊢ m - n = 0
have rw : (Ico n m).length = 0
Tactic: rw [← length, h, List.length]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : Ico n m = []
rw : (Ico n m).length = 0
⊢ m - n = 0
have rw₁ : List.length (α := ℕ) [] = 0
Tactic: rw [← length, h, List.length]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : Ico n m = []
rw : (Ico n m).length = 0
rw₁ : List.length (α := ℕ) [] = 0
⊢ m - n = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [← length, h, List.length]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)
have h : range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
Tactic: convert! range'_append using 2
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
h : range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)
have h₁ : l - n = m - n + (l - m)
Tactic: convert! range'_append using 2
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
have h : range' m (l - m) = range' (n + (m - n)) (l - m)
Tactic: rw [Nat.one_mul, Nat.add_sub_cancel' hnm]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
h : range' m (l - m) = range' (n + (m - n)) (l - m)
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
have h₁ : range' m (l - m) = range' m (l - m)
Tactic: rw [Nat.one_mul, Nat.add_sub_cancel' hnm]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []
have apply : ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l
Tactic: apply eq_nil_iff_forall_not_mem.2
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
have simp : n ≤ a → a < m → m ≤ a → l ≤ a
Tactic: simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l a : ℕ
h : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]
have hml : m ≤ m + 1
Tactic: rwa [← succ_singleton, append_consecutive]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m
have rw : [n] ++ Ico n.succ m = n :: Ico (n + 1) m
Tactic: rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
have pos : ∀ (h : n < m), IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
Tactic: by_cases! h : n < m
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
pos : ∀ (h : n < m), IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
have neg : ∀ (h : m ≤ n), IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
Tactic: by_cases! h : n < m
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : n < m
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
have pos : IsChain (fun (a b : ℕ) ↦ b = a.succ) (n :: Ico (n + 1) m)
Tactic: rw [eq_cons h]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m : ℕ
h : m ≤ n
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
have neg : IsChain (fun (a b : ℕ) ↦ b = a.succ) []
Tactic: rw [eq_nil_of_le h]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true
have simp : l ≤ k
Tactic: simp only [decide_eq_true_eq, not_lt]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
have apply : n ≤ k
Tactic: apply le_trans hln
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inl : ∀ (hnl : n ≤ l), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
Tactic: rcases le_total n l with hnl | hln
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
inl : ∀ (hnl : n ≤ l), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inr : ∀ (hln : l ≤ n), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
Tactic: rcases le_total n l with hnl | hln
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l ++ Ico l m) = Ico n l
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l ++ Ico l m) = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inl₁ : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l ++ Ico l m) = Ico n l
inl₁ : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inl₂ : Ico n l ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l ++ Ico l m) = Ico n l
inl₁ : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
inl₂ : Ico n l ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inl₃ : Ico n l ++ [] = Ico n l
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l ++ Ico l m) = Ico n l
inl₁ : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
inl₂ : Ico n l ++ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico l m) = Ico n l
inl₃ : Ico n l ++ [] = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inl₄ : Ico n l = Ico n l
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inr : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = []
Tactic: rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
inr : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = []
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
have inr₁ : Eq (α := List ℕ) [] []
Tactic: rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
have inl : ∀ (hml : m ≤ l), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
Tactic: rcases le_total m l with hml | hlm
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
inl : ∀ (hml : m ≤ l), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
have inr : ∀ (hlm : l ≤ m), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
Tactic: rcases le_total m l with hml | hlm
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hml : m ≤ l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
have inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n m
Tactic: rw [min_eq_left hml, filter_lt_of_top_le hml]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hml : m ≤ l
inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n m
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
have inl₁ : Ico n m = Ico n m
Tactic: rw [min_eq_left hml, filter_lt_of_top_le hml]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
have inr : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
Tactic: rw [min_eq_right hlm, filter_lt_of_ge hlm]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hlm : l ≤ m
inr : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
have inr₁ : Ico n l = Ico n l
Tactic: rw [min_eq_right hlm, filter_lt_of_ge hlm]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true
have rw : l ≤ k
Tactic: rw [decide_eq_true_eq]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true
have rw : ¬l ≤ k
Tactic: rw [decide_eq_true_eq]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inl : ∀ (hlm : l ≤ m), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
Tactic: rcases le_total l m with hlm | hml
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
inl : ∀ (hlm : l ≤ m), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inr : ∀ (hml : m ≤ l), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
Tactic: rcases le_total l m with hlm | hml
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l ++ Ico l m) = Ico l m
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l ++ Ico l m) = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inl₁ : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l ++ Ico l m) = Ico l m
inl₁ : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inl₂ : [] ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l ++ Ico l m) = Ico l m
inl₁ : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
inl₂ : [] ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inl₃ : [] ++ Ico l m = Ico l m
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l ++ Ico l m) = Ico l m
inl₁ : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n l) ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
inl₂ : [] ++ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico l m) = Ico l m
inl₃ : [] ++ Ico l m = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inl₄ : Ico l m = Ico l m
Tactic: rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inr : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = []
Tactic: rw [eq_nil_of_le hml, filter_le_of_top_le hml]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
inr : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = []
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
have inr₁ : Eq (α := List ℕ) [] []
Tactic: rw [eq_nil_of_le hml, filter_le_of_top_le hml]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
have inl : ∀ (hnl : n ≤ l), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
Tactic: rcases le_total n l with hnl | hln
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
inl : ∀ (hnl : n ≤ l), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
have inr : ∀ (hln : l ≤ n), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
Tactic: rcases le_total n l with hnl | hln
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
have inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
Tactic: rw [max_eq_right hnl, filter_le_of_le hnl]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hnl : n ≤ l
inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
have inl₁ : Ico l m = Ico l m
Tactic: rw [max_eq_right hnl, filter_le_of_le hnl]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hln : l ≤ n
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
have inr : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico n m
Tactic: rw [max_eq_left hln, filter_le_of_le_bot hln]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (goal)
Goal:
n m l : ℕ
hln : l ≤ n
inr : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico n m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
have inr₁ : Ico n m = Ico n m
Tactic: rw [max_eq_left hln, filter_le_of_le_bot hln]
-- Lean 4 proof step from Mathlib.Data.List.Intervals (hypothesis)
Goal:
n m : ℕ
hnm : n < m
⊢ filter (fun (x : ℕ) ↦ decide (x < n + 1)) (Ico n m) = [n]
have r : min m (n + 1) = n + 1
Tactic: have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm