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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ a ∈ l ∧ b ∈ l.tail ∧ R a b)

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
c : α
l₂ : List α
⊢ IsChain R ([] ++ c :: l₂) ↔ IsChain R ([] ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
R : α → α → Prop
c x✝ : α
l₂ : List α
⊢ IsChain R ([x✝] ++ c :: l₂) ↔ IsChain R ([x✝] ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
c x✝ y✝ : α
xs✝ : List α
a✝¹ : ∀ {l₂ : List α}, IsChain R (xs✝ ++ c :: l₂) ↔ IsChain R (xs✝ ++ [c]) ∧ IsChain R (c :: l₂)
a✝ : ∀ (y : α) {l₂ : List α}, IsChain R (y :: xs✝ ++ c :: l₂) ↔ IsChain R (y :: xs✝ ++ [c]) ∧ IsChain R (c :: l₂)
l₂ : List α
⊢ IsChain R (x✝ :: y✝ :: xs✝ ++ c :: l₂) ↔ IsChain R (x✝ :: y✝ :: xs✝ ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
R : α → α → Prop
x✝ : α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [x✝] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R [x✝]

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Tactic:
by
  simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
⊢ IsChain R (map f []) ↔ IsChain (fun a b ↦ R (f a) (f b)) []

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ : β
⊢ IsChain R (map f [x✝]) ↔ IsChain (fun a b ↦ R (f a) (f b)) [x✝]

Tactic:
grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ y✝ : β
xs✝ : List β
a✝¹ : IsChain R (map f xs✝) ↔ IsChain (fun a b ↦ R (f a) (f b)) xs✝
a✝ : ∀ (y : β), IsChain R (map f (y :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (y :: xs✝)
⊢ IsChain R (map f (x✝ :: y✝ :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (x✝ :: y✝ :: xs✝)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
l : List β
⊢ IsChain R (map f l) ↔ IsChain (fun a b ↦ R (f a) (f b)) l

Tactic:
induction l using twoStepInduction <;> grind

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
hl : ∀ (a : α), a ∈ [] → p a
⊢ IsChain S (pmap f [] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) []

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ : α
hl : ∀ (a : α), a ∈ [x✝] → p a
⊢ IsChain S (pmap f [x✝] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) [x✝]

Tactic:
grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ y✝ : α
xs✝ : List α
a✝¹ :
  ∀ (hl : ∀ (a : α), a ∈ xs✝ → p a), IsChain S (pmap f xs✝ hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) xs✝
a✝ :
  ∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs✝ → p a),
    IsChain S (pmap f (y :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (y :: xs✝)
hl : ∀ (a : α), a ∈ x✝ :: y✝ :: xs✝ → p a
⊢ IsChain S (pmap f (x✝ :: y✝ :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (x✝ :: y✝ :: xs✝)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
⊢ IsChain S (pmap f l hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) l

Tactic:
induction l using twoStepInduction <;> grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
hl₁ : IsChain R l
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a b : α), a ∈ l → b ∈ l → R a b → ∃ ha hb, S (f a ha) (f b hb)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
hl₂ : IsChain S (pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ ha hb, S (f a ha) (f b hb)) → R a b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
l : List β
hl : ∀ (b : β), b ∈ l → p b
a : β
ha : p a
⊢ ∀ (a_1 : β), a_1 ∈ a :: l → p a_1

Tactic:
grind

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun x1 x2 ↦ x1 * x2) 1 s)

Tactic:
exact foldr_induction (· * ·) 1 p s p_mul p_one p_s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
a : α
ha : p a
hl₁ : IsChain R (a :: l)
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a_1 b : α), a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → ∃ ha hb, S (f a_1 ha) (f b hb)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : IsChain S (f a ha :: pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ ha hb, S (f a ha) (f b hb)) → R a b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
l : List α
h : IsChain R l
hne : l.dropLast ≠ []
⊢ l ≠ []

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
⊢ IsChain R [].reverse ↔ IsChain (fun a b ↦ R b a) []

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
R : α → α → Prop
a : α
⊢ IsChain R [a].reverse ↔ IsChain (fun a b ↦ R b a) [a]

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u
⊢ [].rotate' 0 = []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate' 0 = head✝ :: tail✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
⊢ l₁.prod = l₂.prod

Tactic:
refine h.foldr_eq' (Pairwise.forall_of_forall (fun _ _ _ ↦ rfl) <| hc.imp fun {a b} h z ↦ ?_) 1

Goal state after:
M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h✝ : l₁ ~ l₂
hc : Pairwise Commute l₁
this : Std.Symm fun x y ↦ ∀ (z : M), y * (x * z) = x * (y * z)
a b : M
h : Commute a b
z : M
⊢ b * (a * z) = a * (b * z)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1

Tactic:
← rotate_mod,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate (n % (a :: l).length)).prod = 1
Module: Mathlib.Data.List.Chain

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

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
h : IsChain r []
initial : ∀ (lne : [] ≠ []), p ([].head lne)
⊢ ∀ (i : α), i ∈ [] → p i

Tactic:
grind

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

Goal state before:
pp: case singleton
α : Type u_1
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : α
h : IsChain r [x✝]
initial : ∀ (lne : [x✝] ≠ []), p ([x✝].head lne)
⊢ ∀ (i : α), i ∈ [x✝] → p i

Tactic:
grind

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

Goal state before:
pp: case cons_cons
α : Type u_1
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ y✝ : α
xs✝ : List α
a✝¹ : IsChain r xs✝ → (∀ (lne : xs✝ ≠ []), p (xs✝.head lne)) → ∀ (i : α), i ∈ xs✝ → p i
a✝ :
  ∀ (y : α), IsChain r (y :: xs✝) → (∀ (lne : y :: xs✝ ≠ []), p ((y :: xs✝).head lne)) → ∀ (i : α), i ∈ y :: xs✝ → p i
h : IsChain r (x✝ :: y✝ :: xs✝)
initial : ∀ (lne : x✝ :: y✝ :: xs✝ ≠ []), p ((x✝ :: y✝ :: xs✝).head lne)
⊢ ∀ (i : α), i ∈ x✝ :: y✝ :: xs✝ → p i

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
H : (∀ (lne : l.reverse ≠ []), p (l.reverse.head lne)) → ∀ (i : α), i ∈ l.reverse → p i
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
hm : IsChain (fun x1 x2 ↦ x1 > x2) []
hmas : [] ≤ as
⊢ IsChain (fun x1 x2 ↦ x1 > x2) [a]

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : 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
n : ℕ
hn : n ∈ map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)
⊢ n = 0

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_3
R : α → α → Prop
v : α
hl : IsChain R []
hv : ∀ (lne : [] ≠ []), R v ([].head lne)
⊢ IsChain R [v]

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_3
R : α → α → Prop
v head✝ : α
tail✝ : List α
hl : IsChain R (head✝ :: tail✝)
hv : ∀ (lne : head✝ :: tail✝ ≠ []), R v ((head✝ :: tail✝).head lne)
⊢ IsChain R (v :: head✝ :: tail✝)

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case nil
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
⊢ ([].sigma l₂).length = (map (fun a ↦ (l₂ a).length) []).sum

Tactic:
rfl

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

Goal state before:
pp: case zero
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
hi : 0 < l.length
⊢ f^[0] l[0] = l[0]

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: a : ℕ
l : List ℕ
⊢ (a :: l).ranges.flatten = range (a :: l).sum

Tactic:
by simp [ranges, ← map_flatten, ranges_flatten, range_add]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • (a ::ₘ s) = n • {a} + n • s

Tactic:
by
  rw [← singleton_add, nsmul_add]

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

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 0 a)

Tactic:
grind

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

Goal state before:
pp: case one
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 1 a)

Tactic:
grind

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

Goal state before:
pp: case more
α : Type u_1
r : α → α → Prop
a : α
h : r a a
n✝ : ℕ
a✝¹ : IsChain r (replicate n✝ a)
a✝ : IsChain r (replicate (n✝ + 1) a)
⊢ IsChain r (replicate (n✝ + 2) a)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
l' : List α
hne : 1 < l'.length
hsub : l' <:+: l.reverse
⊢ l'.reverse ≠ []

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
⊢ op [].prod = (map op []).reverse.prod

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
s : Multiset α
⊢ f s = g s

Tactic:
induction s using Multiset.induction_on with
  | empty => simp only [_root_.map_zero]
  | cons a s ih => simp only [← singleton_add, _root_.map_add, ih, h]

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

Goal state before:
pp: α : 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⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ l = ↑l'

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join

Tactic:
rfl

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ prod 0 = 1

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate i = l.rotate j

Tactic:
← rotate_mod,

Goal state after:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate (i % l.length) = l.rotate j
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
h : l = []
⊢ l ~r l

Tactic:
rfl

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

Goal state before:
pp: α : Type u
l : List α
x : α
h : l = [x]
⊢ l ~r l

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.disjiUnion singleton ⋯ = s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
h : (↑s).PairwiseDisjoint f
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (s.disjiUnion f h) = s.disjiUnion (fun a ↦ filter p (f a)) ⋯

Tactic:
grind

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

Goal state before:
pp: ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ (map (fun i ↦ (f i)⁻¹) m).prod = (map (Inv.inv ∘ f) m).prod

Tactic:
Function.comp_def

Goal state after:
ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ (map (fun i ↦ (f i)⁻¹) m).prod = (map (fun x ↦ (f x)⁻¹) m).prod
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hfg' : i ≠ j → (fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)) i j
hj : j ∈ s
⊢ Disjoint (f i) (g j)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ s.disjiUnion (fun a ↦ (f a).disjUnion (g a) ⋯) ⋯ = (s.disjiUnion f hf).disjUnion (s.disjiUnion g hg) ⋯

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
⊢ s₁.biUnion t₁ = s₂.biUnion t₂

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
s' : Finset β
⊢ s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Finset β
inst✝ : DecidableEq β
a : α
⊢ {a}.biUnion t = t a

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst✝ : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
⊢ s₁.biUnion t ⊆ s₂.biUnion t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
u : α → Finset β
x : α
xs : x ∈ s
⊢ u x ⊆ s.biUnion u

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → Finset β
⊢ s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.biUnion singleton = s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (s.biUnion f) = s.biUnion fun a ↦ filter p (f a)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ (t.biUnion fun a ↦ {c ∈ s | f c = a}) = s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b : β
⊢ (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate (k + ↑⟨n, hn⟩) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩

Tactic:
← rotate_mod,

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((k + ↑⟨n, hn⟩) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
⊢ (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion fun x ↦ t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → β
⊢ (s.biUnion fun a ↦ {f a}) = image f s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ choose 0 0 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).choose 0 = 1

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
| map ((fun x ↦ (x, a)) ∘ Prod.fst) l.zipIdx

Tactic:
Function.comp_def

Goal state after:
α : Type u_1
a : α
l : List α
| map (fun x ↦ (x.fst, a)) l.zipIdx
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n l : ℕ
hk : 0 < l + 1
⊢ (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: k l : ℕ
hn : 0 < l + 1
⊢ (l + 1).choose (k + 1) = (l + 1 - 1).choose k + (l + 1 - 1).choose (k + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ choose 0 0 = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : n✝.choose n✝ = 1
⊢ (n✝ + 1).choose (n✝ + 1) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ 0 * (0 + 1) / 2 = 0 * (0 - 1 + 2) / 2

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (n✝ + 1) * (n✝ + 1 + 1) / 2 = (n✝ + 1) * (n✝ + 1 - 1 + 2) / 2

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (b, b) l.offDiag = count b l * count b l - count b l
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count b l ≤ count b l * count b l
h✝¹ : c = b
h✝ : a = b
⊢ count b l + count b l + (count b l * count b l - count b l) = (count b l + 1) * (count b l + 1) - (count b l + 1)

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count a l ≤ count a l * count a l
h✝¹ : c = a
h✝ : ¬a = b
⊢ count b l + count a l * count b l = (count a l + 1) * count b l

Tactic:
grind

Goal state after: