mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})

Tactic:
convert! key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
cases i
  · simp
  · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
exact hs.pow.mul hs

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter <;> gcongr

Goal state after:
case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ s

case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t

Tactic:
by
  simp only [← image_prod, iUnion_prod_const, image_iUnion]

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 α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
simp_rw [← image_inv_eq_inv]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ (fun x ↦ x⁻¹) '' (s * t) = (fun x ↦ x⁻¹) '' t * (fun x ↦ x⁻¹) '' s
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g f.range = (g.comp f).range

Tactic:
rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
⊢ f.toHomUnits.ker = f.ker

Tactic:
ext x
  simp [mem_ker, Units.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ n, f (unpair n).1 (unpair n).2 = ⨆ i, ⨆ j, f i j

Tactic:
← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _),

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ n, f (unpair n).1 (unpair n).2 = ⨆ x, f x.1 x.2
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
h : ∃ x, p x
w : α
pw : p w
⊢ good p (decode (encode w))

Tactic:
simp [good, encodek, pw]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ x, comap (↑(MulAut.conj ((Equiv.inv G) x))) H

Tactic:
normalCore_eq_iInf_map_conj

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⨅ g, map (↑(MulAut.conj g)) H = ⨅ x, comap (↑(MulAut.conj ((Equiv.inv G) x))) H
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ g i✝

Tactic:
apply min_le_right

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 = c.1 ∧ t.2 ≤ c.2
⊢ (ofLex t).1 ≤ (ofLex c).1

Tactic:
exact h'.1.le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
⊢ idxOf m (hd :: tl) ≤ idxOf a (hd :: tl)

Tactic:
simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢
    cases h : argmax f tl
    · rw [h] at hm
      simp_all
    rw [h] at hm
    dsimp only at hm
    simp only [cond_eq_ite, beq_iff_eq]
    obtain ha | ha := ha <;> split_ifs at hm <;> injection hm with hm <;> subst hm
    · cases not_le_of_gt ‹_› ‹_›
    · rw [if_pos rfl]
    · rw [if_neg, if_neg]
      · exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
      · exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne
      · exact ne_of_apply_ne _ ‹f hd < f _›.ne
    · rw [if_pos rfl]
      exact Nat.zero_le _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toLeft = cons a u.toLeft ⋯

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toLeft = u.toLeft

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toRight = u.toRight

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toRight = cons b u.toRight ⋯

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toLeft = insert a u.toLeft

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toLeft = u.toLeft

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toRight = u.toRight

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toRight = insert b u.toRight

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
by
  induction s using Finset.eraseInduction with | _ s ih
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · exact empty
  · have H : s.max' hne ∈ s := max'_mem s hne
    rw [← insert_erase H]
    exact insert _ _ (fun x ↦ s.lt_max'_of_mem_erase_max' hne) (ih _ H)

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

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ sublistsLen 1 (a :: s) = map (fun x ↦ [x]) (a :: s).reverse

Tactic:
by
    rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]; rfl

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

Goal state before:
pp: case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ (a :: l₁✝).sublists' <+ (a :: l₂✝).sublists'

Tactic:
| cons_cons a _ ih =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ⊆ t

Tactic:
cons_subset_cons,

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
⊢ map Embedding.some s ⊆ map Embedding.some t ↔ s ⊆ t
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ (⋃ i, s i).Finite

Tactic:
by
  suffices ⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this
  refine iUnion_subset fun i x hx => ?_
  by_cases hi : i ∈ t
  · exact mem_biUnion hi hx
  · rw [he i hi, mem_empty_iff_false] at hx
    contradiction

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

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ x ∈ univ, g x) = ⨆ x ∈ univ, f (g x)

Tactic:
exact map_finite_biSup finite_univ f g

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
have h₂ b : BddAbove (Set.range fun c ↦ f (b, c)) := by
    rw [bddAbove_def] at hf ⊢
    obtain ⟨B, hB⟩ := hf
    exact ⟨B, by grind⟩

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ some ⁻¹' Iio ⊤ = univ

Tactic:
rw [← range_coe, preimage_range]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
simpa only [mem_range, exists_exists_eq_and] using! lt_csSup_iff hb (range_nonempty _)

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
rw [max_eq_right gt.le]

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = sSup ∅
Module: Mathlib.Order.Cover

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⩿ s

pp: case neg
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s

Tactic:
· convert! wcovBy_insert a _
    ext
    simp [ha]

Goal state after:
case neg
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithTop α
⊢ a ⋖ ⊤ ↔ ∃ b, IsMax b ∧ a = ↑b

Tactic:
by
  cases a with
  | coe a => simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]
  | top => simp [CovBy]

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

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

Tactic:
subset_image_iff,

Goal state after:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ (∃ s' ⊆ t, image (⇑f) s' = s) ↔ ∃ u ⊆ t, s = image (⇑f) u
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ s ∧ k ∉ s

Tactic:
rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]

Goal state after:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
a b x : α
⊢ x ∈ h₀_finset_Ico a b ↔ x ∈ h₁_finset_Ico a b

Tactic:
h₀_finset_mem_Ico,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
a b x : α
⊢ a ≤ x ∧ x < b ↔ x ∈ h₁_finset_Ico a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯ ⊆ cons ⊤ (Finset.map Embedding.coeWithTop t) ⋯ ↔ s ⊆ t

Tactic:
cons_subset_cons,

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
⊢ Finset.map Embedding.coeWithTop s ⊆ Finset.map Embedding.coeWithTop t ↔ s ⊆ t
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder ↑S := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → ↑S
h₁ : IsMin (a 0)
n : ℕ
h₂ : IsMax (a n)
e : ∀ i < n, a i ⋖ a (i + 1)
⊢ ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder ↑S := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → ↑S
n : ℕ
e : ∀ i < n, a i ⋖ a (i + 1)
h₁ : ↑(a 0) = ↑⊥
h₂ : ↑(a n) = ↑⊤
⊢ ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
Set.Icc_eq_empty_iff

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ¬a ≤ b ↔ ¬a ≤ b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → s.PartiallyWellOrderedOn r

Tactic:
rw [PartiallyWellOrderedOn, wellQuasiOrdered_iff_exists_monotone_subseq]

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) →
    ∀ (f : ℕ → { x // x ∈ s }), ∃ g, ∀ (m n : ℕ), m ≤ n → Subrel r (fun x ↦ x ∈ s) (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
rw [cons_eq_insert, Iio_insert]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set ↑s := {x | ↑x ≤ a}
h : t.Nonempty := Exists.intro ⟨a, ha⟩ le_rfl
⊢ ∃ b ≤ a, Minimal (fun x ↦ x ∈ s) b

Tactic:
refine ⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h,
    (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set ↑s := {x | ↑x ≤ a}
h : t.Nonempty := Exists.intro ⟨a, ha⟩ le_rfl
y : α
hy : (fun x ↦ x ∈ s) y
hle : y ≤ ↑(⋯.min t h)
⊢ ↑(⋯.min t h) ≤ y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

Tactic:
simpa only [Finset.sup_eq_iSup] using! s.wellFoundedOn_sup

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case e'_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
suffices hb : ↑b ∈ orbitRel.Quotient.orbit (⟦a⟧ : orbitRel.Quotient H x.orbit) by
    rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb
    rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
    convert! hb using 1
    rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]

Goal state after:
case e'_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ b ∈ orbit ⟦a⟧
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : center G = ⊤
⊢ ∀ (a b : G), a * b = b * a

Tactic:
rw [eq_top_iff'] at h

Goal state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ center G
__src✝ : Group G := inst✝
⊢ ∀ (a b : G), a * b = b * a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Tactic:
rw [iff_not_exists_isMinBadSeq List.length]

Goal state after:
case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ ¬∃ f,
      IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ Quot.mk (⇑(IsConj.setoid G)) g ∈ ConjClasses.mk '' ↑(Subgroup.center G)

Tactic:
refine ⟨g, ?_, rfl⟩

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ g ∈ ↑(Subgroup.center G)
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • ug • g = ug • a • g

Tactic:
smul_def,

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = ug • a • g
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = ug • a • g

Tactic:
smul_def,

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = ofConjAct ug * a • g * (ofConjAct ug)⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)

Tactic:
by
  rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
  exact subset_closure (mem_inv.mp hs)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)

Tactic:
convert! σ.prod_comp s (fun x => f x (σ.symm x)) hs

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
x✝ : ι
⊢ x✝ = (Equiv.symm σ) (σ x✝)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Tactic:
rw [← left_inv a1 h1, ← left_inv a2 h2]

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯