mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ fract (a - ↑m) = fract a

Tactic:
fract

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ fract (a - ↑n) = fract a

Tactic:
fract

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ -⌈a + ↑z⌉ = -(⌈a⌉ + z)

Tactic:
neg_add',

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ -⌈a + ↑z⌉ = -⌈a⌉ - z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊-(a + ↑z)⌋ = ⌊-a⌋ - z

Tactic:
neg_add',

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌊-a - ↑z⌋ = ⌊-a⌋ - z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b * a - a) = b * a

Tactic:
add_sub_cancel

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b * a = b * a
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l

Tactic:
simp_rw [count, List.count, coe_countP (a = ·) l, @eq_comm _ a]
  rfl

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝³ : Group G
inst✝² : Torsor G P
inst✝¹ : SMul G Q
inst✝ : SDiv G Q
f : P → Q
hf : Surjective f
smul : ∀ (c : G) (x : P), f (c • x) = c • f x
sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y
⊢ ∀ (p₁ p₂ : Q), (p₁ /ₛ p₂) • p₂ = p₁

Tactic:
simp [hf.forall, ← smul, ← sdiv]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝³ : Group G
inst✝² : Torsor G P
inst✝¹ : SMul G Q
inst✝ : SDiv G Q
f : P → Q
hf : Surjective f
smul : ∀ (c : G) (x : P), f (c • x) = c • f x
sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y
⊢ ∀ (g : G) (p : Q), g • p /ₛ p = g

Tactic:
simp [hf.forall, ← smul, ← sdiv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔ ∀ (a : α), count a (Quot.mk (⇑(isSetoid α)) _l) ≤ 1

Tactic:
simp only [quot_mk_to_coe'', coe_nodup, coe_count]
    exact List.nodup_iff_count_le_one

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧

Tactic:
convert! List.count_erase_of_ne ab (l := l)

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = List.count a (l.erase b)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ y, y ∈ l ∧ y ≠ x

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl hl =>
    specialize hl h.of_cons
    by_cases hx : tl = [x]
    · simpa [hx, and_comm, and_or_left] using h
    · rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l.dedup
⊢ ¬∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b

Tactic:
by simpa only [forall_mem_ne, not_not] using! h

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ t = map (fun x ↦ i ↑x ⋯) s.attach

Tactic:
ht.ext

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ ∀ (a : β), a ∈ t ↔ a ∈ map (fun x ↦ i ↑x ⋯) s.attach

α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ (map (fun x ↦ i ↑x ⋯) s.attach).Nodup
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ pmap (fun x x_1 ↦ f x) s ⋯ = map (fun x ↦ f ↑x) s.attach

Tactic:
pmap_eq_map_attach

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map (fun x ↦ f ↑x) s.attach
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
⊢ Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ =
    fun ex_unique ↦ List.chooseX p b ⋯

Tactic:
funext hp

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
⊢ Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ hp =
    List.chooseX p b ⋯
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).inits = map (map g) l.inits

Tactic:
induction l using reverseRecOn <;> simp [*]

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

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).tails = map (map g) l.tails

Tactic:
induction l using reverseRecOn <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
by
  simp only [disjoint_right, mem_union, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
⊢ (image f)^[n] s = image f^[n] s

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ_apply', iterate_succ', ih, image_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (image f s).val.card = s.val.card
⊢ Set.InjOn f ↑s

Tactic:
image,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).toFinset.val.card = s.val.card
⊢ Set.InjOn f ↑s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.SurjOn f ↑s ↑t
⊢ #t ≤ #s

Tactic:
unfold Set.SurjOn at hf

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ↑t ⊆ f '' ↑s
⊢ #t ≤ #s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i ≠ p

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p

Tactic:
· rw [succAbove_of_castSucc_lt _ _ h]
    exact Fin.ne_of_lt h

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s

Tactic:
rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

Goal state after:
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }

Tactic:
rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype]

Goal state after:
case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
obtain rfl | hs₀ := s.eq_empty_or_nonempty
  · simp
  obtain ⟨n, hn', hn⟩ := image_iterate_stabilises_lt_card hs hs₀
  exact ⟨n, hn'.le, hn⟩

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
⊢ m = n

Tactic:
by_contra hmn

Goal state after:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn : ¬m = n
⊢ False
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
xs : List α
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
by
  induction xs <;> grind [Std.Refl]

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).Finite

Tactic:
by
  have := hs.to_subtype
  apply toFinite

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))

Tactic:
rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
      ha.assoc]

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z ∈ {x, y}

Tactic:
simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l.reverse).SortedLT ↔ l.reverse.SortedLT

Tactic:
sortedLT_listMap

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

Goal state before:
pp: ι : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Multiset ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (map f ⟦l⟧).prod (map g ⟦l⟧).prod

Tactic:
simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]

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 : IsChain (flip (flip r)) l
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
replace H := (isChain_reverse.mpr H).induction _ _ (fun _ _ h ↦ carries h)

Goal state after:
α : 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
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:
· rw [List.head?_cons, Option.mem_some_iff]

Goal state after:
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⟩
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + n % l.length + k) % l.length

Tactic:
Nat.sub_add_cancel,

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length + k) % l.length

α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length
Module: Mathlib.Data.List.Rotate

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

Tactic:
Nat.sub_add_cancel,

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

case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse

Tactic:
reverse_rotate,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.reverse.reverse.rotate n =
    l.reverse.reverse.reverse.rotate
      (l.reverse.reverse.length - (l.reverse.reverse.length - n % l.reverse.reverse.length) % l.reverse.reverse.length)
Module: Mathlib.Data.List.Chain

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

Tactic:
induction this with

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

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Tactic:
Nat.sub_add_cancel,

Goal state after:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse = (x :: l).reverse.rotate (x :: l).reverse.length

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
induction s using Multiset.induction

Goal state after:
case empty
n : ℕ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
induction s using Multiset.induction

Goal state after:
case empty
n : ℕ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
induction s using Multiset.induction

Goal state after:
case empty
n : ℤ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
induction s using Multiset.induction

Goal state after:
case empty
n : ℤ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s

Tactic:
induction s using Multiset.induction

Goal state after:
case empty
α : Type u_1
β : Type v
t : Multiset β
⊢ map Prod.swap (0 ×ˢ t) = t ×ˢ 0

case cons
α : Type u_1
β : Type v
t : Multiset β
a✝¹ : α
s✝ : Multiset α
a✝ : map Prod.swap (s✝ ×ˢ t) = t ×ˢ s✝
⊢ map Prod.swap ((a✝¹ ::ₘ s✝) ×ˢ t) = t ×ˢ (a✝¹ ::ₘ s✝)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
⊢ (map f (s ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s).prod

Tactic:
induction s using Multiset.induction

Goal state after:
case empty
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
⊢ (map f (0 ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) 0).prod

case cons
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
a✝¹ : α
s✝ : Multiset α
a✝ : (map f (s✝ ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s✝).prod
⊢ (map f ((a✝¹ ::ₘ s✝) ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) (a✝¹ ::ₘ s✝)).prod
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
⊢ ((a ::ₘ s).pi t).Nodup

Tactic:
have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
⊢ ((a ::ₘ s).pi t).Nodup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
r n : ℕ
b : n < r
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
choose_eq_zero_of_lt b

Goal state after:
case inr
r n : ℕ
b : n < r
⊢ 0 ≤ n.choose (n / 2)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
      Nat.choose_succ_succ]

Goal state after:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
g h : G
⊢ ∃ g_1, g_1 • g • x₀ = h • x₀

Tactic:
exact ⟨h * g⁻¹, by simp [mul_smul]⟩

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)

Tactic:
have := Fintype.ofFinite (PLift α)
  have := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ t.Nonempty ∧ ¬s.Finite ∨ s.Nonempty ∧ ¬t.Finite

Tactic:
← Classical.not_imp

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)

Goal state after:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(∅ ^ k) = Fintype.card ↑(∅ ^ Fintype.card G)

case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j

Tactic:
image_iUnion

Goal state after: