[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
n : ℕ
l : List α
⊢ countp.go p l n = n + countp.go p l 0
[PROOFSTEP]
induction' l with head tail ih generalizing n
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
n✝ n : ℕ
⊢ countp.go p [] n = n + countp.go p [] 0
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0
[PROOFSTEP]
unfold countp.go
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then countp.go p tail (n + 1) else countp.go p tail n) =
    n + bif p head then countp.go p tail (0 + 1) else countp.go p tail 0
[PROOFSTEP]
rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
[PROOFSTEP]
by_cases h : p head
[GOAL]
case pos
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
[PROOFSTEP]
simp [h, add_assoc]
[GOAL]
case neg
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : ¬p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp p (a :: l) = countp p l + 1
[PROOFSTEP]
have : countp.go p (a :: l) 0 = countp.go p l 1
[GOAL]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp.go p (a :: l) 0 = countp.go p l 1
[PROOFSTEP]
change (bif _ then _ else _) = countp.go _ _ _
[GOAL]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
[PROOFSTEP]
rw [pa]
[GOAL]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif true then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp p (a :: l) = countp p l + 1
[PROOFSTEP]
unfold countp
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp.go p (a :: l) 0 = countp.go p l 0 + 1
[PROOFSTEP]
rw [this, add_comm, List.countp_go_eq_add]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ countp p (a :: l) = countp p l
[PROOFSTEP]
change (bif _ then _ else _) = countp.go _ _ _
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
[PROOFSTEP]
rw [Bool.of_not_eq_true pa]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif false then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
⊢ countp p (a :: l) = countp p l + if p a = true then 1 else 0
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
h : p a = true
⊢ countp p (a :: l) = countp p l + if p a = true then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
h : ¬p a = true
⊢ countp p (a :: l) = countp p l + if p a = true then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ length l = countp p l + countp (fun a => decide ¬p a = true) l
[PROOFSTEP]
induction' l with x h ih
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
⊢ length [] = countp p [] + countp (fun a => decide ¬p a = true) []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l : List α
p q : α → Bool
x : α
h : List α
ih : length h = countp p h + countp (fun a => decide ¬p a = true) h
⊢ length (x :: h) = countp p (x :: h) + countp (fun a => decide ¬p a = true) (x :: h)
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
[PROOFSTEP]
rw [countp_cons_of_pos _ _ h, countp_cons_of_neg _ _ _, length, ih]
[GOAL]
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ ¬(decide ¬p x = true) = true
[PROOFSTEP]
simp only [h]
[GOAL]
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
[PROOFSTEP]
rw [countp_cons_of_pos (fun a => ¬p a) _ _, countp_cons_of_neg _ _ h, length, ih]
[GOAL]
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 =
    countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (fun a => decide ¬p a = true) x = true
[PROOFSTEP]
simp only [h]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ countp p l = length (filter p l)
[PROOFSTEP]
induction' l with x l ih
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p [] = length (filter p [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l✝ : List α
p q : α → Bool
x : α
l : List α
ih : countp p l = length (filter p l)
⊢ countp p (x :: l) = length (filter p (x :: l))
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
x : α
l : List α
ih : countp p l = length (filter p l)
h : p x = true
⊢ countp p (x :: l) = length (filter p (x :: l))
[PROOFSTEP]
rw [countp_cons_of_pos p l h, ih, filter_cons_of_pos l h, length]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
x : α
l : List α
ih : countp p l = length (filter p l)
h : ¬p x = true
⊢ countp p (x :: l) = length (filter p (x :: l))
[PROOFSTEP]
rw [countp_cons_of_neg p l h, ih, filter_cons_of_neg l h]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l ≤ length l
[PROOFSTEP]
simpa only [countp_eq_length_filter] using length_filter_le _ _
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
l₁ l₂ : List α
⊢ countp p (l₁ ++ l₂) = countp p l₁ + countp p l₂
[PROOFSTEP]
simp only [countp_eq_length_filter, filter_append, length_append]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
a : List α
l : List (List α)
⊢ countp p (join (a :: l)) = sum (map (countp p) (a :: l))
[PROOFSTEP]
rw [join, countp_append, map_cons, sum_cons, countp_join l]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ 0 < countp p l ↔ ∃ a, a ∈ l ∧ p a = true
[PROOFSTEP]
simp only [countp_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← pos_iff_ne_zero, countp_pos]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ (∃ a, a ∈ l ∧ p a = true) ↔ ¬∀ (a : α), a ∈ l → ¬p a = true
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp p l = length l ↔ ∀ (a : α), a ∈ l → p a = true
[PROOFSTEP]
rw [countp_eq_length_filter, filter_length_eq_length]
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ length (filter p l) < length l ↔ ∃ x, x ∈ l ∧ ¬p x = true
[PROOFSTEP]
simpa [length_eq_countp_add_countp p l, countp_eq_length_filter] using countp_pos (fun x => ¬p x) (l := l)
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ countp p l₁ ≤ countp p l₂
[PROOFSTEP]
simpa only [countp_eq_length_filter] using length_le_of_sublist (s.filter p)
[GOAL]
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ countp p (filter q l) = countp (fun a => decide (p a = true ∧ q a = true)) l
[PROOFSTEP]
simp only [countp_eq_length_filter, filter_filter]
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp (fun x => true) l = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
⊢ countp (fun x => false) l = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ countp p (map f (a :: l)) = countp (p ∘ f) (a :: l)
[PROOFSTEP]
rw [map_cons, countp_cons, countp_cons, countp_map p f l]
[GOAL]
α : Type u_2
l✝ : List α
p✝ q : α → Bool
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ (countp (p ∘ f) l + if p (f a) = true then 1 else 0) = countp (p ∘ f) l + if (p ∘ f) a = true then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p l ≤ countp q l
[PROOFSTEP]
induction' l with a l ihl
[GOAL]
case nil
α : Type u_1
l : List α
p q : α → Bool
h✝ : ∀ (x : α), x ∈ l → p x = true → q x = true
h : ∀ (x : α), x ∈ [] → p x = true → q x = true
⊢ countp p [] ≤ countp q []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l✝ : List α
p q : α → Bool
h✝ : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
h : ∀ (x : α), x ∈ a :: l → p x = true → q x = true
⊢ countp p (a :: l) ≤ countp q (a :: l)
[PROOFSTEP]
rw [forall_mem_cons] at h
[GOAL]
case cons
α : Type u_1
l✝ : List α
p q : α → Bool
h✝ : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
h : (p a = true → q a = true) ∧ ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p (a :: l) ≤ countp q (a :: l)
[PROOFSTEP]
cases' h with ha hl
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countp p (a :: l) ≤ countp q (a :: l)
[PROOFSTEP]
rw [countp_cons, countp_cons]
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ (countp p l + if p a = true then 1 else 0) ≤ countp q l + if q a = true then 1 else 0
[PROOFSTEP]
refine' _root_.add_le_add (ihl hl) _
[GOAL]
case cons.intro
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ (if p a = true then 1 else 0) ≤ if q a = true then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : p a = true
h✝ : q a = true
⊢ 1 ≤ 1
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : p a = true
h✝ : ¬q a = true
⊢ 1 ≤ 0
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case pos
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : ¬p a = true
h✝ : q a = true
⊢ 0 ≤ 1
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : ¬p a = true
h✝ : ¬q a = true
⊢ 0 ≤ 0
[PROOFSTEP]
simp only [le_rfl, _root_.zero_le]
[GOAL]
case neg
α : Type u_1
l✝ : List α
p q : α → Bool
h : ∀ (x : α), x ∈ l✝ → p x = true → q x = true
a : α
l : List α
ihl : (∀ (x : α), x ∈ l → p x = true → q x = true) → countp p l ≤ countp q l
ha : p a = true → q a = true
hl : ∀ (x : α), x ∈ l → p x = true → q x = true
h✝¹ : p a = true
h✝ : ¬q a = true
⊢ False
[PROOFSTEP]
exact absurd (ha ‹_›) ‹_›
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
conv =>
  simp [count, countp_cons]
  lhs
  simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
  simp [count, countp_cons]
  lhs
  simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
  simp [count, countp_cons]
  lhs
  simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| count a (b :: l) = count a l + if a = b then 1 else 0
[PROOFSTEP]
simp [count, countp_cons]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| (if b = a then 1 else 0) = if a = b then 1 else 0
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
| if b = a then 1 else 0
[PROOFSTEP]
simp only [eq_comm]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ count a (b :: l) = if a = b then succ (count a l) else count a l
[PROOFSTEP]
simp [count_cons']
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (count a l + if a = b then 1 else 0) = if a = b then succ (count a l) else count a l
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h✝ : a = b
⊢ count a l + 1 = succ (count a l)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h✝ : ¬a = b
⊢ count a l + 0 = count a l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (a :: l) = count a l + 1
[PROOFSTEP]
simp [count_cons']
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ count a (b :: l) = count a l
[PROOFSTEP]
simp [count_cons']
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
l : List α
⊢ a = b → False
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    count a (head :: tail) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
[PROOFSTEP]
rw [count_cons']
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
⊢ count a (List.tail (head :: tail)) =
    (count a tail + if a = head then 1 else 0) - if a = get (head :: tail) { val := 0, isLt := h } then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : a = head
h✝ : a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 1 - 1
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : a = head
h✝ : ¬a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 1 - 0
[PROOFSTEP]
simp at *
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : ¬a = head
h✝ : a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 0 - 1
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : ¬a = head
h✝ : ¬a = get (head :: tail) { val := 0, isLt := h }
⊢ count a (List.tail (head :: tail)) = count a tail + 0 - 0
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : a = head
h✝ : ¬a = head
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
head : α
tail : List α
a : α
h : 0 < length (head :: tail)
h✝¹ : ¬a = head
h✝ : a = head
⊢ count a tail = count a tail - 1
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ count a [a] = 1
[PROOFSTEP]
rw [count_cons]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ (if a = a then succ (count a []) else count a []) = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ count a [b] = if a = b then 1 else 0
[PROOFSTEP]
rw [count_cons]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ (if a = b then succ (count a []) else count a []) = if a = b then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (concat l a) = succ (count a l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ 0 < count a l ↔ a ∈ l
[PROOFSTEP]
simp only [count, countp_pos, beq_iff_eq, exists_eq_right]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ count a l = length l ↔ ∀ (b : α), b ∈ l → a = b
[PROOFSTEP]
simp_rw [count, countp_eq_length, beq_iff_eq, eq_comm]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if a = b then n else 0
[PROOFSTEP]
split
[GOAL]
case inl
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
h✝ : a = b
⊢ count a (replicate n b) = n
case inr α : Type u_1 l : List α inst✝ : DecidableEq α a b : α n : ℕ h✝ : ¬a = b ⊢ count a (replicate n b) = 0
[PROOFSTEP]
exacts [‹a = b› ▸ count_replicate_self _ _, count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ filter (fun x => x == a) l = replicate (count a l) a
[PROOFSTEP]
simp only [count, countp_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a
[PROOFSTEP]
exact ⟨trivial, fun _ h => h.2⟩
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
l : List α
a : α
⊢ filter (fun x => decide (a = x)) l = replicate (count a l) a
[PROOFSTEP]
simpa only [eq_comm] using filter_eq' l a
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
n : ℕ
a : α
h : replicate n a <+ l
⊢ n ≤ count a l
[PROOFSTEP]
simpa only [count_replicate_self] using h.count_le a
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ count a (filter p l) = count a l
[PROOFSTEP]
rw [count, countp_filter]
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ countp (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) l = countp (fun x => x == a) l
[PROOFSTEP]
congr
[GOAL]
case e_p
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
⊢ (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) = fun x => x == a
[PROOFSTEP]
funext b
[GOAL]
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide ((b == a) = true ∧ p b = true) = (b == a)
[PROOFSTEP]
rw [Bool.beq_eq_decide_eq]
[GOAL]
case e_p.h
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
[PROOFSTEP]
by_cases hb : b = a
[GOAL]
case pos
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
[PROOFSTEP]
simp [hb, h]
[GOAL]
case neg
α : Type u_1
l : List α
inst✝ : DecidableEq α
p : α → Bool
a : α
h : p a = true
b : α
hb : ¬b = a
⊢ decide (decide (b = a) = true ∧ p b = true) = decide (b = a)
[PROOFSTEP]
simp [hb]
[GOAL]
α✝ : Type ?u.43925
l✝ : List α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → List β
x : β
⊢ count x (List.bind l f) = sum (map (count x ∘ f) l)
[PROOFSTEP]
rw [List.bind, count_join, map_map]
[GOAL]
α✝ : Type ?u.44336
l✝ : List α✝
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ count (f x) (map f l) = count x l
[PROOFSTEP]
simp only [count, countp_map, (· ∘ ·), hf.beq_eq]
[GOAL]
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ count x l ≤ count (f x) (map f l)
[PROOFSTEP]
rw [count, count, countp_map]
[GOAL]
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ countp (fun x_1 => x_1 == x) l ≤ countp ((fun x_1 => x_1 == f x) ∘ f) l
[PROOFSTEP]
exact countp_mono_left <| by simp (config := { contextual := true })
[GOAL]
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ ∀ (x_1 : α), x_1 ∈ l → (x_1 == x) = true → ((fun x_2 => x_2 == f x) ∘ f) x_1 = true
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ count a (List.erase [] b) = count a [] - if a = b then 1 else 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (List.erase (c :: l) b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
rw [erase_cons]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
by_cases hc : c = b
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_pos hc, hc, count_cons', Nat.add_sub_cancel]
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_neg hc, count_cons', count_cons', count_erase a b l]
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
by_cases ha : a = b
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
rw [← ha, eq_comm] at hc
[GOAL]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬a = c
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_pos ha, if_neg hc, add_zero, add_zero]
[GOAL]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : ¬a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
[PROOFSTEP]
rw [if_neg ha, tsub_zero, tsub_zero]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a (List.erase l a) = count a l - 1
[PROOFSTEP]
rw [count_erase, if_pos rfl]
[GOAL]
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
l : List α
⊢ count a (List.erase l b) = count a l
[PROOFSTEP]
rw [count_erase, if_neg ab, tsub_zero]
[GOAL]
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a : α
f : α → β
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ prod (map f l) = f a ^ count a l
[PROOFSTEP]
induction' l with a' as h generalizing a
[GOAL]
case nil
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ prod (map f []) = f a ^ count a []
[PROOFSTEP]
rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
[GOAL]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → prod (map f as) = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
[PROOFSTEP]
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
[GOAL]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ prod (map f (a' :: as)) = f a ^ count a (a' :: as)
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, count_cons, h]
[GOAL]
case cons
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ if a = a' then succ (count a as) else count a as
[PROOFSTEP]
split_ifs with ha'
[GOAL]
case pos
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : a = a'
⊢ f a' * f a ^ count a as = f a ^ succ (count a as)
[PROOFSTEP]
rw [ha', _root_.pow_succ]
[GOAL]
case neg
α : Type u_2
l : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : Monoid β
a✝ : α
f : α → β
hf✝ : ∀ (a' : α), a' ≠ a✝ → a' ∈ l → f a' = 1
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : prod (map f as) = f a ^ count a as
ha' : ¬a = a'
⊢ f a' * f a ^ count a as = f a ^ count a as
[PROOFSTEP]
rw [hf a' (Ne.symm ha') (List.mem_cons_self a' as), one_mul]
[GOAL]
α : Type u_1
l : List α
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 1
⊢ prod l = prod (map id l)
[PROOFSTEP]
rw [map_id]


[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l (n % length l) = rotate l n
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
n : ℕ
⊢ rotate [] n = []
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
l : List α
⊢ rotate l 0 = l
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
n : ℕ
⊢ rotate' [] n = []
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u
⊢ rotate' [] zero = []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
n✝ : ℕ
⊢ rotate' [] (succ n✝) = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l : List α
⊢ rotate' l 0 = l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
⊢ rotate' [] 0 = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ rotate' (head✝ :: tail✝) 0 = head✝ :: tail✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l : List α
a : α
n : ℕ
⊢ rotate' (a :: l) (succ n) = rotate' (l ++ [a]) n
[PROOFSTEP]
simp [rotate']
[GOAL]
α : Type u
x✝ : ℕ
⊢ length (rotate' [] x✝) = length []
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
⊢ length (rotate' (a :: l) (n + 1)) = length (a :: l)
[PROOFSTEP]
rw [List.rotate', length_rotate' (l ++ [a]) n]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
⊢ length (l ++ [a]) = length (a :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
h : n ≤ length []
⊢ rotate' [] n = drop n [] ++ take n []
[PROOFSTEP]
simp [drop_append_of_le_length h]
[GOAL]
α : Type u
l : List α
h : 0 ≤ length l
⊢ rotate' l 0 = drop 0 l ++ take 0 l
[PROOFSTEP]
simp [take_append_of_le_length h]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
[PROOFSTEP]
have hnl : n ≤ l.length := le_of_succ_le_succ h
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
[PROOFSTEP]
have hnl' : n ≤ (l ++ [a]).length := by rw [length_append, length_cons, List.length]; exact le_of_succ_le h
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length (l ++ [a])
[PROOFSTEP]
rw [length_append, length_cons, List.length]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length l + succ 0
[PROOFSTEP]
exact le_of_succ_le h
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
[PROOFSTEP]
rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take, drop_append_of_le_length hnl,
  take_append_of_le_length hnl]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
m : ℕ
⊢ rotate' (rotate' (a :: l) 0) m = rotate' (a :: l) (0 + m)
[PROOFSTEP]
simp
[GOAL]
α : Type u
n m : ℕ
⊢ rotate' (rotate' [] n) m = rotate' [] (n + m)
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
n m : ℕ
⊢ rotate' (rotate' (a :: l) (n + 1)) m = rotate' (a :: l) (n + 1 + m)
[PROOFSTEP]
rw [rotate'_cons_succ, rotate'_rotate' _ n, add_right_comm, ← rotate'_cons_succ]
[GOAL]
α : Type u
l : List α
⊢ rotate' l (length l) = l
[PROOFSTEP]
rw [rotate'_eq_drop_append_take le_rfl]
[GOAL]
α : Type u
l : List α
⊢ drop (length l) l ++ take (length l) l = l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
⊢ rotate' l (length l * 0) = l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' l (length l * (n + 1)) = rotate' (rotate' l (length l * n)) (length (rotate' l (length l * n)))
[PROOFSTEP]
simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' (rotate' l (length l * n)) (length (rotate' l (length l * n))) = l
[PROOFSTEP]
rw [rotate'_length, rotate'_length_mul l n]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' l (n % length l) = rotate' (rotate' l (n % length l)) (length (rotate' l (n % length l)) * (n / length l))
[PROOFSTEP]
rw [rotate'_length_mul]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' (rotate' l (n % length l)) (length (rotate' l (n % length l)) * (n / length l)) = rotate' l n
[PROOFSTEP]
rw [rotate'_rotate', length_rotate', Nat.mod_add_div]
[GOAL]
α : Type u
l : List α
n : ℕ
h : length l = 0
⊢ rotate l n = rotate' l n
[PROOFSTEP]
simp_all [length_eq_zero]
[GOAL]
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = rotate' l n
[PROOFSTEP]
rw [← rotate'_mod, rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
[GOAL]
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
l : List α
a : α
n : ℕ
⊢ rotate (a :: l) (succ n) = rotate (l ++ [a]) n
[PROOFSTEP]
rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]
[GOAL]
α : Type u
x✝ : α
n : ℕ
⊢ x✝ ∈ rotate [] n ↔ x✝ ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
x✝ : α
⊢ x✝ ∈ rotate (a :: l) 0 ↔ x✝ ∈ a :: l
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
x✝ : α
n : ℕ
⊢ x✝ ∈ rotate (a :: l) (n + 1) ↔ x✝ ∈ a :: l
[PROOFSTEP]
simp [rotate_cons_succ, mem_rotate, or_comm]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ length (rotate l n) = length l
[PROOFSTEP]
rw [rotate_eq_rotate', length_rotate']
[GOAL]
α : Type u
a : α
n k : ℕ
⊢ length (rotate (replicate n a) k) = n
[PROOFSTEP]
rw [length_rotate, length_replicate]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate l n = drop n l ++ take n l
[PROOFSTEP]
rw [rotate_eq_rotate']
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate' l n = drop n l ++ take n l
[PROOFSTEP]
exact rotate'_eq_drop_append_take
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
cases' l.length.zero_le.eq_or_lt with hl hl
[GOAL]
case inl
α : Type u
l : List α
n : ℕ
hl : 0 = length l
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
simp [eq_nil_of_length_eq_zero hl.symm]
[GOAL]
case inr
α : Type u
l : List α
n : ℕ
hl : 0 < length l
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]
[GOAL]
α : Type u
l l' : List α
⊢ rotate (l ++ l') (length l) = l' ++ l
[PROOFSTEP]
rw [rotate_eq_rotate']
[GOAL]
α : Type u
l l' : List α
⊢ rotate' (l ++ l') (length l) = l' ++ l
[PROOFSTEP]
induction l generalizing l'
[GOAL]
case nil
α : Type u
l' : List α
⊢ rotate' ([] ++ l') (length []) = l' ++ []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), rotate' (tail✝ ++ l') (length tail✝) = l' ++ tail✝
l' : List α
⊢ rotate' (head✝ :: tail✝ ++ l') (length (head✝ :: tail✝)) = l' ++ head✝ :: tail✝
[PROOFSTEP]
simp_all [rotate']
[GOAL]
α : Type u
l : List α
n m : ℕ
⊢ rotate (rotate l n) m = rotate l (n + m)
[PROOFSTEP]
rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']
[GOAL]
α : Type u
l : List α
⊢ rotate l (length l) = l
[PROOFSTEP]
rw [rotate_eq_rotate', rotate'_length]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l (length l * n) = l
[PROOFSTEP]
rw [rotate_eq_rotate', rotate'_length_mul]
[GOAL]
α : Type u
inst✝ : Group α
x✝¹ : prod [] = 1
x✝ : ℕ
⊢ prod (rotate [] x✝) = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
⊢ prod (rotate (a :: l) n) = 1
[PROOFSTEP]
have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
⊢ length (a :: l) > 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
[PROOFSTEP]
rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
n : ℕ
hl : prod (take (n % length (a :: l)) (a :: l) ++ drop (n % length (a :: l)) (a :: l)) = 1
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
[PROOFSTEP]
rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ← one_mul (List.prod _)⁻¹, ←
  hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~ l
[PROOFSTEP]
rw [rotate_eq_rotate']
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' l n ~ l
[PROOFSTEP]
induction' n with n hn generalizing l
[GOAL]
case zero
α : Type u
l✝ l : List α
⊢ rotate' l zero ~ l
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
l : List α
⊢ rotate' l (succ n) ~ l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
⊢ rotate' [] (succ n) ~ []
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
hd : α
tl : List α
⊢ rotate' (hd :: tl) (succ n) ~ hd :: tl
[PROOFSTEP]
rw [rotate'_cons_succ]
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
hd : α
tl : List α
⊢ rotate' (tl ++ [hd]) n ~ hd :: tl
[PROOFSTEP]
exact (hn _).trans (perm_append_singleton _ _)
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l n = [] ↔ l = []
[PROOFSTEP]
induction' n with n hn generalizing l
[GOAL]
case zero
α : Type u
l✝ l : List α
⊢ rotate l zero = [] ↔ l = []
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ {l : List α}, rotate l n = [] ↔ l = []
l : List α
⊢ rotate l (succ n) = [] ↔ l = []
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ {l : List α}, rotate l n = [] ↔ l = []
⊢ rotate [] (succ n) = [] ↔ [] = []
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ {l : List α}, rotate l n = [] ↔ l = []
hd : α
tl : List α
⊢ rotate (hd :: tl) (succ n) = [] ↔ hd :: tl = []
[PROOFSTEP]
simp [rotate_cons_succ, hn]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ [] = rotate l n ↔ [] = l
[PROOFSTEP]
rw [eq_comm, rotate_eq_nil_iff, eq_comm]
[GOAL]
α✝ : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : length l = length l'
⊢ rotate (zipWith f l l') n = zipWith f (rotate l n) (rotate l' n)
[PROOFSTEP]
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod, h, zipWith_append, ←
  zipWith_distrib_drop, ← zipWith_distrib_take, List.length_zipWith, h, min_self]
[GOAL]
case h
α✝ : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : length l = length l'
⊢ length (drop (n % length l') l) = length (drop (n % length l') l')
[PROOFSTEP]
rw [length_drop, length_drop, h]
[GOAL]
α : Type u
β : Type u_1
f : α → α → β
x y : α
l : List α
⊢ zipWith f (x :: y :: l) (rotate (x :: y :: l) 1) = f x y :: zipWith f (y :: l) (l ++ [x])
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (rotate l n) m = get? l ((m + n) % length l)
[PROOFSTEP]
rw [rotate_eq_drop_append_take_mod]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
rcases lt_or_le m (l.drop (n % l.length)).length with hm | hm
[GOAL]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
rw [get?_append hm, get?_drop, add_comm m, ← mod_add_mod]
[GOAL]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
[PROOFSTEP]
rw [length_drop, lt_tsub_iff_left] at hm
[GOAL]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm✝ : m < length l - n % length l
hm : n % length l + m < length l
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
[PROOFSTEP]
rw [mod_eq_of_lt hm]
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
rw [get?_append_right hm, get?_take, length_drop]
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? l (m - (length l - n % length l)) = get? l ((m + n) % length l)
[PROOFSTEP]
congr 1
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
rw [length_drop] at hm
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
have hm' := tsub_le_iff_left.1 hm
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
have : n % length l + m - length l < length l
[GOAL]
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m - length l < length l
[PROOFSTEP]
rw [tsub_lt_iff_left hm']
[GOAL]
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m < length l + length l
[PROOFSTEP]
exact Nat.add_lt_add hlt hml
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
conv_rhs => rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
| (m + n) % length l
[PROOFSTEP]
rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
| (m + n) % length l
[PROOFSTEP]
rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
| (m + n) % length l
[PROOFSTEP]
rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = n % length l + m - length l
[PROOFSTEP]
rw [← add_right_inj l.length, ← add_tsub_assoc_of_le, add_tsub_tsub_cancel, add_tsub_cancel_of_le, add_comm]
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l ≤ n % length l + m
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ n % length l ≤ length l
case inr.e_a.h
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l - n % length l ≤ m
[PROOFSTEP]
exacts [hm', hlt.le, hm]
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - length (drop (n % length l) l) < n % length l
[PROOFSTEP]
rwa [tsub_lt_iff_left hm, length_drop, tsub_add_cancel_of_le hlt.le]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ get (rotate l n) k = get l { val := (↑k + n) % length l, isLt := (_ : (↑k + n) % length l < length l) }
[PROOFSTEP]
rw [← Option.some_inj, ← get?_eq_get, ← get?_eq_get, get?_rotate]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ ↑k < length l
[PROOFSTEP]
exact k.2.trans_eq (length_rotate _ _)
[GOAL]
α : Type u
l : List α
n : ℕ
h : n < length l
⊢ head? (rotate l n) = get? l n
[PROOFSTEP]
rw [← get?_zero, get?_rotate (n.zero_le.trans_lt h), zero_add, Nat.mod_eq_of_lt h]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get (rotate l n)
      { val := (length l - n % length l + ↑k) % length l,
        isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) }
[PROOFSTEP]
rw [get_rotate]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get l
      {
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
[PROOFSTEP]
refine congr_arg l.get (Fin.eq_of_val_eq ?_)
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k =
    ↑{
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
[PROOFSTEP]
simp only [mod_add_mod]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k = (length l - n % length l + ↑k + n) % length l
[PROOFSTEP]
rw [← add_mod_mod, add_right_comm, tsub_add_cancel_of_le, add_mod_left, mod_eq_of_lt]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k < length l
α : Type u l : List α n : ℕ k : Fin (length l) ⊢ n % length l ≤ length l
[PROOFSTEP]
exacts [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]
[GOAL]
α : Type u
hα : Nonempty α
⊢ (∀ (n : ℕ), rotate [] n = []) ↔ ∃ a, [] = replicate (length []) a
[PROOFSTEP]
simp
[GOAL]
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), rotate (a :: l) n = a :: l
n : ℕ
h₁ : n < length (a :: l)
h₂ : n < length (replicate (length (a :: l)) a)
⊢ get (a :: l) { val := n, isLt := h₁ } = get (replicate (length (a :: l)) a) { val := n, isLt := h₂ }
[PROOFSTEP]
rw [get_replicate, ← Option.some_inj, ← get?_eq_get, ← head?_rotate h₁, h, head?_cons]
[GOAL]
α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (length (a :: l)) a_1
n : ℕ
b : α
hb : a :: l = replicate (length (a :: l)) b
⊢ rotate (a :: l) n = a :: l
[PROOFSTEP]
rw [hb, rotate_replicate]
[GOAL]
α : Type u
inst✝ : Nonempty α
l : List α
h : rotate l 1 = l
n✝ n : ℕ
hn : rotate l n = l
⊢ rotate l (succ n) = l
[PROOFSTEP]
rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]
[GOAL]
α : Type u
n : ℕ
⊢ Injective fun l => rotate l n
[PROOFSTEP]
rintro l l' (h : l.rotate n = l'.rotate n)
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
⊢ l = l'
[PROOFSTEP]
have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
hle : length l = length l'
⊢ l = l'
[PROOFSTEP]
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ l = l'
[PROOFSTEP]
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ length (drop (n % length l) l) = length (drop (n % length l') l')
[PROOFSTEP]
simp_all
[GOAL]
case intro
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
hd : drop (n % length l) l = drop (n % length l') l'
ht : take (n % length l) l = take (n % length l') l'
⊢ l = l'
[PROOFSTEP]
rw [← take_append_drop _ l, ht, hd, take_append_drop]
[GOAL]
α : Type u
l l' : List α
n : ℕ
⊢ rotate l n = l' ↔ l = rotate l' (length l' - n % length l')
[PROOFSTEP]
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
[GOAL]
α : Type u
l l' : List α
n : ℕ
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
cases' l'.length.zero_le.eq_or_lt with hl hl
[GOAL]
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil, rotate_eq_nil_iff]
[GOAL]
case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
cases' (Nat.zero_le (n % l'.length)).eq_or_lt with hn hn
[GOAL]
case inr.inl
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
hn : 0 = n % length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
simp [← hn]
[GOAL]
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
hn : 0 < n % length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
rw [mod_eq_of_lt (tsub_lt_self hl hn), tsub_add_cancel_of_le, mod_self, rotate_zero]
[GOAL]
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
hn : 0 < n % length l'
⊢ n % length l' ≤ length l'
[PROOFSTEP]
exact (Nat.mod_lt _ hl).le
[GOAL]
α : Type u
l : List α
n : ℕ
x : α
⊢ rotate l n = [x] ↔ l = [x]
[PROOFSTEP]
rw [rotate_eq_iff, rotate_singleton]
[GOAL]
α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = rotate l n ↔ [x] = l
[PROOFSTEP]
rw [eq_comm, rotate_eq_singleton_iff, eq_comm]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ reverse (rotate l n) = rotate (reverse l) (length l - n % length l)
[PROOFSTEP]
rw [← length_reverse l, ← rotate_eq_iff]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (rotate l n)) n = reverse l
[PROOFSTEP]
induction' n with n hn generalizing l
[GOAL]
case zero
α : Type u
l✝ l : List α
⊢ rotate (reverse (rotate l zero)) zero = reverse l
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
l : List α
⊢ rotate (reverse (rotate l (succ n))) (succ n) = reverse l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
⊢ rotate (reverse (rotate [] (succ n))) (succ n) = reverse []
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
hd : α
tl : List α
⊢ rotate (reverse (rotate (hd :: tl) (succ n))) (succ n) = reverse (hd :: tl)
[PROOFSTEP]
rw [rotate_cons_succ, Nat.succ_eq_add_one, ← rotate_rotate, hn]
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
hd : α
tl : List α
⊢ rotate (reverse (tl ++ [hd])) 1 = reverse (hd :: tl)
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse l) n = reverse (rotate l (length l - n % length l))
[PROOFSTEP]
rw [← reverse_reverse l]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (reverse (reverse l))) n =
    reverse (rotate (reverse (reverse l)) (length (reverse (reverse l)) - n % length (reverse (reverse l))))
[PROOFSTEP]
simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate, length_reverse]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ reverse l = rotate (reverse l) (length l - (length l - n % length l) % length l + (length l - n % length l))
[PROOFSTEP]
rw [← length_reverse l]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
let k := n % l.reverse.length
[GOAL]
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
cases' hk' : k with k'
[GOAL]
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
hk' : k = zero
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
simp_all! [length_reverse, ← rotate_rotate]
[GOAL]
case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
k' : ℕ
hk' : k = succ k'
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
cases' l with x l
[GOAL]
case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % length (reverse [])
hk' : k = succ k'
⊢ reverse [] =
    rotate (reverse [])
      (length (reverse []) - (length (reverse []) - n % length (reverse [])) % length (reverse []) +
        (length (reverse []) - n % length (reverse [])))
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ reverse (x :: l) =
    rotate (reverse (x :: l))
      (length (reverse (x :: l)) -
          (length (reverse (x :: l)) - n % length (reverse (x :: l))) % length (reverse (x :: l)) +
        (length (reverse (x :: l)) - n % length (reverse (x :: l))))
[PROOFSTEP]
rw [Nat.mod_eq_of_lt, tsub_add_cancel_of_le, rotate_length]
[GOAL]
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) ≤ length (reverse (x :: l))
[PROOFSTEP]
exact tsub_le_self
[GOAL]
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) < length (reverse (x :: l))
[PROOFSTEP]
exact tsub_lt_self (by simp) (by simp_all! )
[GOAL]
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ 0 < length (reverse (x :: l))
[PROOFSTEP]
simp
[GOAL]
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ 0 < n % length (reverse (x :: l))
[PROOFSTEP]
simp_all!
[GOAL]
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
⊢ map f (rotate l n) = rotate (map f l) n
[PROOFSTEP]
induction' n with n hn IH generalizing l
[GOAL]
case zero
α : Type u
β : Type u_1
f : α → β
l✝ l : List α
⊢ map f (rotate l zero) = rotate (map f l) zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type u_1
f : α → β
l✝ : List α
n : ℕ
hn : ∀ (l : List α), map f (rotate l n) = rotate (map f l) n
l : List α
⊢ map f (rotate l (succ n)) = rotate (map f l) (succ n)
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
hn : ∀ (l : List α), map f (rotate l n) = rotate (map f l) n
⊢ map f (rotate [] (succ n)) = rotate (map f []) (succ n)
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
hn : ∀ (l : List α), map f (rotate l n) = rotate (map f l) n
hd : α
tl : List α
⊢ map f (rotate (hd :: tl) (succ n)) = rotate (map f (hd :: tl)) (succ n)
[PROOFSTEP]
simp [hn]
[GOAL]
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l ↔ n % length l = 0 ∨ l = []
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l → n % length l = 0 ∨ l = []
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
⊢ n % length l = 0 ∨ l = []
[PROOFSTEP]
cases' l.length.zero_le.eq_or_lt with hl' hl'
[GOAL]
case mp.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 = length l
⊢ n % length l = 0 ∨ l = []
[PROOFSTEP]
simp [← length_eq_zero, ← hl']
[GOAL]
case mp.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0 ∨ l = []
[PROOFSTEP]
left
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
[PROOFSTEP]
rw [nodup_iff_nthLe_inj] at hl
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
[PROOFSTEP]
refine' hl _ _ (mod_lt _ hl') hl' _
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe l (n % length l) (_ : n % length l < length l) = nthLe l 0 hl'
[PROOFSTEP]
rw [← nthLe_rotate' _ n]
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe (rotate l n) ((length l - n % length l + n % length l) % length l)
      (_ : (length l - n % length l + n % length l) % length l < length (rotate l n)) =
    nthLe l 0 hl'
[PROOFSTEP]
simp_rw [h, tsub_add_cancel_of_le (mod_lt _ hl').le, mod_self]
[GOAL]
case mpr
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ n % length l = 0 ∨ l = [] → rotate l n = l
[PROOFSTEP]
rintro (h | h)
[GOAL]
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l n = l
[PROOFSTEP]
rw [← rotate_mod, h]
[GOAL]
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l 0 = l
[PROOFSTEP]
exact rotate_zero l
[GOAL]
case mpr.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : l = []
⊢ rotate l n = l
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
⊢ i % length l = j % length l
[PROOFSTEP]
have hi : i % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
⊢ i % length l = j % length l
[PROOFSTEP]
have hj : j % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ i % length l = j % length l
[PROOFSTEP]
refine' (nodup_iff_nthLe_inj.mp hl) _ _ hi hj _
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe l (i % length l) hi = nthLe l (j % length l) hj
[PROOFSTEP]
rw [← nthLe_rotate' l i, ← nthLe_rotate' l j]
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe (rotate l i) ((length l - i % length l + i % length l) % length l)
      (_ : (length l - i % length l + i % length l) % length l < length (rotate l i)) =
    nthLe (rotate l j) ((length l - j % length l + j % length l) % length l)
      (_ : (length l - j % length l + j % length l) % length l < length (rotate l j))
[PROOFSTEP]
simp [tsub_add_cancel_of_le, hi.le, hj.le, h]
[GOAL]
α : Type u
l✝ l' l : List α
⊢ rotate l 0 = l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~r l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case intro.nil
α : Type u
n : ℕ
⊢ rotate [] n ~r []
[PROOFSTEP]
exists 0
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (hd :: tl) n ~r (hd :: tl)
[PROOFSTEP]
use(hd :: tl).length * n - n
[GOAL]
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (rotate (hd :: tl) n) (length (hd :: tl) * n - n) = hd :: tl
[PROOFSTEP]
rw [rotate_rotate, add_tsub_cancel_of_le, rotate_length_mul]
[GOAL]
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ length (hd :: tl) * n
[PROOFSTEP]
exact Nat.le_mul_of_pos_left (by simp)
[GOAL]
α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < length (hd :: tl)
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' l✝ : List α
n m : ℕ
⊢ rotate l✝ (n + m) = rotate (rotate l✝ n) m
[PROOFSTEP]
rw [rotate_rotate]
[GOAL]
α : Type u
l l' : List α
x✝ : l ~r []
n : ℕ
hn : rotate l n = []
⊢ l = []
[PROOFSTEP]
simpa using hn
[GOAL]
α : Type u
l l' : List α
h : l = []
⊢ l ~r l
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l l' : List α
⊢ [] ~r l ↔ [] = l
[PROOFSTEP]
rw [isRotated_comm, isRotated_nil_iff, eq_comm]
[GOAL]
α : Type u
l l' : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : rotate l n = [x]
⊢ l = [x]
[PROOFSTEP]
simpa using hn
[GOAL]
α : Type u
l l' : List α
x : α
h : l = [x]
⊢ l ~r l
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l l' : List α
x : α
⊢ [x] ~r l ↔ [x] = l
[PROOFSTEP]
rw [isRotated_comm, isRotated_singleton_iff, eq_comm]
[GOAL]
α : Type u
l l' : List α
hd : α
tl : List α
⊢ rotate (hd :: tl) 1 = tl ++ [hd]
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
⊢ rotate (l ++ l') (length l) = l' ++ l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
h : l ~r l'
⊢ List.reverse l ~r List.reverse l'
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l : List α
n : ℕ
⊢ List.reverse l ~r List.reverse (rotate l n)
[PROOFSTEP]
exact ⟨_, (reverse_rotate _ _).symm⟩
[GOAL]
α : Type u
l l' : List α
⊢ reverse l ~r l' ↔ l ~r reverse l'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
l l' : List α
⊢ reverse l ~r l' → l ~r reverse l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
l l' : List α
h : reverse l ~r l'
⊢ l ~r reverse l'
[PROOFSTEP]
simpa using h.reverse
[GOAL]
case mpr
α : Type u
l l' : List α
⊢ l ~r reverse l' → reverse l ~r l'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
l l' : List α
h : l ~r reverse l'
⊢ reverse l ~r l'
[PROOFSTEP]
simpa using h.reverse
[GOAL]
α : Type u
l l' : List α
⊢ reverse l ~r reverse l' ↔ l ~r l'
[PROOFSTEP]
simp [isRotated_reverse_comm_iff]
[GOAL]
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n, n ≤ length l ∧ rotate l n = l'
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
[GOAL]
α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n, n ≤ length l ∧ rotate l n = l'
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1, n_1 ≤ length l ∧ rotate l n_1 = rotate l n
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case intro.nil
α : Type u
n : ℕ
⊢ ∃ n_1, n_1 ≤ length [] ∧ rotate [] n_1 = rotate [] n
[PROOFSTEP]
simp
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ length (hd :: tl) ∧ rotate (hd :: tl) n_1 = rotate (hd :: tl) n
[PROOFSTEP]
refine' ⟨n % (hd :: tl).length, _, rotate_mod _ _⟩
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % length (hd :: tl) ≤ length (hd :: tl)
[PROOFSTEP]
refine' (Nat.mod_lt _ _).le
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ length (hd :: tl) > 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map (rotate l) (range (length l + 1))
[PROOFSTEP]
simp_rw [mem_map, mem_range, isRotated_iff_mod]
[GOAL]
α : Type u
l l' : List α
⊢ (∃ n, n ≤ length l ∧ rotate l n = l') ↔ ∃ a, a < length l + 1 ∧ rotate l a = l'
[PROOFSTEP]
exact ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩, fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩
[GOAL]
α : Type u
l l' : List α
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (rotate l₁ n)
[PROOFSTEP]
rw [map_rotate]
[GOAL]
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r rotate (List.map f l₁) n
[PROOFSTEP]
use n
[GOAL]
α : Type u
l✝ l' l : List α
h : l ≠ []
⊢ cyclicPermutations l = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails l) (inits l))
[PROOFSTEP]
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h
[GOAL]
case intro.intro
α : Type u
l l' : List α
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ cyclicPermutations (hd :: tl) = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails (hd :: tl)) (inits (hd :: tl)))
[PROOFSTEP]
exact cyclicPermutations_cons _ _
[GOAL]
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ length (cyclicPermutations (x :: l)) = length l + 1
[PROOFSTEP]
simp [cyclicPermutations_cons]
[GOAL]
α : Type u
l✝ l' l : List α
h : l ≠ []
⊢ length (cyclicPermutations l) = length l
[PROOFSTEP]
simp [cyclicPermutations_of_ne_nil _ h]
[GOAL]
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
[PROOFSTEP]
obtain rfl | h := eq_or_ne l []
[GOAL]
case inl
α : Type u
l l' : List α
n : ℕ
hn : n < length (cyclicPermutations [])
⊢ nthLe (cyclicPermutations []) n hn = rotate [] n
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
[PROOFSTEP]
rw [length_cyclicPermutations_of_ne_nil _ h] at hn
[GOAL]
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn✝ : n < length (cyclicPermutations l)
hn : n < length l
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn✝ = rotate l n
[PROOFSTEP]
simp [dropLast_eq_take, cyclicPermutations_of_ne_nil _ h, nthLe_take', rotate_eq_drop_append_take hn.le]
[GOAL]
α : Type u
l✝ l' l : List α
⊢ l ∈ cyclicPermutations l
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
α : Type u
l l' : List α
⊢ [] ∈ cyclicPermutations []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ x :: l ∈ cyclicPermutations (x :: l)
[PROOFSTEP]
rw [mem_iff_nthLe]
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ ∃ n h, nthLe (cyclicPermutations (x :: l)) n h = x :: l
[PROOFSTEP]
refine' ⟨0, by simp, _⟩
[GOAL]
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ 0 < length (cyclicPermutations (x :: l))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ nthLe (cyclicPermutations (x :: l)) 0 (_ : 0 < length (cyclicPermutations (x :: l))) = x :: l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l' l : List α
h : l' ∈ cyclicPermutations l
⊢ length l' = length l
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
[GOAL]
case intro.intro
α : Type u
l✝ l : List α
k : ℕ
hk : k < length (cyclicPermutations l)
h : nthLe (cyclicPermutations l) k hk ∈ cyclicPermutations l
⊢ length (nthLe (cyclicPermutations l) k hk) = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' → l ~r l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
l✝ l'✝ l l' : List α
h : l ∈ cyclicPermutations l'
⊢ l ~r l'
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
[GOAL]
case mp.intro.intro
α : Type u
l l'✝ l' : List α
k : ℕ
hk : k < length (cyclicPermutations l')
h : nthLe (cyclicPermutations l') k hk ∈ cyclicPermutations l'
⊢ nthLe (cyclicPermutations l') k hk ~r l'
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u
l✝ l'✝ l l' : List α
⊢ l ~r l' → l ∈ cyclicPermutations l'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
l✝ l'✝ l l' : List α
h : l ~r l'
⊢ l ∈ cyclicPermutations l'
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h.symm
[GOAL]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ rotate l' k ∈ cyclicPermutations l'
[PROOFSTEP]
rw [mem_iff_nthLe]
[GOAL]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n h, nthLe (cyclicPermutations l') n h = rotate l' k
[PROOFSTEP]
simp only [exists_prop, nthLe_cyclicPermutations]
[GOAL]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n, n < length (cyclicPermutations l') ∧ rotate l' n = rotate l' k
[PROOFSTEP]
cases' l' with x l
[GOAL]
case mpr.intro.nil
α : Type u
l l' : List α
k : ℕ
h : rotate [] k ~r []
⊢ ∃ n, n < length (cyclicPermutations []) ∧ rotate [] n = rotate [] k
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ ∃ n, n < length (cyclicPermutations (x :: l)) ∧ rotate (x :: l) n = rotate (x :: l) k
[PROOFSTEP]
refine' ⟨k % length (x :: l), _, rotate_mod _ _⟩
[GOAL]
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ k % length (x :: l) < length (cyclicPermutations (x :: l))
[PROOFSTEP]
simpa using Nat.mod_lt _ (zero_lt_succ _)
[GOAL]
α : Type u
l✝ l' l : List α
⊢ cyclicPermutations l = [[]] ↔ l = []
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by simp [h]⟩
[GOAL]
α : Type u
l✝ l' l : List α
h : l = []
⊢ cyclicPermutations l = [[]]
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
l✝ l' l : List α
h : cyclicPermutations l = [[]]
⊢ l = []
[PROOFSTEP]
rw [eq_comm, ← isRotated_nil_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
[GOAL]
α : Type u
l✝ l' l : List α
x : α
⊢ cyclicPermutations l = [[x]] ↔ l = [x]
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by simp [cyclicPermutations, h, dropLast_eq_take]⟩
[GOAL]
α : Type u
l✝ l' l : List α
x : α
h : l = [x]
⊢ cyclicPermutations l = [[x]]
[PROOFSTEP]
simp [cyclicPermutations, h, dropLast_eq_take]
[GOAL]
α : Type u
l✝ l' l : List α
x : α
h : cyclicPermutations l = [[x]]
⊢ l = [x]
[PROOFSTEP]
rw [eq_comm, ← isRotated_singleton_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
[GOAL]
α : Type u
l✝ l' l : List α
hn : Nodup l
⊢ Nodup (List.cyclicPermutations l)
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
α : Type u
l l' : List α
hn : Nodup []
⊢ Nodup (List.cyclicPermutations [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ Nodup (List.cyclicPermutations (x :: l))
[PROOFSTEP]
rw [nodup_iff_nthLe_inj]
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ ∀ (i j : ℕ) (h₁ : i < length (List.cyclicPermutations (x :: l))) (h₂ : j < length (List.cyclicPermutations (x :: l))),
    nthLe (List.cyclicPermutations (x :: l)) i h₁ = nthLe (List.cyclicPermutations (x :: l)) j h₂ → i = j
[PROOFSTEP]
intro i j hi hj h
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi : i < length (List.cyclicPermutations (x :: l))
hj : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi = nthLe (List.cyclicPermutations (x :: l)) j hj
⊢ i = j
[PROOFSTEP]
simp only [length_cyclicPermutations_cons] at hi hj
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i = j
[PROOFSTEP]
rw [← mod_eq_of_lt hi, ← mod_eq_of_lt hj]
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i % (length l + 1) = j % (length l + 1)
[PROOFSTEP]
apply hn.rotate_congr
[GOAL]
case cons.hn
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ x :: l ≠ []
[PROOFSTEP]
simp
[GOAL]
case cons.h
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ rotate (x :: l) i = rotate (x :: l) j
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
⊢ cyclicPermutations (rotate l k) = rotate (cyclicPermutations l) k
[PROOFSTEP]
have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) :=
  by
  cases l
  · simp
  · rw [length_cyclicPermutations_of_ne_nil] <;> simp
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
⊢ length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
l l' : List α
k : ℕ
⊢ length (cyclicPermutations (rotate [] k)) = length (rotate (cyclicPermutations []) k)
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ length (cyclicPermutations (rotate (head✝ :: tail✝) k)) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
[PROOFSTEP]
rw [length_cyclicPermutations_of_ne_nil]
[GOAL]
case cons
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ length (rotate (head✝ :: tail✝) k) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
[PROOFSTEP]
simp
[GOAL]
case cons.h
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ rotate (head✝ :: tail✝) k ≠ []
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
⊢ cyclicPermutations (rotate l k) = rotate (cyclicPermutations l) k
[PROOFSTEP]
refine' ext_nthLe this fun n hn hn' => _
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ nthLe (cyclicPermutations (rotate l k)) n hn = nthLe (rotate (cyclicPermutations l) k) n hn'
[PROOFSTEP]
rw [nthLe_rotate, nthLe_cyclicPermutations, rotate_rotate, ← rotate_mod, add_comm]
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ rotate l ((n + k) % length l) =
    nthLe (cyclicPermutations l) ((n + k) % length (cyclicPermutations l))
      (_ : (n + k) % length (cyclicPermutations l) < length (cyclicPermutations l))
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
l l' : List α
k n : ℕ
this : length (cyclicPermutations (rotate [] k)) = length (rotate (cyclicPermutations []) k)
hn : n < length (cyclicPermutations (rotate [] k))
hn' : n < length (rotate (cyclicPermutations []) k)
⊢ rotate [] ((n + k) % length []) =
    nthLe (cyclicPermutations []) ((n + k) % length (cyclicPermutations []))
      (_ : (n + k) % length (cyclicPermutations []) < length (cyclicPermutations []))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l l' : List α
k n : ℕ
head✝ : α
tail✝ : List α
this : length (cyclicPermutations (rotate (head✝ :: tail✝) k)) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
hn : n < length (cyclicPermutations (rotate (head✝ :: tail✝) k))
hn' : n < length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
⊢ rotate (head✝ :: tail✝) ((n + k) % length (head✝ :: tail✝)) =
    nthLe (cyclicPermutations (head✝ :: tail✝)) ((n + k) % length (cyclicPermutations (head✝ :: tail✝)))
      (_ : (n + k) % length (cyclicPermutations (head✝ :: tail✝)) < length (cyclicPermutations (head✝ :: tail✝)))
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l'✝ l l' : List α
h : l ~r l'
⊢ List.cyclicPermutations l ~r List.cyclicPermutations l'
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h
[GOAL]
case intro
α : Type u
l✝ l' l : List α
k : ℕ
⊢ List.cyclicPermutations l ~r List.cyclicPermutations (rotate l k)
[PROOFSTEP]
exact ⟨k, by simp⟩
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
⊢ rotate (List.cyclicPermutations l) k = List.cyclicPermutations (rotate l k)
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l'✝ l l' : List α
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
by_cases hl : l = []
[GOAL]
case pos
α : Type u
l✝ l'✝ l l' : List α
hl : l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
simp [hl, eq_comm]
[GOAL]
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
have hl' : l.cyclicPermutations.length = l.length := length_cyclicPermutations_of_ne_nil _ hl
[GOAL]
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
refine' ⟨fun h => _, IsRotated.cyclicPermutations⟩
[GOAL]
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
h : cyclicPermutations l ~r cyclicPermutations l'
⊢ l ~r l'
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ l ~r l'
[PROOFSTEP]
refine' ⟨k % l.length, _⟩
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ rotate l (k % length l) = l'
[PROOFSTEP]
have hk' : k % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hl)
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ rotate l (k % length l) = l'
[PROOFSTEP]
rw [← nthLe_cyclicPermutations _ _ (hk'.trans_le hl'.ge), ← nthLe_rotate' _ k]
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ nthLe (rotate (cyclicPermutations l) k)
      ((length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
        length (cyclicPermutations l))
      (_ :
        (length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
            length (cyclicPermutations l) <
          length (rotate (cyclicPermutations l) k)) =
    l'
[PROOFSTEP]
simp [hk, hl', tsub_add_cancel_of_le hk'.le]


[GOAL]
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₂ : List α
⊢ [] <+ []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ l₁ ∪ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂
[PROOFSTEP]
simp only [e, cons_union, insert_of_mem h]
[GOAL]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
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₂
[PROOFSTEP]
simp only [cons_append, cons_union, e, insert_of_not_mem h]
[GOAL]
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ (∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x
[PROOFSTEP]
simp only [mem_union_iff, or_imp, forall_and]
[GOAL]
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂
[PROOFSTEP]
simp only [Inter.inter, List.inter, filter_cons_of_pos, h]
[GOAL]
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂
[PROOFSTEP]
simp only [Inter.inter, List.inter, filter_cons_of_neg, h]
[GOAL]
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂
[PROOFSTEP]
simpa using of_mem_filter h
[GOAL]
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ decide (a ∈ l₂) = true
[PROOFSTEP]
simpa using h₂
[GOAL]
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ Disjoint l₁ l₂
[PROOFSTEP]
simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]
[GOAL]
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ Disjoint l₁ l₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
xs ys : List α
⊢ List.inter xs (reverse ys) = List.inter xs ys
[PROOFSTEP]
simp only [List.inter, mem_reverse]
[GOAL]
α : Type u_1
l✝ l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l : List α
⊢ List.bagInter [] l = []
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ List.bagInter [] [] = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ List.bagInter [] (head✝ :: tail✝) = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l✝ l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l : List α
⊢ List.bagInter l [] = []
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ List.bagInter [] [] = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ List.bagInter (head✝ :: tail✝) [] = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ List.bagInter (a :: l₁) l₂ = a :: List.bagInter l₁ (List.erase l₂ a)
[PROOFSTEP]
cases l₂
[GOAL]
case nil
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ []
⊢ List.bagInter (a :: l₁) [] = a :: List.bagInter l₁ (List.erase [] a)
[PROOFSTEP]
exact if_pos h
[GOAL]
case cons
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : a ∈ head✝ :: tail✝
⊢ List.bagInter (a :: l₁) (head✝ :: tail✝) = a :: List.bagInter l₁ (List.erase (head✝ :: tail✝) a)
[PROOFSTEP]
simp only [List.bagInter, if_pos (elem_eq_true_of_mem h)]
[GOAL]
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ List.bagInter (a :: l₁) l₂ = List.bagInter l₁ l₂
[PROOFSTEP]
cases l₂
[GOAL]
case nil
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ []
⊢ List.bagInter (a :: l₁) [] = List.bagInter l₁ []
[PROOFSTEP]
simp only [bagInter_nil]
[GOAL]
case cons
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ List.bagInter (a :: l₁) (head✝ :: tail✝) = List.bagInter l₁ (head✝ :: tail✝)
[PROOFSTEP]
simp only [erase_of_not_mem h, List.bagInter, if_neg (mt mem_of_elem_eq_true h)]
[GOAL]
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₂ : List α
⊢ a ∈ List.bagInter [] l₂ ↔ a ∈ [] ∧ a ∈ l₂
[PROOFSTEP]
simp only [nil_bagInter, not_mem_nil, false_and_iff]
[GOAL]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
⊢ a ∈ List.bagInter (b :: l₁) l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂
[PROOFSTEP]
by_cases h : b ∈ l₂
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ a ∈ List.bagInter (b :: l₁) l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂
[PROOFSTEP]
rw [cons_bagInter_of_pos _ h, mem_cons, mem_cons, mem_bagInter]
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ List.erase l₂ b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂
[PROOFSTEP]
by_cases ba : a = b
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
ba : a = b
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ List.erase l₂ b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂
[PROOFSTEP]
simp only [ba, h, eq_self_iff_true, true_or_iff, true_and_iff]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
ba : ¬a = b
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ List.erase l₂ b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂
[PROOFSTEP]
simp only [mem_erase_of_ne ba, ba, false_or_iff]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a ∈ List.bagInter (b :: l₁) l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂
[PROOFSTEP]
rw [cons_bagInter_of_neg _ h, mem_bagInter, mem_cons, or_and_right]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a ∈ l₁ ∧ a ∈ l₂ ↔ a = b ∧ a ∈ l₂ ∨ a ∈ l₁ ∧ a ∈ l₂
[PROOFSTEP]
symm
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a = b ∧ a ∈ l₂ ∨ a ∈ l₁ ∧ a ∈ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
[PROOFSTEP]
apply or_iff_right_of_imp
[GOAL]
case neg.ha
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a = b ∧ a ∈ l₂ → a ∈ l₁ ∧ a ∈ l₂
[PROOFSTEP]
rintro ⟨rfl, h'⟩
[GOAL]
case neg.ha.intro
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h' : a ∈ l₂
h : ¬a ∈ l₂
⊢ a ∈ l₁ ∧ a ∈ l₂
[PROOFSTEP]
exact h.elim h'
[GOAL]
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₂ : List α
⊢ count a (List.bagInter [] l₂) = min (count a []) (count a l₂)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ count a (List.bagInter l₁ []) = min (count a l₁) (count a [])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
by_cases hb : b ∈ l₂
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
rw [cons_bagInter_of_pos _ hb, count_cons', count_cons', count_bagInter, count_erase, ← min_add_add_right]
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
[PROOFSTEP]
by_cases ab : a = b
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : a = b
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
[PROOFSTEP]
rw [if_pos ab, @tsub_add_cancel_of_le]
[GOAL]
case pos.h
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : a = b
⊢ 1 ≤ count a l₂
[PROOFSTEP]
rwa [succ_le_iff, count_pos, ab]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : ¬a = b
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
[PROOFSTEP]
rw [if_neg ab, tsub_zero, add_zero, add_zero]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
rw [cons_bagInter_of_neg _ hb, count_bagInter]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
by_cases ab : a = b
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
rw [← ab] at hb
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬a ∈ l₂
ab : a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
rw [count_eq_zero.2 hb, min_zero, min_zero]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : ¬a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
[PROOFSTEP]
rw [count_cons_of_ne ab]
[GOAL]
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₂ : List α
⊢ List.bagInter [] l₂ <+ []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ List.bagInter (b :: l₁) l₂ <+ b :: l₁
[PROOFSTEP]
by_cases h : b ∈ l₂
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ List.bagInter (b :: l₁) l₂ <+ b :: l₁
[PROOFSTEP]
simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ List.bagInter (b :: l₁) l₂ <+ b :: l₁
[PROOFSTEP]
simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ b :: List.bagInter l₁ (List.erase l₂ b) <+ b :: l₁
[PROOFSTEP]
exact (bagInter_sublist_left _ _).cons_cons _
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ List.bagInter l₁ l₂ <+ b :: l₁
[PROOFSTEP]
apply sublist_cons_of_sublist
[GOAL]
case neg.a
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ List.bagInter l₁ l₂ <+ l₁
[PROOFSTEP]
apply bagInter_sublist_left
[GOAL]
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₂ : List α
⊢ List.bagInter [] l₂ = [] ↔ [] ∩ l₂ = []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ List.bagInter (b :: l₁) l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
[PROOFSTEP]
by_cases h : b ∈ l₂
[GOAL]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ List.bagInter (b :: l₁) l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ List.bagInter (b :: l₁) l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ List.bagInter l₁ l₂ = [] ↔ l₁ ∩ l₂ = []
[PROOFSTEP]
exact bagInter_nil_iff_inter_nil l₁ l₂