mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
⊢ x ∈ ↑(closure (s \ t))

Tactic:
by_cases hxt : x ∈ t

Goal state after:
case pos
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∈ t
⊢ x ∈ ↑(closure (s \ t))

case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case pos
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∈ t
⊢ x ∈ ↑(closure (s \ t))

Tactic:
exact hts hxt

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
H✝ : Subgroup G
inst✝ : IsMulCommutative G
H : Subgroup G
⊢ ∀ (n : G), n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H

Tactic:
by simp [mul_comm']

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

Goal state before:
pp: M : Type u_6
inst✝ : CommGroup M
S : Subgroup M
n : ℕ
⊢ (map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range

Tactic:
by
  ext : 1
  simp [mem_subgroupOf]
  grind

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

Goal state before:
pp: motive : ℕ → Sort u
⊢ Function.Injective fun H n ↦ bitCasesOn n H

Tactic:
intro H₁

Goal state after:
motive : ℕ → Sort u
H₁ : (b : Bool) → (n : ℕ) → motive (bit b n)
⊢ ∀ ⦃a₂ : (b : Bool) → (n : ℕ) → motive (bit b n)⦄,
    (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) a₂ → H₁ = a₂
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ pair m n < (max m n + 1) ^ 2

Tactic:
simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]
  split_ifs <;> simp [Nat.le_of_lt, not_lt.1, *] <;> lia

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ closure (⇑↑(MulAut.conj g) '' s) = closure s

Tactic:
MonoidHom.coe_coe,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ closure (⇑(MulAut.conj g) '' s) = closure s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
· rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
    exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
xs : List M
x : M
h₁ : x ∈ xs
⊢ x ≤ xs.prod

Tactic:
induction xs with
  | nil => simp at h₁
  | cons y ys ih =>
    simp only [mem_cons] at h₁
    rcases h₁ with (rfl | h₁)
    · simp
    · specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

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

Goal state before:

Tactic:
f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)

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

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

Tactic:
induction s using Finset.eraseInduction with | _ s ihs

Goal state after:
case H
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
classical
  obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
  exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩

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

Goal state before:
pp: case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) (x✝ :: l₁✝) ~ powersetCardAux (n + 1) (x✝ :: l₂✝)

Tactic:
simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ∈ s.ssubsets

Tactic:
by
  rw [mem_ssubsets, ssubset_iff_subset_ne]
  exact ⟨empty_subset s, h.ne_empty.symm⟩

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup ↑(image f s)

Tactic:
← sup_id_eq_sSup,

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = (image f s).sup id
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r ≠ 0
hrs : r ≤ #s
⊢ (powersetCard r s).biUnion id = s

Tactic:
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r.succ ≠ 0
hrs : r.succ ≤ #s
⊢ (powersetCard r.succ s).biUnion id = s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ p (s.sup' H f)

Tactic:
change @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p ↑(s.sup' H f)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
· rw [iSup_of_empty', iSup_of_empty']

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ ⨆ (h : p), f h = sSup ∅

Tactic:
rw [iSup]
  congr
  rwa [range_eq_empty_iff, isEmpty_Prop]

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

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
· rw [iSup_of_empty', iSup_of_empty']

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Tactic:
ext
  simpa using le_ciInf_iff hf

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi ↑a ∩ range some = Ioo ↑a ⊤

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi ↑a ∩ Iio ⊤ = Ioo ↑a ⊤
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a ∩ range some = Ico ↑a ⊤

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a ∩ Iio ⊤ = Ico ↑a ⊤
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iio ↑a ∩ range some = Iio ↑a

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iio ↑a ∩ Iio ⊤ = Iio ↑a
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iic ↑a ∩ range some = Iic ↑a

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Iic ↑a ∩ Iio ⊤ = Iic ↑a
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Icc ↑a ↑b ∩ range some = Icc ↑a ↑b

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Icc ↑a ↑b ∩ Iio ⊤ = Icc ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico ↑a ↑b ∩ range some = Ico ↑a ↑b

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico ↑a ↑b ∩ Iio ⊤ = Ico ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioc ↑a ↑b ∩ range some = Ioc ↑a ↑b

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioc ↑a ↑b ∩ Iio ⊤ = Ioc ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioo ↑a ↑b ∩ range some = Ioo ↑a ↑b

Tactic:
range_coe,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioo ↑a ↑b ∩ Iio ⊤ = Ioo ↑a ↑b
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t : Finset ι
this : ∀ (st : Finset ι), BddAbove (Set.range fun x ↦ ⨆ (_ : x ∈ st), f x)
⊢ ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
by
    simp [ciSup_or', ciSup_sup_eq, this]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
have := hn.coe_sort

Goal state after:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
this : Nonempty ↑c
⊢ ∃ i ∈ c, ↑s ⊆ f i
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⋖ b ↔ a < b

Tactic:
unfold CovBy

Goal state after:
⊢ ∀ {a b : Bool}, (a < b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a < b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (ReflTransGen fun x1 x2 ↦ x1 ⩿ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
by
  rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Tactic:
exact mk_wcovBy_mk_iff_right.2 h

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : ¬f j ≤ f i
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1

Tactic:
exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ico a a = 0

Tactic:
by rw [Ico, Finset.Ico_self, Finset.empty_val]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico c b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableLT α
inst✝ : DecidableLE α
a b x : α
⊢ x ∈ (Set.Ico a b).toFinset ↔ a ≤ x ∧ x < b

Tactic:
by simp only [Set.mem_toFinset, Set.mem_Ico]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m} - n + n)

Tactic:
rw [Nat.sub_add_cancel hn]

Goal state after:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i % a = i

Tactic:
Nat.mod_eq_of_lt hia

Goal state after:
case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i = i
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inr.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i % a = i

Tactic:
Nat.mod_eq_of_lt hia

Goal state after:
case inr.mpr.inr.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i = i
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
by
  rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]

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

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
H : S
⊢ ↑H * ↑H = ↑H

Tactic:
aesop (add simp mem_mul)

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1 ∈ ↑S

Tactic:
exact S.one_mem'

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

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ g⁻¹ • a ∈ U

Tactic:
← hu₂

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ g⁻¹ • (fun x ↦ g • x) u ∈ U
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
b : α
left✝ : b ≤ a
hb : Minimal (fun x ↦ x ∈ s) b
⊢ ∃ a, Minimal (fun x ↦ x ∈ s) a

Tactic:
exact ⟨b, hb⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
exact subsingleton_of_subsingleton.partiallyWellOrderedOn

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

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
rw [eq_top_iff']

Goal state after:
G : Type u_2
inst✝ : CommGroup G
⊢ ∀ (x : G), x ∈ center G
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∏ x, f x = ∏ x ∈ m.toFinset, g x

Tactic:
refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, ↑a ∈ m.toFinset

case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ⟨a, ⋯⟩ ∈ univ

case refine_3
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : { x // x ∈ m }) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

case refine_4
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ↑⟨a, ⋯⟩ = a

case refine_5
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, f a = g ↑a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ j ∈ t, g j

Tactic:
classical
  exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
    prod_subset (image_subset_iff.2 hest) <| by simpa using h'

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ Con.liftOn 1 ⇑f ⋯ = 1

Tactic:
rw [← f.map_one]; rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case inv_of
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : α
hx : (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) (of x)) = of x
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) (of x)⁻¹) = (of x)⁻¹

Tactic:
| inv_of x hx =>

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
s : Multiset ι
M : Type u_5
inst✝ : CommMonoid M
f : ι → M
l : List ι
⊢ (Multiset.map f (Quot.mk (⇑(isSetoid ι)) l)).prod =
    ∏ m ∈ Multiset.toFinset (Quot.mk (⇑(isSetoid ι)) l), f m ^ Multiset.count m (Quot.mk (⇑(isSetoid ι)) l)

Tactic:
simp [prod_list_map_count l f]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
⊢ P.FG

Tactic:
by
  have hpwo := Set.isPWO_of_wellQuasiOrderedLE { x | x ∈ P ∧ x ≠ 1 }
  rw [fg_iff]
  refine ⟨_, ?_, (setOfPred_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOfPred_minimal_subset _))⟩
  ext x
  constructor
  · intro hx
    rw [← P.closure_eq]
    exact closure_mono ((setOfPred_minimal_subset _).trans fun _ => And.left) hx
  · intro hx₁
    by_cases hx₂ : x = 1
    · simp [hx₂]
    refine hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_
    simp only [Set.mem_ofPred_eq, and_imp] at ih
    by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y
    · exact mem_closure_of_mem hy₃
    rcases exists_lt_of_not_minimal ⟨hy₁, hy₂⟩ hy₃ with ⟨z, hz₁, hz₂, hz₃⟩
    rcases exists_mul_of_le hz₁.le with ⟨y, rfl⟩
    apply mul_mem
    · exact ih _ hz₂ hz₃ hz₁.le hz₁.not_ge
    apply ih
    · exact hP _ hz₂ _ hy₁
    · exact (one_lt_of_lt_mul_right hz₁).ne.symm
    · exact le_mul_self
    · rw [mul_le_iff_le_one_left']
      exact (one_lt_of_ne_one hz₃).not_ge

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'

Tactic:
· obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
    obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
    rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
      QuotientGroup.eq_one_iff]
    apply hGN
    rw [commutator_eq_closure]
    exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
m₁ m₂ : M
s₁ s₂ : ↥⊤
h : (r ⊤) (m₁, s₁) (m₂, s₂)
⊢ ⋯ ▸ mk ↑s₁ ⟨m₁, ⋯⟩ = mk ↑s₂ ⟨m₂, ⋯⟩

Tactic:
simpa [r_iff_exists, mk_eq_mk_iff, eq_comm, mul_comm] using h

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

Tactic:
rw [OreLocalization.expand' _ s t', OreLocalization.expand' _ s t']

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) /ₒ (t' * s) = t' • (r₁ * r' * r₂) /ₒ (t' * s)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₂ * ↑c.2 * (↑t₁ * (↑b.2 * a.1)) = ↑t₁ * ↑a.2 * (↑t₂ * (↑c.2 * b.1))

Tactic:
rw [ht₁]; ac_rfl

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case h.left
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * (r₃ * v)) • r₂ = (↑s₄ * r₃) • v • r₂

Tactic:
simp only [smul_smul, mul_assoc]

Goal state after: