mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ ↑k
n : ℤ
hn : n ∈ s
⊢ a ^ n ≤ a ^ ↑k

Tactic:
exact le_trans hn hk

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
⊢ R (f x) (f y)

Tactic:
rcases existsUnique_sub_zsmul_mem_Ioc ha y l with ⟨n, hny, -⟩
    rcases lt_trichotomy n 0 with hn | rfl | hn
    · -- Since `l ≤ x ≤ y`, the case `n < 0` is impossible
      refine absurd ?_ hxy.not_ge
      calc
        y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.1
    · -- If `n = 0`, then `l < y ≤ l + a`, hence we can apply the assumption
      exact hf x (Ico_subset_Icc_self hx) y (by simpa using Ioc_subset_Icc_self hny) hxy
    · -- In the remaining case `0 < n` we use transitivity.
      -- If `R = (· < ·)`, then the proof looks like
      -- `f x < f (l + a) ≤ f (l + n • a) < f y`
      trans f (l + (1 : ℤ) • a)
      · grind
      have hy : R (f (l + n • a)) (f y) := by
        rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
        refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1; simpa
      rw [← Int.add_one_le_iff, zero_add] at hn
      rcases hn.eq_or_lt with rfl | hn; · assumption
      trans f (l + n • a)
      · refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn
        simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]
        refine hR (k • b) (hf _ ?_ _ ?_ ?_) <;> simpa
      · assumption

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have ex : ∃ m : ℕ, y ≤ (m * δ) ^ n := by
    have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)
    refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]
    · exact (lt_add_of_pos_right _ <| by positivity).le.trans hm
    · exact (le_add_of_nonneg_left <| by positivity).trans hm

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs

Tactic:
· intro h
    rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
    · simp [*]
    · simp [*, cons_swap a b]

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

Goal state before:
pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i < (a :: l).length
⊢ (a :: l).erase (a :: l)[i] = (a :: l).eraseIdx i

Tactic:
| cons a l IH =>

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

Goal state before:
pp: α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f x s)

Tactic:
rw [foldl_swap]

Goal state after:
α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun x y ↦ f y x) x s)
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
| cons a l IH =>

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
⊢ n - t.card < n - s.card

Tactic:
decreasing_by have := (card_lt_card _h); lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∪ t + u = s + u ∪ (t + u)

Tactic:
by
  simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using
    show s + u - (t + u) = s - t by
      rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]

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

Goal state before:
pp: case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ ∀ (a : α), ¬a ∈ u

Tactic:
exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t

Tactic:
rw [and_iff_right_of_imp]

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t → u + s = u ∪ s
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndinter (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) a✝

Tactic:
rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ Disjoint (filter (fun x ↦ p x ∧ ¬q x) s) (filter (fun x ↦ q x ∧ ¬p x) s)

Tactic:
intro _ htp htq
  simp only [bot_eq_empty, subset_empty]
  by_contra! ⟨_, hx⟩
  exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
by
  classical
  obtain ⟨a, ha, b, hb, hab⟩ := hs
  have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
  refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase ha, *]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.attach = ∅ ↔ s = ∅

Tactic:
simp [eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
by
  simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]

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

Goal state before:
pp: k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ a = b

Tactic:
simpa [← val_eq_val] using hab

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

Tactic:
coe_int_sub_eq_ite

Goal state after:
n : ℕ
u v : Fin n
⊢ (if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n) = (↑↑u - ↑↑v) % ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:

Tactic:
#s = #(s.image f) := (card_image_of_injOn f_inj).symm
    _ ≤ #t := card_le_card <| image_subset_iff.2 hf

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

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ k, k ≤ b ∧ b = a + k

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h

Goal state after:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ ∃ k, k ≤ b ∧ b = a + k
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
cases n
  · lia
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h
  have hkb : k < b := by lia
  refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩
  simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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

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

Tactic:
card_le_one_iff_subsingleton_coe,

Goal state after:
α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ (↑s).Subsingleton
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∀ (n : ℕ), P (f n)

Tactic:
intro n

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)
Module: Mathlib.Data.Finset.Card

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

Tactic:
card_le_one_iff_subsingleton_coe,

Goal state after:
α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ Subsingleton ↑↑s
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = #s

Tactic:
rw [← card_ofFinset s H]

Goal state after:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
rw [duplicate_cons_iff_of_ne hx, IH]

Goal state after:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ image f^[i + 1] s ⊆ image f^[i] s

Tactic:
Function.iterate_succ,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ image (f^[i] ∘ f) s ⊆ image f^[i] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b) =
    if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b

Tactic:
split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl)

Goal state after:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b

case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton (insert a s) = insert a s

Tactic:
fold_insert has,

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ {a} ∪ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = insert a s
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' ≤ l
⊢ a :: l' ≤ a :: l

Tactic:
rw [le_iff_lt_or_eq] at h ⊢
  exact h.imp .cons (congr_arg _)

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

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → (length ∘ map fun x ↦ a + x) a_1 = a_1.length

Tactic:
intro s _

Goal state after:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
s : List ℕ
a✝ : s ∈ l.ranges
⊢ (length ∘ map fun x ↦ a + x) s = s.length
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)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
by
  have H : IsChain (flip (flip r)) l := h
  replace H := (isChain_reverse.mpr H).induction _ _ (fun _ _ h ↦ carries h)
  grind

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l')

pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
List.length_zipWith,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % min l.length l'.length) (zipWith f l l') ++ take (n % min l.length l'.length) (zipWith f l l') =
    drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l')

α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
Module: Mathlib.Data.List.Rotate

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

Tactic:
simp only [hn, or_false]
    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
    rw [← rotate_mod, h, rotate_mod]

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
h : ∀ (x : M), x ∈ s → x = 1
⊢ s.prod = 1

Tactic:
induction s using Quotient.inductionOn; simp [List.prod_eq_one h]

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

Goal state before:
pp: case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n

Tactic:
rotate_eq_drop_append_take (by simpa using h.le)

Goal state after:
case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = drop n (a :: l) ++ take n (a :: l)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n.choose n = 1

Tactic:
induction n <;> grind

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)

Tactic:
set p := n - 1

Goal state after:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)
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
has : ¬a ∈ s
⊢ ((a ::ₘ s).pi t).Nodup

Tactic:
have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2

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
hs : s.Nodup
⊢ ((a ::ₘ s).pi t).Nodup
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ {f | ∀ (i : ι), f i ∈ t i}.Finite

Tactic:
simpa [Set.pi] using Finite.pi ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ (∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ Surjective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
surjective_iff_surjective_of_iUnion_eq_univ hU

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
    ∀ (i : ι), Bijective ((U i).restrictPreimage f)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
ext; simp [mem_mul]; aesop

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✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ ∀ {a b : M}, a ∈ Set.ofPred IsUnit → b ∈ Set.ofPred IsUnit → a * b ∈ Set.ofPred IsUnit

Tactic:
intro a b ha hb
    rw [Set.mem_ofPred_eq] at *
    exact IsUnit.mul ha hb

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

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

Tactic:
rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    exact ⟨n + m, zpow_add x n m⟩

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

Goal state before:
pp: case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Tactic:
· rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
x : (i : ι) → M i
⊢ (x ∈ pi Set.univ fun i ↦ ⊥) ↔ x ∈ ⊥

Tactic:
by simp [mem_pi, funext_iff]

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ m + n ≤ pair m n

Tactic:
by
  simp only [pair, Nat.add_assoc]
  split_ifs
  · have := le_mul_self n
    lia
  · exact Nat.le_add_left _ _

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
x : (i : η) → f i
⊢ (x ∈ pi univ fun i ↦ ⊥) ↔ x ∈ ⊥

Tactic:
by simp [mem_pi, funext_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
by
  simp_rw [← hh]
  exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

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

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ min (map f l).prod (map g l).prod

Tactic:
rw [le_min_iff]

Goal state after:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod ∧ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
by
    cases x with | h x
    cases y with | h y
    simp only [Prod.Lex.toLex_lt_toLex] at h
    rcases h with (h | h)
    · obtain ⟨v, hv⟩ := exists_lt y.2
      use toLex (y.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]
    · obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * ((-(↑(m + 1) * 1) + ↑(m + 1) * ↑n) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑(m + 1) * ↑(n - 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
simp only [cond_eq_ite, beq_iff_eq]

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1