mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)

Tactic:
·

Goal state after:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!

pp: case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Range

Goal state before:
pp: a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ Function.Injective fun x ↦ a + x

Tactic:
exact fun u v => Nat.add_left_cancel

Goal state after:
Module: Mathlib.Data.List.ProdSigma

Goal state before:
pp: α : Type u_1
σ : α → Type u_3
head✝ : α
l : List α
⊢ ((head✝ :: l).sigma fun a ↦ []) = []

Tactic:
by simp [sigma_cons, sigma_nil l]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = (↑s.toList).prod

Tactic:
prod_coe

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = s.toList.prod
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

pp: case neg
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)

Tactic:
·

Goal state after:
case pos
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit (m :: L).prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
rw [prod_cons, IsUnit.mul_iff] at h

Goal state after:
case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b

pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = countP p as

pp: case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
·

Goal state after:
case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = countP p as
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

pp: case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
·

Goal state after:
case inl
α : Type u
l : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
·

Goal state after:
case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
l' : List α
⊢ ([] ++ l').rotate' [].length = l' ++ []

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝

Tactic:
·

Goal state after:
case nil
α : Type u
l' : List α
⊢ ([] ++ l').rotate' [].length = l' ++ []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝

Tactic:
·

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ [].rotate' (n + 1) ~ []

pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
·

Goal state after:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ [].rotate' (n + 1) ~ []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
·

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate' n ~ l

Tactic:
induction n generalizing l with

Goal state after:
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.cons.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'

pp: case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'

Tactic:
·

Goal state after:
case cons.cons.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
⊢ [].rotate (n + 1) = [] ↔ [] = []

pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
·

Goal state after:
case succ.nil
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
⊢ [].rotate (n + 1) = [] ↔ [] = []
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'

Tactic:
·

Goal state after:
case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
·

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ l = []

Tactic:
induction n generalizing l with

Goal state after:
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ i < l.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0

pp: case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
·

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
·

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • 0) = n • filter p 0

pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • 0) = n • filter p 0
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?

pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
·

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}

Tactic:
·

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
·

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩

pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
·

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : ¬a ∈ s
⊢ count a s ≤ count a (s.card • t)

pp: case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ count a s ≤ count a (s.card • t)

Tactic:
·

Goal state after:
case pos
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : ¬a ∈ s
⊢ count a s ≤ count a (s.card • t)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ a ∈ (↑⟨a :: l, hl⟩).head?

pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : Acc r a
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
·

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ a ∈ (↑⟨a :: l, hl⟩).head?
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'

pp: case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
·

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
·

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

pp: case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
·

Goal state after:
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
·

Goal state after:
case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)