awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Intervals
Goal:
n : ℕ
⊢ Ico n n = []

Tactic:
eq_nil_of_le (le_refl n)

Premises used: le_refl, List.Ico.eq_nil_of_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : Ico n m = []
rw : (Ico n m).length = 0
rw₁ : List.length (α := ℕ) [] = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ m - n = 0

Tactic:
rw [← length, h, List.length]

Premises used: List.Ico.length, List.length
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' (n + 1 * (m - n)) (l - m) = range' n (m - n + (l - m))

Tactic:
range'_append

Premises used: List.range'_append
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
h : range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
h₁ : l - n = m - n + (l - m)
convert_3 : ℕ
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)

Tactic:
convert! range'_append using 2

Premises used: List.range'_append
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
h : range' m (l - m) = range' (n + (m - n)) (l - m)
h₁ h₂ : range' m (l - m) = range' m (l - m)
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)

Tactic:
rw [Nat.one_mul, Nat.add_sub_cancel' hnm]

Premises used: Nat.add_sub_cancel', Nat.one_mul
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)

Tactic:
lia
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
apply : ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l
⊢ Ico n m ∩ Ico m l = []

Tactic:
apply eq_nil_iff_forall_not_mem.2

Premises used: Iff.mpr, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l a : ℕ
simp : n ≤ a → a < m → m ≤ a → l ≤ a
⊢ ¬a ∈ Ico n m ∩ Ico m l

Tactic:
simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]

Premises used: and_imp, not_lt, List.mem_inter_iff, not_and, List.Ico.mem
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l a : ℕ
h : n ≤ a
h₂ : a < m
h₃ : m ≤ a
exfalso : False
⊢ l ≤ a

Tactic:
exfalso
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l a : ℕ
h : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False

Tactic:
not_lt_of_ge h₃ h₂

Premises used: not_lt_of_ge
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l a : ℕ
h : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False

Tactic:
exact not_lt_of_ge h₃ h₂

Premises used: not_lt_of_ge
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
inter_consecutive n m l

Premises used: List.Ico.inter_consecutive
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
convert! inter_consecutive n m l

Premises used: List.Ico.inter_consecutive
-- Module: Mathlib.Data.List.Intervals
Goal:
n : ℕ
⊢ range' n (n + 1 - n) = [n]

Tactic:
simp [Nat.add_sub_cancel_left]

Premises used: Nat.add_sub_cancel_left
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n ≤ m
hml : m ≤ m + 1
⊢ Ico n (m + 1) = Ico n m ++ [m]

Tactic:
rwa [← succ_singleton, append_consecutive]

Premises used: List.Ico.succ_singleton, List.Ico.append_consecutive
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1

Tactic:
Nat.le_succ _

Premises used: Nat.le_succ
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1

Tactic:
exact Nat.le_succ _

Premises used: Nat.le_succ
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n < m
rw : [n] ++ Ico n.succ m = n :: Ico (n + 1) m
⊢ Ico n m = n :: Ico (n + 1) m

Tactic:
rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]

Premises used: Nat.le_succ, List.Ico.succ_singleton, List.Ico.append_consecutive
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n < m
⊢ [n] ++ Ico n.succ m = n :: Ico (n + 1) m

Tactic:
rfl
-- Module: Mathlib.Data.List.Intervals
Goal:
m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]

Tactic:
simp [Ico, Nat.sub_sub_self (succ_le_of_lt h)]

Premises used: Nat.sub_sub_self, Nat.succ_le_of_lt, List.Ico
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
pos : ∀ (h : n < m), IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
neg : ∀ (h : m ≤ n), IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)

Tactic:
by_cases! h : n < m
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n < m
pos : IsChain (fun (a b : ℕ) ↦ b = a.succ) (n :: Ico (n + 1) m)
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)

Tactic:
rw [eq_cons h]

Premises used: List.Ico.eq_cons
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n < m
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (n :: range' (n + 1) (m - (n + 1)))

Tactic:
isChain_range' _ (_ + 1) 1

Premises used: List.range', List.isChain_range', HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : n < m
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (n :: range' (n + 1) (m - (n + 1)))

Tactic:
exact isChain_range' _ (_ + 1) 1

Premises used: List.isChain_range', HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : m ≤ n
neg : IsChain (fun (a b : ℕ) ↦ b = a.succ) []
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) (Ico n m)

Tactic:
rw [eq_nil_of_le h]

Premises used: List.Ico.eq_nil_of_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : m ≤ n
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) []

Tactic:
.nil

Premises used: List.IsChain.nil
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : m ≤ n
⊢ IsChain (fun (a b : ℕ) ↦ b = a.succ) []

Tactic:
exact .nil
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
⊢ ¬m ∈ Ico n m

Tactic:
simp
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ decide (k < l) = true

Tactic:
simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_true]

Premises used: decide_true, And.right, Iff.mp, List.Ico.mem, lt_of_lt_of_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
simp : l ≤ k
⊢ ¬decide (k < l) = true

Tactic:
simp only [decide_eq_true_eq, not_lt]

Premises used: not_lt, decide_eq_true_eq
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
apply : n ≤ k
⊢ l ≤ k

Tactic:
apply le_trans hln

Premises used: le_trans
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k

Tactic:
(mem.1 hk).1

Premises used: And.left, Iff.mp, List.Ico.mem
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k

Tactic:
exact (mem.1 hk).1

Premises used: And.left, Iff.mp, List.Ico.mem
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hlm : l ≤ m
inl : ∀ (hnl : n ≤ l), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
inr : ∀ (hln : l ≤ n), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
rcases le_total n l with hnl | hln

Premises used: le_total
-- Module: Mathlib.Data.List.Intervals
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
inl₄ inl₅ : Ico n l = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n 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]

Premises used: le_refl, List.Ico.filter_lt_of_top_le, List.Ico.filter_lt_of_le_bot, List.append_nil, List.filter_append, List.Ico.append_consecutive
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
inr : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = []
inr₁ inr₂ : Eq (α := List ℕ) [] []
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]

Premises used: List.Ico.eq_nil_of_le, List.Ico.filter_lt_of_le_bot
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
inl : ∀ (hml : m ≤ l), filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)
inr : ∀ (hlm : l ≤ m), 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)

Tactic:
rcases le_total m l with hml | hlm

Premises used: le_total
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hml : m ≤ l
inl : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n m
inl₁ inl₂ : Ico n m = Ico n m
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
rw [min_eq_left hml, filter_lt_of_top_le hml]

Premises used: List.Ico.filter_lt_of_top_le, min_eq_left
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hlm : l ≤ m
inr : filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n l
inr₁ inr₂ : Ico n l = Ico n l
⊢ filter (fun (x : ℕ) ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
rw [min_eq_right hlm, filter_lt_of_ge hlm]

Premises used: List.Ico.filter_lt_of_ge, min_eq_right
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
rw : l ≤ k
⊢ decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]

Premises used: decide_eq_true_eq
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Tactic:
le_trans hln (mem.1 hk).1

Premises used: And.left, Iff.mp, List.Ico.mem, le_trans
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Tactic:
exact le_trans hln (mem.1 hk).1

Premises used: And.left, Iff.mp, List.Ico.mem, le_trans
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
rw : ¬l ≤ k
⊢ ¬decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]

Premises used: decide_eq_true_eq
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k

Tactic:
not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

Premises used: And.right, Iff.mp, not_le_of_gt, List.Ico.mem, lt_of_lt_of_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k

Tactic:
exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

Premises used: And.right, Iff.mp, not_le_of_gt, List.Ico.mem, lt_of_lt_of_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnl : n ≤ l
inl : ∀ (hlm : l ≤ m), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
inr : ∀ (hml : m ≤ l), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rcases le_total l m with hlm | hml

Premises used: le_total
-- Module: Mathlib.Data.List.Intervals
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
inl₄ inl₅ : Ico l m = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n 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]

Premises used: le_refl, List.Ico.filter_le_of_le_bot, List.Ico.filter_le_of_top_le, List.filter_append, List.nil_append, List.Ico.append_consecutive
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
inr : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = []
inr₁ inr₂ : Eq (α := List ℕ) [] []
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rw [eq_nil_of_le hml, filter_le_of_top_le hml]

Premises used: List.Ico.eq_nil_of_le, List.Ico.filter_le_of_top_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
inl : ∀ (hnl : n ≤ l), filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m
inr : ∀ (hln : l ≤ n), 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

Tactic:
rcases le_total n l with hnl | hln

Premises used: le_total
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hnl : n ≤ l
inl : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico l m
inl₁ inl₂ : Ico l m = Ico l m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
rw [max_eq_right hnl, filter_le_of_le hnl]

Premises used: max_eq_right, List.Ico.filter_le_of_le
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
hln : l ≤ n
inr : filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico n m
inr₁ inr₂ : Ico n m = Ico n m
⊢ filter (fun (x : ℕ) ↦ decide (l ≤ x)) (Ico n m) = Ico (max n l) m

Tactic:
rw [max_eq_left hln, filter_le_of_le_bot hln]

Premises used: List.Ico.filter_le_of_le_bot, max_eq_left
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
hnm : n < m
⊢ min m (n + 1) = n + 1

Tactic:
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun (x : ℕ) ↦ decide (x < n + 1)) (Ico n m) = [n]

Tactic:
simp [filter_lt n m (n + 1), r]

Premises used: List.Ico.filter_lt, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
hnm : n < m
rw : filter (fun (x : ℕ) ↦ decide (x ≤ n)) (Ico n m) = filter (fun (x : ℕ) ↦ decide (x < n + 1)) (Ico n m)
⊢ filter (fun (x : ℕ) ↦ decide (x ≤ n)) (Ico n m) = [n]

Tactic:
rw [← filter_lt_of_succ_bot hnm]

Premises used: List.Ico.filter_lt_of_succ_bot
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
hnm : n < m
x : ℕ
h : x ∈ Ico n m
⊢ decide (x ≤ n) = decide (x < n + 1)

Tactic:
simpa using Nat.lt_succ_iff.symm

Premises used: Nat.lt_succ_iff, Iff.symm
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
hnm : n < m
⊢ filter (fun (x : ℕ) ↦ decide (x ≤ n)) (Ico n m) = filter (fun (x : ℕ) ↦ decide (x < n + 1)) (Ico n m)

Tactic:
exact filter_congr fun _ _ => by
    simpa using Nat.lt_succ_iff.symm

Premises used: List.filter_congr
-- Module: Mathlib.Data.List.Intervals
Goal:
n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Tactic:
grind [mem]

Premises used: List.Ico.mem
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
zero : ∀ (a : α), (iterate f a 0).length = 0
succ : ∀ (n : ℕ), (∀ (a : α), (iterate f a n).length = n) → ∀ (a : α), (iterate f a (n + 1)).length = n + 1
⊢ (iterate f a n).length = n

Tactic:
induction n generalizing a
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
⊢ (iterate f a 0).length = 0

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
n : ℕ
h : ∀ (a : α), (iterate f a n).length = n
a : α
⊢ (iterate f a (n + 1)).length = n + 1

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
rw : (iterate f a n).length = 0 ↔ n = 0
rw₁ rw₂ : n = 0 ↔ n = 0
⊢ iterate f a n = [] ↔ n = 0

Tactic:
rw [← length_eq_zero_iff, length_iterate]

Premises used: List.length_iterate, List.length_eq_zero_iff
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
h : 0 < n + 1
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (iterate f a (n + 1)) 0 = some (f^[0] a)

Tactic:
simp
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ i < n

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (iterate f a (n + 1)) (i + 1) = some (f^[i + 1] a)

Tactic:
simp [getElem?_iterate f (f a) n i (by simpa using h)]
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i < (iterate f a n).length
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : i < n), i < n
⊢ i < n

Tactic:
rwa [length_iterate] at h

Premises used: List.length_iterate
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
n : ℕ
b : α
⊢ b ∈ iterate f a n ↔ ∃ (m : ℕ), m < n ∧ b = f^[m] a

Tactic:
simp [List.mem_iff_get, Fin.exists_iff, eq_comm (b := b)]

Premises used: List.mem_iff_get, eq_comm, Fin.exists_iff
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
n : ℕ
f : α → α
a : α
hl : length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = (iterate f a n).length
h :
  ∀ (i : ℕ) (h₁ : i < length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n))) (h₂ : i < (iterate f a n).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (iterate f a n) i h₂
⊢ map (fun (x : ℕ) ↦ f^[x] a) (range n) = iterate f a n

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = (iterate f a n).length

Tactic:
simp
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ ∀ (i : ℕ) (h₁ : i < length.{u_1} (α := α) (map (fun (x : ℕ) ↦ f^[x] a) (range n))) (h₂ : i < (iterate f a n).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (map (fun (x : ℕ) ↦ f^[x] a) (range n)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (iterate f a n) i h₂

Tactic:
simp
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
n : ℕ
a : α
⊢ iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n

Tactic:
simp
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
n_1 n : ℕ
ih : ∀ (a : α), iterate f a (n + n_1) = iterate f a n ++ iterate f (f^[n] a) n_1
a : α
succ : iterate f a (n + 1 + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₁ : iterate f a (n + n_1 + 1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₂ : a :: iterate f (f a) (n + n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₃ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n_1
succ₄ : a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1
succ₅ succ₆ :
  a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1) = a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n_1)
⊢ iterate f a (n + 1 + n_1) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n_1

Tactic:
rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

Premises used: List.iterate, add_right_comm, Nat.iterate, List.cons_append
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
zero : ∀ (a : α), iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n
succ :
  ∀ (n_1 : ℕ) (ih : ∀ (a : α), iterate f a (n_1 + n) = iterate f a n_1 ++ iterate f (f^[n_1] a) n) (a : α),
    iterate f a (n_1 + 1 + n) = iterate f a (n_1 + 1) ++ iterate f (f^[n_1 + 1] a) n
⊢ iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

Tactic:
induction m generalizing a with
  | zero => simp
  | succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

Premises used: List.iterate, add_right_comm, Nat.iterate, List.cons_append
-- Module: Mathlib.Data.List.Iterate
Goal:
α : Type u_1
f : α → α
a : α
m n : ℕ
rw : take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)) = iterate f a (min m n)
rw₁ :
  Eq.{u_1 + 1} (α := List α) (take m (map (fun (x : ℕ) ↦ f^[x] a) (range n)))
    (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
rw₂ :
  Eq.{u_1 + 1} (α := List α) (map (fun (x : ℕ) ↦ f^[x] a) (take m (range n)))
    (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
rw₃ rw₄ :
  Eq.{u_1 + 1} (α := List α) (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
    (map (fun (x : ℕ) ↦ f^[x] a) (range (min m n)))
⊢ take m (iterate f a n) = iterate f a (min m n)

Tactic:
rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]

Premises used: List.take_range, List.range_map_iterate, List.map_take
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
d : l₁.Disjoint l₂
⊢ l₂.Disjoint l₁

Tactic:
fun _ i₂ i₁ => d i₁ i₂

Premises used: List.Disjoint
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
a : α
inst : DecidableEq α
h : a ∈ l₁
l₂ : List α
⊢ a ∈ l₁ ∪ l₂

Tactic:
mem_union_iff.2 (Or.inl h)

Premises used: Iff.mpr, List.mem_union_iff, Or.inl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ a ∈ l₁ ∪ l₂

Tactic:
mem_union_iff.2 (Or.inr h)

Premises used: Iff.mpr, List.mem_union_iff, Or.inr
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ Sublist.{u_1} (α := α) [] []

Tactic:
rfl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ l₁ ∪ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
simp only [e, cons_union, insert_of_mem h]

Premises used: List.insert_of_mem, List.cons_union
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ l₁ ∪ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
simp only [cons_append, cons_union, e, insert_of_not_mem h]

Premises used: List.cons_union, List.cons_append, List.insert_of_not_mem
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <:+ l₁ ∪ l₂

Tactic:
(sublist_suffix_of_union l₁ l₂).imp fun _ => And.right

Premises used: Exists.imp, And.right, List.IsSuffix, List.sublist_suffix_of_union
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ l₁ ∪ l₂ <+ l₁ ++ l₂

Tactic:
let ⟨_, s, e⟩ := sublist_suffix_of_union l₁ l₂
  e ▸ (append_sublist_append_right _).2 s

Premises used: Iff.mpr, Eq.rec, List.append_sublist_append_right, List.Sublist, Union.union, _private.0.List.union_sublist_append.match_1, HAppend.hAppend, List.sublist_suffix_of_union
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst : DecidableEq α
⊢ (∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
simp only [mem_union_iff, or_imp, forall_and]

Premises used: List.mem_union_iff, or_imp, forall_and
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst : DecidableEq α
h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x
⊢ ∀ (x : α), x ∈ l₁ → p x

Tactic:
(forall_mem_union.1 h).1

Premises used: List.forall_mem_union, And.left, Iff.mp
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst : DecidableEq α
h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x
⊢ ∀ (x : α), x ∈ l₂ → p x

Tactic:
(forall_mem_union.1 h).2

Premises used: List.forall_mem_union, And.right, Iff.mp
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
h : [] ⊆ ys
⊢ [] ∪ ys = ys

Tactic:
simp
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
ys : List α
x : α
xs : List α
ih : ∀ (h : xs ⊆ ys), xs ∪ ys = ys
h : x :: xs ⊆ ys
cons : List.insert x (xs ∪ ys) = ys
cons₁ : xs ∪ ys = ys
cons₂ cons₃ : ys = ys
⊢ x :: xs ∪ ys = ys

Tactic:
rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]

Premises used: List.mem_union_right, List.insert_of_mem, List.cons_union, List.mem_cons_self, List.subset_of_cons_subset
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
nil : ∀ (h : [] ⊆ ys), [] ∪ ys = ys
cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : xs ⊆ ys), xs ∪ ys = ys) (h : x :: xs ⊆ ys), x :: xs ∪ ys = ys
⊢ xs ∪ ys = ys

Tactic:
induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]

Premises used: List.mem_union_right, List.insert_of_mem, List.cons_union, List.cons, List.subset_of_cons_subset, List.nil
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ [] ∩ l = []

Tactic:
rfl

Premises used: List.filter, rfl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Tactic:
simp [Inter.inter, List.inter, h]

Premises used: Inter.inter, List.inter