mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
x✝¹ x✝ num✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(if true = true then NNRat.divNat x✝¹ (10 ^ x✝) else ↑(x✝¹ * 10 ^ x✝)) = ↑num✝ * ⅟↑denom✝

Tactic:
if_pos rfl

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
x✝¹ x✝ num✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
rcases em (2 * x ∈ range Int.cast) with ⟨m, hm⟩ | hx'
  · rw [← hm, ceil_intCast]
    rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩
    · obtain rfl : m = x := mul_left_cancel₀ two_ne_zero <| by simp [← hm, ← two_mul]
      rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]
    · refine absurd ?_ hx
      exact (mul_fract_eq_one_iff_exists_int one_lt_two).mpr ⟨m, mod_cast hm.symm⟩
  · rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr hx']

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:

Tactic:
|a - b|
    _ = a - b := abs_of_nonneg (sub_nonneg_of_le h0)
    _ < ⌊a⌋ + 1 - b := sub_lt_sub_right (lt_floor_add_one a) _
    _ ≤ ⌊a⌋ + 1 - ⌊b⌋ := sub_le_sub_left (floor_le b) _
    _ = 1 := by rw [h, add_sub_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
rw [ceil_eq_zero.mpr h.le, cast_zero]
    exact neg_lt_iff_pos_add.mp ha

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s

Tactic:
obtain ⟨y, rfl⟩ := hf x

Goal state after:
case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ a, map f a = s
y : α
⊢ ∃ a, map f a = f y ::ₘ s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a✝ : α
s t u : Multiset α
a : α
⊢ count a (s ⊔ t ⊓ u) = count a ((s ⊔ t) ⊓ (s ⊔ u))

Tactic:
simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union,
      Multiset.count_union, Multiset.inf_eq_inter]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup

Tactic:
by
  simp [Finset.ext_iff, perm_ext_iff_of_nodup (nodup_dedup _) (nodup_dedup _)]

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
⊢ u = ⊥

Tactic:
bot_eq_zero,

Goal state after:
case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u = 0
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
⊢ filter p (s - t) = filter p s - filter p t

Tactic:
by
  revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  rw [sub_cons, IH]
  by_cases h : p a
  · rw [filter_cons_of_pos _ h, sub_cons]
    congr
    by_cases m : a ∈ s
    · rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]
    · rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]
  · rw [filter_cons_of_neg _ h]
    by_cases m : a ∈ s
    · rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
        cons_erase m]
    · rw [erase_of_notMem m]

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = (map reverse (a :: l).reverse.tails).reverse

Tactic:
by simp [inits_eq_tails l, map_inj_left, ← map_reverse]

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

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬a_1 ∈ map (fun x ↦ a + x) m

Tactic:
intro x hxa hxb

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False

Tactic:
rw [range, mem_coe, List.mem_range] at hxa

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ (map g (map f s)).val = (map (f.trans g) s).val

Tactic:
simp only [map_val, Multiset.map_map]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
p : α → Prop
inst✝ : DecidablePred p
⊢ map f.toEmbedding (filter p s) = filter (p ∘ ⇑f.symm) (map f.toEmbedding s)

Tactic:
by
  simp only [filter_map, Function.comp_def, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).castSucc.rev = i.rev

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ i.rev = i.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
obtain h | h := (rev i).succ_le_or_le_castSucc p

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯) ≤ if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯

Tactic:
split_ifs with ha hb hb

Goal state after:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ a.pred ⋯ ≤ b.pred ⋯

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.pred ⋯ ≤ b.castPred ⋯

case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ a.castPred ⋯ ≤ b.pred ⋯

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.castPred ⋯ ≤ b.castPred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯) ≤ if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯

Tactic:
split_ifs with ha hb hb

Goal state after:
case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯

case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ i.castPred ⋯ ≤ i.pred ⋯

case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.castSucc = (i.succ.castPred ⋯).castSucc
⊢ i = j

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.castSucc = i.succ
⊢ i = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_1
α : 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
val✝ : α
property✝ : val✝ ∈ s
⊢ ∀ ⦃a₂ : ↥s⦄, (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩ = (fun a ↦ i ↑a ⋯) a₂ → ⟨val✝, property✝⟩ = a₂

Tactic:
⟨_, _⟩

Goal state after:
case calc_1
α : 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
val✝¹ : α
property✝¹ : val✝¹ ∈ s
val✝ : α
property✝ : val✝ ∈ s
⊢ (fun a ↦ i ↑a ⋯) ⟨val✝¹, property✝¹⟩ = (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩ → ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
⊢ i = (i.castPred hi).castSucc

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
⊢ i = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ (i.castPred hi).castSucc < j.castSucc ↔ i < j.castSucc

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i < j.castSucc ↔ i < j.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j.castSucc < (i.castPred hi).castSucc ↔ j.castSucc < i

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j.castSucc < i ↔ j.castSucc < i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ (i.castPred hi).castSucc ≤ j.castSucc ↔ i ≤ j.castSucc

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i ≤ j.castSucc ↔ i ≤ j.castSucc
Module: Mathlib.Data.Finset.Card

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

Tactic:
have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ Set.InjOn f ↑s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j.castSucc ≤ (i.castPred hi).castSucc ↔ j.castSucc ≤ i

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j.castSucc ≤ i ↔ j.castSucc ≤ i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ (i.castPred ⋯).castSucc = i

Tactic:
castSucc_castPred

Goal state after:
n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ i = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rcases i.le_or_gt (castSucc j) with (h | h)

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).castSucc.succAbove (b.castPred hb).castSucc = ((a.succAbove b).castPred hk).castSucc

Tactic:
castSucc_castPred

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove i.succ = i

Tactic:
predAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h),

Goal state after:
n : ℕ
p i : Fin n
h : p ≤ i
⊢ i.succ.pred ⋯ = i
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (Fin.cons x₀ xs 0 :: ofFn fun i ↦ Fin.cons x₀ xs i.succ).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
Fin.cons_succ,

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (Fin.cons x₀ xs 0 :: ofFn fun i ↦ xs i).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ b = (b.castPred ⋯).castSucc

Tactic:
castSucc_castPred

Goal state after:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ b = b
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ map { toFun := f, inj' := h } univ

Tactic:
by
        rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]

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

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x (i.addNat 1) = x i

Tactic:
Fin.addNat_one

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x i.succ = x i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))

Tactic:
simp [modNat, Nat.add_mod]

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.toFinset = s.toFinset

Tactic:
Subsingleton.elim h.fintype

Goal state after:
α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.toFinset = s.toFinset

α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ Fintype ↑s
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite

Tactic:
by
  rw [← range_subset_iff] at hf
  exact (infinite_range_of_injective hi).mono hf

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
⊢ ∀ (a b : α), (decide (r a b) || decide (r b a)) = true

Tactic:
by simpa using total_of r

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

Goal state before:
pp: n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯

Tactic:
simp_rw [find?_eq_dite, Option.get_dite]

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

Goal state before:
pp: m n : ℕ
p q : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
i j : Fin n
h : ∃ i, p i
⊢ decide (p h.choose) = true

Tactic:
by simp only [h.choose_spec, decide_true]

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
have hnl : n ≤ l.length := le_of_succ_le_succ h
    have hnl' : n ≤ (l ++ [a]).length := by
      rw [length_append, length_cons, List.length]; exact le_of_succ_le h
    rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take,
        drop_append_of_le_length hnl, take_append_of_le_length hnl]; simp

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

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

Tactic:
rintro ⟨_⟩ ⟨_⟩

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

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

Tactic:
rintro ⟨_⟩ ⟨_⟩

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

Tactic:
have : Acc (List.lex_chains r) l' := by
      rcases l with - | ⟨b, l⟩
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      /- l' is accessible by induction hypothesis -/
      · apply ih b (List.isChain_cons_cons.1 hl).1

Goal state after:
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) (a :: l)
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩
Module: Mathlib.Data.List.Chain

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

Tactic:
rintro ⟨_⟩ ⟨_⟩

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

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

Tactic:
| intro l _ ihl =>

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

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

Tactic:
by
  rw [isRotated_comm, isRotated_singleton_iff, eq_comm]

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.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)

Tactic:
by
  simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion]

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

Goal state before:
pp: case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun i ↦ fold op (b i) (t i)) (a ::ₘ ha))

Tactic:
| cons a ha ih =>

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

Goal state before:
pp: α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations

Tactic:
simpa using head_mem (cyclicPermutations_ne_nil l)

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ ↑(s ∩ t).offDiag = ↑(s.offDiag ∩ t.offDiag)

Tactic:
push_cast
    exact Set.offDiag_inter _ _

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
by
  rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ id '' (s / t) = s * (fun x ↦ x⁻¹) '' t

Tactic:
exact image_image2_distrib_right div_eq_mul_inv

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
by
  rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ (∃ x, x ∈ H ∧ ¬x ∈ K) → H ≤ L

Tactic:
← SetLike.coe_subset_coe

Goal state after:
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ (∃ x, x ∈ H ∧ ¬x ∈ K) → ↑H ⊆ ↑L
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ H ≠ ⊥

Tactic:
rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ x ∈ (normalizer ↑H).op ↔ x ∈ normalizer ↑H.op

Tactic:
mem_op,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ MulOpposite.unop x ∈ normalizer ↑H ↔ x ∈ normalizer ↑H.op
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ x ∈ mker f.mrangeRestrict ↔ x ∈ mker f

Tactic:
change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ ⟨f x, ⋯⟩ = ⟨1, ⋯⟩ ↔ f x = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalizer ↑H = ⊤ ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H

Tactic:
Subgroup.eq_top_iff',

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (x : G), x ∈ normalizer ↑H) ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H

Tactic:
exact h (c * b)

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < (a :: b :: l).prod

Tactic:
List.prod_cons

Goal state after:
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < a * (b :: l).prod
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
exact Or.inr (Lex.right _ _ hba)

Goal state after: