mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ a ::ₘ filter p s = {a} + filter p s

Tactic:
singleton_add

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ a ::ₘ filter p s = a ::ₘ filter p s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0

Tactic:
by
  split_ifs with h
  · exact count_filter_of_pos h
  · exact count_filter_of_neg h

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

Goal state before:
pp: n : ℕ
⊢ {n} + ↑(List.range n) = n ::ₘ ↑(List.range n)

Tactic:
singleton_add

Goal state after:
n : ℕ
⊢ n ::ₘ ↑(List.range n) = n ::ₘ ↑(List.range n)
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), x ∉ {a} ∩ s

Tactic:
simp only [mem_inter, mem_singleton]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
x : α
hx : x ∈ s
⊢ f x = a✝ ↔ g x = a✝

Tactic:
rw [h hx]

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : 2 < n
⊢ ∃ k, k ≠ i ∧ k ≠ j

Tactic:
have : NeZero n := ⟨by lia⟩

Goal state after:
n : ℕ
i j : Fin n
h : 2 < n
this : NeZero n
⊢ ∃ k, k ≠ i ∧ k ≠ j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ succ 0 = 1

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1

Tactic:
· exact (NeZero.ne 0 rfl).elim

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ succ 1 = 2

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2

Tactic:
· exact (NeZero.ne 0 rfl).elim

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i ↦ (a :: l).get i.succ) = l

Tactic:
exact ofFn_get l

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

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

Tactic:
exact Fin.ne_of_gt h

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = 0 ↔ b = 0

Tactic:
rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
i : Fin n
h : Function.Injective f
⊢ find? p (ofFn f) = some (f i) ↔ p (f i) = true ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true

Tactic:
by
  simp only [find?_ofFn_eq_some, h.eq_iff, Bool.not_eq_true, exists_eq_left]

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ count a (finRange n) = 1

Tactic:
by
  simp [List.Nodup.count (nodup_finRange n)]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}

Tactic:
exact card_le_card hx

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m

Tactic:
rw [hv, Nat.add_zero]

Goal state after:
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)
⊢ append as (snoc bs b) ⟨i, isLt⟩ = snoc (append as bs) b ⟨i, isLt⟩

Tactic:
simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
    eq_rec_constant, Nat.add_eq]

Goal state after:
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
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ #s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
← Fintype.card_coe

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s
Module: Mathlib.Data.Fintype.EquivFin

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

Tactic:
have hmn : m < n := lt_of_le_of_ne hmlen hmn

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).castPred H₁) = p j

Tactic:
revert H₂

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
⊢ ∀ (H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j), H₂ ▸ p ((i.succAbove j).castPred H₁) = p j
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
⊢ orderedInsert r a l = takeWhile (fun b ↦ decide ¬r a b) l ++ a :: dropWhile (fun b ↦ decide ¬r a b) l

Tactic:
by
  induction l <;> grind [takeWhile, dropWhile]

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

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).pred H₁) = p j

Tactic:
revert H₂

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
⊢ ∀ (H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j), H₂ ▸ p ((i.succAbove j).pred H₁) = p j
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
⊢ ¬Fin.find p h ≤ i ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
find_le_iff,

Goal state after:
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
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ Fin.find p h ∈ find? fun b ↦ decide (p b)

Tactic:
grind [find?_eq_dite]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
⊢ R (l.get a) (l.get b)

Tactic:
obtain rfl | hlt := Fin.eq_or_lt_of_le hab; exacts [refl _, (pairwise_iff_get.1 h) _ _ hlt]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

Tactic:
· rcases h with (_ | h | h)
      · exact Or.inl h
      · exact Or.inr ⟨rfl, h⟩

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝

Tactic:
· simp_all [rotate']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
h : (↑s).PairwiseDisjoint t
⊢ ↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)

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

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

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l

Tactic:
by
  obtain ⟨n, rfl⟩ := h
  rcases l with - | ⟨hd, tl⟩
  · exists 0
  · use (hd :: tl).length * n - n
    rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
    exact Nat.le_mul_of_pos_left _ (by simp)

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

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k)! = (n - k) * (n - k.succ)!

Tactic:
← succ_sub_succ,

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n.succ - k.succ)! = (n.succ - k.succ) * (n - k.succ)!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + 1 * n ! + n * n ! - k * n ! = (n + 1) * n !

Tactic:
Nat.add_assoc,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + (1 * n ! + n * n !) - k * n ! = (n + 1) * n !
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)

Tactic:
exact hf _ _

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

Goal state before:
pp: case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n - k)

Tactic:
← succ_sub_succ,

Goal state after:
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (k + 1) + n.choose k.succ * (n.succ - k.succ)
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ 1 • x✝ = x✝

Tactic:
by simpa [(· • ·)] using one_smul ..

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Tactic:
rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]

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

Goal state before:
pp: case h₁
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k ⊆ v i

pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
· simp [iInter_subset]

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ s.seq t = ⋃ f ∈ s, f '' t

Tactic:
rw [seq_eq_image2, iUnion_image_left]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x ↦ x⁻¹ * a) ⁻¹' {b} = {a / b}

Tactic:
rw [← image_div_left, image_singleton]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
⊢ x ∈ iSup K ↔ ∃ i, x ∈ K i

Tactic:
have : iSup K = ⨆ i : PLift ι, ⨆ (_ : True), K i.down := by simp [iSup_plift_down]
  rw [this, mem_biSup_of_directedOn trivial]
  · simp
  · simp only [ofPred_true]
    rw [directedOn_onFun_iff, Set.image_univ, directedOn_range]
    -- `Directed.mono_comp` and much of the Set API requires `Type u` instead of `Sort u`
    intro i
    simp only [PLift.exists]
    intro j
    refine (hK i.down j.down).imp ?_
    simp
  · exact PLift.up hι.some

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
hxy : x * y = 1
hx1 : x = 1 := h hx (Subgroup.inv_mem H₂ hy) (eq_inv_iff_mul_eq_one.mpr hxy)
⊢ y = 1

Tactic:
simpa [hx1] using hxy

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

Goal state before:
pp: case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
simp only [h, ↓reduceIte, gt_iff_lt, s]

Goal state after:
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
simp only [h, ↓reduceIte, gt_iff_lt, s]

Goal state after:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Subgroup.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

Goal state after:
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 < a + b₂ * b₂

Tactic:
Nat.add_assoc,

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.Data.Nat.Pairing

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ m * m + n ≤ m * m + m + n

Tactic:
Nat.add_assoc,

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ m * m + n ≤ m * m + (m + n)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)

Tactic:
gcongr <;> apply smul_set_subset_mul <;> simpa

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
by
  constructor
  · rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩
  · obtain ⟨i, a⟩ := a
    dsimp only
    rintro (h | ⟨rfl, h⟩)
    · exact Lex.left _ _ h
    · exact Lex.right _ h

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ closure s = mrange (FreeMonoid.lift Subtype.val)

Tactic:
by
  rw [FreeMonoid.mrange_lift, Subtype.range_coe]

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

Goal state before:
pp: case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
rw [hf, Option.mem_def] at ho

Goal state after:
case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : (Option.casesOn (some c) (some a) fun c ↦ if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ m.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ m → a.Nodup

Tactic:
induction m using Multiset.induction_on with
  | empty => simp
  | cons _ _ h => simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun x ↦ f (inl x)) s) (fold op b₂ (fun x ↦ f (inr x)) t)

Tactic:
by
  simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ s.min = ⊤ ↔ s = ∅

Tactic:
by
  simp [Finset.min, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Multiset α
⊢ ∀ (a : List α), (powersetCard n ⟦a⟧).card = (card ⟦a⟧).choose n

Tactic:
by simp [powersetCard_coe]

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

Goal state before:
pp: case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
sublists_concat,

Goal state after:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    (l'.sublists ++ map (fun x ↦ x ++ [a]) l'.sublists).zip (l'.sublists ++ map (fun x ↦ x ++ [a]) l'.sublists).reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse
⊢ l₁ ++ l₂ ~ a :: l

Tactic:
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *

Goal state after:
case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id (cons a)) (l.sublists'.zip l.sublists'.reverse) ++
      map (Prod.map (cons a) id) (l.sublists'.zip l.sublists'.reverse)
⊢ l₁ ++ l₂ ~ a :: l

case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (image f s).max' ⋯ ∈ image f s

Tactic:
exact max'_mem (image f s) _

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

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
have : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
mem_sigmaLift

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
mem_sigmaLift

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b

Tactic:
mem_sigmaLift

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
⊢ s.Finite

Tactic:
by_contra! hi
  obtain ⟨m, n, hmn, h⟩ := hp (hi.natEmbedding _)
  exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) ⋯

Tactic:
rw [cons_eq_insert, Ioi_insert]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }

Tactic:
refine Nat.rec ?_ fun n fn => ?_
    · exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩
    · exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1,
        (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer ↑H)
h : G
hh : h ∈ ↑H
⊢ ϕ (h * g) = ϕ (g * h)

Tactic:
rw [map_mul, map_mul]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer ↑H)
h : G
hh : h ∈ ↑H
⊢ ϕ h * ϕ g = ϕ g * ϕ h