mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
rcases n with - | n
  · simp
  rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]

Goal state after:
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ OfScientific.ofScientific (↑a✝) false ↑n✝ = ↑(a✝ * 10 ^ n✝)

Tactic:
rw [NNRatCast.ofScientific_eq_ite, if_neg Bool.false_ne_true]
    norm_cast

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m : ℤ
hx : 2 * fract ↑m ≠ 1
hm : ↑(m + m) = 2 * ↑m
⊢ m = 2 * m / 2

Tactic:
Int.mul_ediv_cancel_left _ two_ne_zero

Goal state after:
case inl.inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m : ℤ
hx : 2 * fract ↑m ≠ 1
hm : ↑(m + m) = 2 * ↑m
⊢ m = m
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a * ↑n⌋ / ↑n = ⌊a⌋

Tactic:
mul_natCast_floor_div_cancel hn

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a⌋ = ⌊a⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a = 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
exact Or.inl ha

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
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x - ↑n) = f x - n • b

Tactic:
simpa using map_sub_nsmul f x n

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

Tactic:
suffices 0 < (1 - fract q) * q.den by
    rw [← sub_lt_iff_lt_add']
    simpa

Goal state after:
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den

Tactic:
rwa [right_distrib, one_mul] at this

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

Goal state before:
pp: case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ ∃ n, ↑x ≤ n • ↑y

Tactic:
simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

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

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ s + u = t + u ↔ s = t

Tactic:
by classical simp [Multiset.ext]

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

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ s + t = s + u ↔ t = u

Tactic:
by classical simp [Multiset.ext]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hstu : s + t = u
⊢ s = u - t

Tactic:
rw [← hstu, Multiset.add_sub_cancel_right]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
    exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ (a ::ₘ s.erase a) ∩ t

Tactic:
cons_inter_of_pos _ h₂

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case cons
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ motive (Finset.cons a { val := s, nodup := ⋯ } ⋯)

Tactic:
exact cons a _ _ (IH _)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∪ t \ s = t ∪ s \ t

Tactic:
by simp [union_comm]

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

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

Tactic:
congr!

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

Goal state before:
pp: case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ insert (k + 1) (range (k + 1)) \ {0} = image Nat.succ (insert k (range k))

Tactic:
image_insert,

Goal state after:
case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ insert (k + 1) (range (k + 1)) \ {0} = insert k.succ (image Nat.succ (range k))
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
h : Nonempty (Fin (n + 1) ↪ Fin m)
⊢ n + 1 ≤ m

Tactic:
obtain ⟨e⟩ := h
    rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
    refine Nat.succ_le_succ <| ihn ⟨?_⟩
    refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
    simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = #s

Tactic:
rw [insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card

Tactic:
simp only [H, Multiset.card_map, le_rfl]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = #s ↔ ∀ x ∈ s, p x

Tactic:
by
  rw [← (card_filter_le s p).ge_iff_eq, eq_iff_card_le_of_subset (filter_subset p s),
    filter_eq_self]

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

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n

Tactic:
rw [natCast_emod, Int.emod_eq_of_lt] <;> omega

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

Goal state before:
pp: case h
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
j : ℕ
hj : ∀ (m : ℕ), m < j → ∀ (hi : m < n), motive ⟨m, hi⟩
hi : j < n
⊢ motive ⟨j, hi⟩

Tactic:
exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)

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

Goal state before:
pp: case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

pp: case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
· intro H i
    exact H i.castSucc_lt_succ

Goal state after:
case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ a.succ.castPred ⋯ ≤ b ↔ a < b

Tactic:
castpred_succ_le_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ a < b ↔ a < b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ a.castLT ha - b.castLT ⋯ = (a - b).castLT ⋯

Tactic:
by
  rw [Fin.ext_iff]
  exact val_sub_castLT_of_le ha h

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

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
· rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }

Tactic:
congr!

Goal state after:
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 = card ↑p

Tactic:
congr!

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β

Tactic:
congr!

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

Goal state before:
pp: case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x

Tactic:
have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x

Goal state after:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) →
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
      exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: case inr
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this✝ : DecidableEq α := Classical.decEq α
this : ∀ ⦃m n : ℕ⦄, natEmbeddingAux α m = natEmbeddingAux α n → m ≤ n → m = n
hmlen : ¬m ≤ n
⊢ m = n

Tactic:
exact (this h.symm <| le_of_not_ge hmlen).symm

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ Fintype ↑{i | i ≤ n}

Tactic:
simpa [Nat.lt_succ_iff] using Set.fintypeLTNat (n + 1)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
l : List α
hl : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r l) = insertionSort s (map f l)

Tactic:
by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp_rw [List.forall_mem_cons, forall_and] at hl
    simp_rw [List.map, insertionSort_cons]
    rw [List.map_orderedInsert _ s, ih hl.2.2]
    · simpa only [mem_insertionSort] using hl.2.1
    · simpa only [mem_insertionSort] using hl.1.2

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
classical
  simp_rw [@and_comm ((_ : Set _) ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop

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

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)

Tactic:
congr!

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ (¬∃ m, m ≤ i ∧ p m) ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
not_exists,

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ (∀ (x : Fin n), ¬(x ≤ i ∧ p x)) ↔ ∀ (m : Fin n), m ≤ i → ¬p m
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (insert x xs)) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)

Tactic:
image_insert,

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (insert (g x) (image g xs)) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ (¬∃ m, m < i ∧ p m) ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
not_exists,

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ (∀ (x : Fin n), ¬(x < i ∧ p x)) ↔ ∀ (m : Fin n), m < i → ¬p m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ Fin.find p hᵢ = natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)

Tactic:
have hⱼ : ∃ j : Fin n, p (j.natAdd m) :=
    ⟨(Fin.cast (Nat.add_comm _ _) (Fin.find p hᵢ)).subNat _ hm, by simp [Fin.find_spec]⟩
  refine (find_eq_iff _).2 ⟨Fin.find_spec hⱼ, fun i hi ↦ ?_⟩
  cases i using addCases with | left i => _ | right i => _
  · exact Fin.find_min hᵢ (Fin.lt_def.mpr <| (Fin.castAdd_lt _ _).trans_le hm)
  · rw [Fin.natAdd_lt_natAdd_iff] at hi
    exact Fin.find_min hⱼ hi

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
by
    rw [← rotate'_mod,
        rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
    simp [rotate]

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ (map g1 S).prod ∣ (map g2 S).prod

Tactic:
apply Multiset.induction_on' S

Goal state after:
case h₁
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ (map g1 0).prod ∣ (map g2 0).prod

case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : M} {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : (a :: b :: L).head hL = (a :: b :: L).getLast hL
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'

Goal state after:
α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : a = (b :: L).getLast ⋯
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
by
    choose f hf using fun a => Quotient.exists_rep (t a)
    simpa [← funext hf] using List.Nodup.sigma

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

Goal state before:
pp: case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y

Tactic:
rintro ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, hne⟩

Goal state after:
case mpr
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne : ¬l[i] = l[j]
⊢ ∃ i_1 h j_1 h_1, ¬i_1 = j_1 ∧ l[i_1] = l[i] ∧ l[j_1] = l[j]
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t

Tactic:
by
  simpa using filter_product (fun _ : α => true) q

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 β
⊢ Finite (α ↪ β)

Tactic:
rcases isEmpty_or_nonempty (α ↪ β) with _ | h

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h✝ : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)

case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ ∀ (x y : α), ∃ g, g • x = y

Tactic:
intro x y
  use Equiv.swap x y
  simp

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : Submonoid M
s : Subsemigroup M
hs : 1 ∈ s.carrier
t : Subsemigroup M
ht : 1 ∈ t.carrier
⊢ { toSubsemigroup := s, one_mem' := hs }.toSubsemigroup = { toSubsemigroup := t, one_mem' := ht }.toSubsemigroup →
    { toSubsemigroup := s, one_mem' := hs } = { toSubsemigroup := t, one_mem' := ht }

Tactic:
congr!

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 ∈ {x | f x = g x}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ f 1 = g 1
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 α
⊢ s / t = s * t⁻¹

Tactic:
by
      rw [← image_id (s / t), ← image_inv_eq_inv]
      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
s : Set M
⊢ ↑(closure s) = {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
apply le_antisymm

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ⊆ {1} ∪ ↑(Subsemigroup.closure s)

case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = s * ⇑m '' ⇑m ⁻¹' t

Tactic:
image_preimage_eq_iff.2 ht,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = s * t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = s / ⇑m '' ⇑m ⁻¹' t

Tactic:
image_preimage_eq_iff.2 ht,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = s / t
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = y

Tactic:
eq_of_mem_singleton hy

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s \ {1}) = closure s

Tactic:
rw [← closure_union_one (s \ {1}), sdiff_union_self, closure_union_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ map f ⊤ = ⊤

Tactic:
eq_top_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ ⊤ ≤ map f ⊤
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
x✝ : ∃ y ∈ s, ∃ z ∈ t, y * z = x
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hp : y * z = x
⊢ z * (z⁻¹ * y * z) = x

Tactic:
by simp [mul_assoc, hp]

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

Goal state before:
pp: case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ {x | ∃ y, encode y = x}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ ∃ y, encode y = n
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 1 ≤ n / 2

Tactic:
rw [Nat.le_div_iff_mul_le]

Goal state after:
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

n : ℕ
h : 2 ≤ n
⊢ 0 < 2
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
· exact mul_mem ihx ihy

Goal state after:
case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Nonempty α
a : α
n : ℕ
⊢ (ofList (List.replicate n a)).length = n

Tactic:
by simp [length]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
b : FreeMonoid α
hb : (map f) b = of d
⊢ ∃ a, f a = d

Tactic:
induction b using FreeMonoid.inductionOn' with
    | one =>
      have H := congr_arg length hb
      simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
    | of_mul head _ _ =>
      simp only [map_mul, map_of] at hb
      use head
      have H := congr_arg length hb
      simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
      rw [H, mul_one] at hb
      exact FreeMonoid.of_injective hb

Goal state after: