mathlib-initiative/mathlib-tactics huggingface dataset:
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 (f '' ↑s)

Tactic:
by
  classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)

Tactic:
refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite

Tactic:
exact infinite_iUnion Subtype.coe_injective

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ g ↑t ≤ ⨆ i, g ↑i

Tactic:
refine le_ciSup_set ?_ t.prop

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ BddAbove (g '' f '' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
by
  by_cases hp : p <;>
  by_cases hq : q <;>
  simp [hp, hq]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂

Tactic:
by
  simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ i x, x ⩿ b i ∧ a = Function.update b i x

Tactic:
exact ⟨i, a i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ i x, x ⋖ b i ∧ a = Function.update b i x

Tactic:
exact ⟨i, a i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ y ≤ x → x ≤ y

Tactic:
rw [← f.le_iff_le, ← f.le_iff_le]
    exact h.le_of_le ⟨hy, mem_range_self y⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
by
  classical
    rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' a (b + 1 - a)), nodup := ⋯ } ↔ a ≤ x ∧ x ≤ b

Tactic:
Finset.mem_mk,

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ x ∈ ↑(List.range' a (b + 1 - a)) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' a (b - a)), nodup := ⋯ } ↔ a ≤ x ∧ x < b

Tactic:
Finset.mem_mk,

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ x ∈ ↑(List.range' a (b - a)) ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ } ↔ a < x ∧ x ≤ b

Tactic:
Finset.mem_mk,

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ x ∈ ↑(List.range' (a + 1) (b - a)) ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ } ↔ a < x ∧ x < b

Tactic:
Finset.mem_mk,

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ x ∈ ↑(List.range' (a + 1) (b - a - 1)) ↔ a < x ∧ x < b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n

Tactic:
simp_rw [Nat.lt_add_one_iff, biSup_le_eq_sup]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < (n + 1).succ), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n.succ), u (k + 1)

Tactic:
iSup_lt_succ'

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

Goal state before:
pp: a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
this : k = n
⊢ k = n + a

Tactic:
by contradiction

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (Subtype.val ⁻¹' t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩

Goal state after:
case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (Subtype.val ⁻¹' t).Nonempty
m : α
ms : m ∈ s
mt : ⟨m, ms⟩ ∈ Subtype.val ⁻¹' t
hm : ∀ x ∈ Subtype.val ⁻¹' t, ¬Subrel r (fun x ↦ x ∈ s) x ⟨m, ms⟩
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f (g m) i) (f (g n) i)
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
obtain ⟨g', hg'⟩ := ih (f ∘ g)

Goal state after:
case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f (g m) i) (f (g n) i)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i (((f ∘ ⇑g) ∘ ⇑g') a i) (((f ∘ ⇑g) ∘ ⇑g') b i)
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), x n ∈ s

pp: case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
· rintro ⟨⟨f, hf⟩⟩
    have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
    refine ⟨⟨f, ?_⟩, H⟩
    simpa only [H, and_true] using @hf

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Iio_subset_Iio h

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ioi a) = Ioi ↑a

Tactic:
by
  rw [subtype_Ioi_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop

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

Goal state before:
pp: N : Type u_7
inst✝ : CommMonoid N
H K : Submonoid N
⊢ ↑(H ⊔ K) = ↑H * ↑K

Tactic:
by
  ext x
  simp [mem_sup, Set.mem_mul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
cons_eq_insert,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = insert b (Ico a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
cons_eq_insert,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = insert a (Ioc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) ⋯

Tactic:
cons_eq_insert,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = insert b (Ioo a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
cons_eq_insert,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = insert a (Ioo a b)
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:
cons_eq_insert,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = insert a (Ioi a)
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:
cons_eq_insert,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = insert b (Iio b)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ a✝ * x✝ • b✝ = a✝ * b✝

Tactic:
hb

Goal state after:
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ a✝ * b✝ = a✝ * b✝
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : (fun m ↦ m • ↑b) g = ↑a
⊢ a ∈ orbit (↥H) b

Tactic:
dsimp at h

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ orbit (↥H) b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

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

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : (fun m ↦ m • ↑b) g = ↑a
⊢ a ∈ MulAction.orbit (↥H) b

Tactic:
dsimp at h

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ MulAction.orbit (↥H) b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ s.IsPWO

Tactic:
rw [IsPWO, partiallyWellOrderedOn_iff_exists_lt]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ ∀ (f : ℕ → Lex (α × β)), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
c : M
inst✝ : Mul M
h : IsMulCentral c
a b : M
⊢ a * b * c = a * c * b

Tactic:
by
  simp only [h.right_assoc, h.mid_assoc, (h.comm _).eq]

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'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f h * f g = f g * f h

Tactic:
← map_mul,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f (h * g) = f g * f h
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f (h * g) = f g * f h

Tactic:
← map_mul,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f (h * g) = f (g * h)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : g ∈ closure s
x : X
hx : x ∈ t
⊢ g • x ∈ t

Tactic:
induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
⊢ b ∈ s.erase a → Commute a b

Tactic:
hb

Goal state after:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
hb : b ∈ s.erase a
⊢ Commute a b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
M : Type u_7
inst✝ : CommMonoid M
f : ι → M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
nonempty : s.Nonempty
base : ∀ x ∈ s, p (f x)
⊢ Multiset.map (fun x ↦ f x) s.val ≠ ∅

Tactic:
simp [nonempty_iff_ne_empty.mp nonempty]

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

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s)

Tactic:
rw [sup_eq_eqvGen]; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
x : M → M → Prop
iseqv✝¹ : Equivalence x
mul'✝¹ :
  ∀ {w x_1 y z : M},
    { r := x, iseqv := iseqv✝¹ } w x_1 →
      { r := x, iseqv := iseqv✝¹ } y z → { r := x, iseqv := iseqv✝¹ } (w * y) (x_1 * z)
y : M → M → Prop
iseqv✝ : Equivalence y
mul'✝ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝ } w x → { r := y, iseqv := iseqv✝ } y_1 z → { r := y, iseqv := iseqv✝ } (w * y_1) (x * z)
h :
  (fun c ↦ ⇑c.toSetoid) { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } =
    (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝, mul' := mul'✝ }
⊢ { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } = { r := y, iseqv := iseqv✝, mul' := mul'✝ }

Tactic:
have : x = y := h

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
x : M → M → Prop
iseqv✝¹ : Equivalence x
mul'✝¹ :
  ∀ {w x_1 y z : M},
    { r := x, iseqv := iseqv✝¹ } w x_1 →
      { r := x, iseqv := iseqv✝¹ } y z → { r := x, iseqv := iseqv✝¹ } (w * y) (x_1 * z)
y : M → M → Prop
iseqv✝ : Equivalence y
mul'✝ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝ } w x → { r := y, iseqv := iseqv✝ } y_1 z → { r := y, iseqv := iseqv✝ } (w * y_1) (x * z)
h :
  (fun c ↦ ⇑c.toSetoid) { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } =
    (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝, mul' := mul'✝ }
this : x = y
⊢ { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } = { r := y, iseqv := iseqv✝, mul' := mul'✝ }
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]

Tactic:
subst L'

Goal state after:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ ↑(a * b) = ↑a

Tactic:
rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten

Tactic:
rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, g x = (map f) x

Tactic:
by
  rintro ⟨L⟩
  exact List.recOn L g.map_one fun ⟨x, b⟩ t (ih : g (FreeGroup.mk t) = map f (FreeGroup.mk t)) =>
    Bool.recOn b
      (show g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) =
          FreeGroup.map f ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) by
        simp [g.map_mul, g.map_inv, hg, ih])
      (show g (FreeGroup.of x * FreeGroup.mk t) =
          FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by simp [g.map_mul, hg, ih])

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

Goal state before:
pp: case calc_3
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
⊢ b ∈ {x ∈ t | g x ≠ 1} → ∃ a, ∃ (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ = b

Tactic:
hb

Goal state after:
case calc_3
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
⊢ ∃ a, ∃ (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ = b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
s : Multiset M
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s

Tactic:
by
  convert! prod_multiset_map_count s id
  rw [Multiset.map_id]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ IsMulCommutative (G ⧸ N) ↔ _root_.commutator G ≤ N

Tactic:
by
  refine ⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩
  · rw [commutator_eq_normalClosure, ← Subgroup.normalClosure_subset_iff]
    rintro x ⟨p, q, rfl⟩
    rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
    simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
    rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']
  · 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.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (map ⇑f) ((map ⇑f.symm) x) = x

Tactic:
by rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]

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

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
f : S.LocalizationMap N
j : N →* P
x✝ : N
⊢ j (f.toMonoidHom (f.sec x✝).1) = j (f.toMonoidHom ↑(f.sec x✝).2) * j x✝

Tactic:
← map_mul,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j : N →* P
x✝ : N
⊢ j (f.toMonoidHom (f.sec x✝).1) = j (f.toMonoidHom ↑(f.sec x✝).2 * x✝)
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
f : M → N
hf : S.IsLocalizationMap f
E : Type u_4
inst✝¹ : EquivLike E N P
inst✝ : MulEquivClass E N P
e✝ : E
y : P
e : N ≃* P := ↑e✝
x : M × ↥S
eq : e.symm y * f ↑x.2 = f x.1
⊢ e.symm (y * (⇑e✝ ∘ f) ↑x.2) = e.symm ((⇑e✝ ∘ f) x.1)

Tactic:
by simpa [e]

Goal state after: