mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
simp only [subset_iff, not_imp_not]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₃) * (p₃ /ₛ p₂) = p₁ /ₛ p₂

Tactic:
sdiv_mul_sdiv_cancel

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ /ₛ p₂ = p₁ /ₛ p₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ (pointReflection x) y = y ↔ y = x

Tactic:
by
  rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∈ s
⊢ count a s = 1

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0

Tactic:
· exact count_eq_one_of_mem d h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s t ↔ s = t

Tactic:
constructor
  · intro h
    induction h <;> simp [*]
  · rintro rfl
    exact rel_eq_refl

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

Goal state before:
pp: case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
· exact (h j i hj hi hji hg.symm).elim

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <+: l₂
hne : l₂ ≠ []
hl : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
grind [List.IsPrefix]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
⊢ ∀ (x : Multiset α), (∀ (x_1 : α), x_1 ∈ x → p x_1) → ∃ y, map c y = x

Tactic:
rintro ⟨l⟩ hl
    lift l to List β using hl
    exact ⟨l, map_coe _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b

Tactic:
by
  constructor
  · intro h
    obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
    refine ⟨a, ha, ?_⟩
    rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
  · rintro ⟨a, rfl, rfl⟩
    simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ⟦l₁⟧ - ⟦l₂⟧ = foldl erase ⟦l₁⟧ ⟦l₂⟧

Tactic:
change ofList (l₁.diff l₂) = foldl erase l₁ l₂
    rw [diff_eq_foldl l₁ l₂]
    symm
    exact foldl_hom _ fun x y => rfl

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)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g t

Tactic:
rw [this, Multiset.map_map]

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 (g ∘ fun x ↦ i ↑x ⋯) s.attach
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup

Tactic:
induction l₁ with | nil => rfl | cons a l₁ IH => ?_
  simp only [cons_union] at *
  rw [← IH, cons_append]
  by_cases h : a ∈ dedup (l₁ ++ l₂)
  · rw [dedup_cons_of_mem' h, insert_of_mem h]
  · rw [dedup_cons_of_notMem' h, insert_of_not_mem h]

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs

Tactic:
simp only [dropSlice_eq]
  have : n ≤ n + m := Nat.le_add_right _ _
  have h₂ := h.nodup_iff.2 h'
  apply Perm.trans _ (Perm.inter_append _).symm
  · exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')
  · exact disjoint_take_drop h₂ this

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t

Tactic:
refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
  · simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)
  · rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]
    exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (range n).Nontrivial

Tactic:
rw [Finset.Nontrivial, Finset.coe_range]

Goal state after:
n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ ∅ᶜ = univ

Tactic:
compl_empty

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ univ = univ
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ((sumPiEquivProdPi fun b ↦ α ↑((Finset.union s t h) b)).symm.trans (piCongrLeft (fun i ↦ α ↑i) (Finset.union s t h)))
      (f, g) ⟨i, hi'⟩ =
    f ⟨i, hi⟩

Tactic:
sumPiEquivProdPi,

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        (piCongrLeft (fun i ↦ α ↑i) (Finset.union s t h)))
      (f, g) ⟨i, hi'⟩ =
    f ⟨i, hi⟩
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
rw [← subtype_map, subtype_univ]

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ((sumPiEquivProdPi fun b ↦ α ↑((Finset.union s t h) b)).symm.trans (piCongrLeft (fun i ↦ α ↑i) (Finset.union s t h)))
      (f, g) ⟨i, hi'⟩ =
    g ⟨i, hi⟩

Tactic:
sumPiEquivProdPi,

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        (piCongrLeft (fun i ↦ α ↑i) (Finset.union s t h)))
      (f, g) ⟨i, hi'⟩ =
    g ⟨i, hi⟩
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ b ∈ t

pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
· obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi

Goal state after:
case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ (↑s).Subsingleton

Tactic:
rw [card_le_one_iff_subsingleton_coe, ← Set.subsingleton_coe, SetLike.coe_sort_coe]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
obtain h | h := p.le_or_gt i
  · rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]
  · rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
⊢ init (update q (last n) z) = init q

Tactic:
ext j
  simp [init, Fin.ne_of_lt]

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ f (a + 1) - (f 0 + 1) ≤ f (b + 1) - (f 0 + 1) ↔ a ≤ b

Tactic:
rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos

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

Goal state before:
pp: case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) → ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
rintro ⟨f, hf⟩
    have h : ∀ {i : ℕ}, i < l.length → f i < l'.length := by
      intro i hi
      specialize hf i
      rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
      obtain ⟨h, -⟩ := hf
      exact h
    refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩
    · simp
    · intro i
      apply Option.some_injective
      simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

Tactic:
rw [List.map_orderedInsert _ s, ih hl.2.2]

Goal state after:
case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ (cons a f ∘ rev) i = snoc (f ∘ rev) a i

Tactic:
exact cons_rev ..

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 α
⊢ List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (⇑e) l) ↔ List.Pairwise (fun x1 x2 ↦ x1 < x2) l

Tactic:
exact e.ltEmbedding.pairwise_listMap

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLE ↔ l.SortedGE

Tactic:
by
  grind [hf.le_iff_ge]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGE ↔ l.SortedLE

Tactic:
by
  grind [hf.le_iff_ge]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g k.succ

pp: case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc

Tactic:
contractNth_apply_of_gt

Goal state after:
case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ g k.succ = g k.succ

case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ ↑j < ↑k

case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
by
  classical
  exact Decidable.List.Lex.ne_iff H

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

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

Tactic:
rw [eq_comm, rotate_eq_singleton_iff, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩
  · rw [← image_uncurry_prod] at h
    exact h.of_image _
  · rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
    · exact hs.image2_left hb (hfs _ hb)
    · exact ht.image2_right ha (hft _ ha)

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
induction x using dense_induction s with

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hT : T.Nonempty
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₂, h₂⟩ := hT

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 1) * univ = univ

Tactic:
univ_pow n.succ_ne_zero,

Goal state after:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ * univ = univ
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Tactic:
rintro ⟨b, c, rfl, rfl, h⟩
    rw [singleton_mul_singleton, h, singleton_one]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
induction x using dense_induction s with

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ Disjoint H f.range ↔ H = ⊥

Tactic:
f.range_eq_top_of_surjective hf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ Disjoint H ⊤ ↔ H = ⊥
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
· by_cases h₂ : a₂ < b
    · simp [h₂, h]
    simp only [h₂, ↓reduceIte]
    apply Nat.add_lt_add_of_le_of_lt
    · exact Nat.mul_self_le_mul_self (not_lt.mp h₂)
    · exact Nat.lt_add_right _ h

Goal state after:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a + b₁ + a * a < b₂ * b₂ + a

Tactic:
Nat.add_comm _ a,

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a + b₁ + a * a < a + b₂ * b₂
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
h : ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
i j : α
ne : ((j⁻¹ * i) • s ∩ s).Nonempty
⊢ i = j

Tactic:
simpa [inv_mul_eq_one, eq_comm] using h _ ne

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
x✝ : WithBot ↑s
hmax : t.maximum = x✝
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
cases hmax : List.maximum t with

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsGLB (↑s) i ↔ IsLeast (↑s) i

Tactic:
by
  refine ⟨fun his => ?_, IsLeast.isGLB⟩
  suffices i = min' s hs by
    rw [this]
    exact isLeast_min' s hs
  rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his
  exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))

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

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [[]] ++ flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
List.singleton_append

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)

Tactic:
simp only [disjoint_iff, sup_inf_distrib_left, Finset.sup_eq_bot_iff]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ OrderDual.toDual (⨅ i ∈ s, f i) = OrderDual.toDual ((image f s).min' h')

Tactic:
toDual_min',

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ OrderDual.toDual (⨅ i ∈ s, f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅

Tactic:
by simp [eq_empty_iff_forall_notMem]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
x✝ : IsTop b ∧ a ⋖ b
hb : IsTop b
hab : a ⋖ b
⊢ Ioi a = {b}

Tactic:
cases b, hb using IsTop.rec; rwa [← Ioc_top, Ioc_eq_singleton_right_iff]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι

Tactic:
by
  rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]

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

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
simp_rw [map_eq_image, subset_image_iff, eq_comm]

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i

Tactic:
lift s to Finset ι using h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : (↑s).Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ ↑s) f i
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x

Tactic:
rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
h : 0 < a
x : ℕ
⊢ x ∈ Ico (a - 1) a ↔ x ∈ {a - 1}

Tactic:
rw [mem_Ico, mem_singleton]

Goal state after:
a : ℕ
h : 0 < a
x : ℕ
⊢ a - 1 ≤ x ∧ x < a ↔ x = a - 1
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n

Tactic:
Nat.lt_add_one_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mp
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a

Tactic:
rintro ⟨i, _, rfl⟩
    exact mod_lt i ha.bot_lt

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

Tactic:
refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
      rw [Nat.mul_add, mul_one, ← add_assoc, hn]

Goal state after: