mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
⊢ (∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, (insert a r).sup id ≤ x

Tactic:
intro h
      have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
      -- x ∈ s is above the sup of r
      obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
      -- y ∈ s is above a
      obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
      -- z ∈ s is above x and y
      obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
      use z, hzs
      rw [sup_insert, id, sup_le_iff]
      exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some (eraseNone s) = s.erase none

Tactic:
by
  rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]

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

Goal state before:
pp: case insert.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s = ∅
⊢ max (f a) (s.sup f) ∈ f '' ↑(insert a s)

Tactic:
| inl hs =>

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ a ⊓ s.sup' hs f = s.sup' hs fun i ↦ f i ⊓ a

Tactic:
sup'_inf_distrib_left

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.sup' hs fun i ↦ a ⊓ f i) = s.sup' hs fun i ↦ f i ⊓ a
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 ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
Set.biUnion_eq_iUnion

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
⊢ ∃ i ∈ c, ↑s ⊆ f i
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case cons
ι : 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
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1

Tactic:
by_cases hji : f j ≤ f i

Goal state after:
case pos
ι : 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

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
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f a < f x ∧ f x ≤ f b ↔ a < x ∧ x ≤ b

Tactic:
f.lt_iff_lt,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ a < x ∧ f x ≤ f b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f a < f x ∧ f x < f b ↔ a < x ∧ x < b

Tactic:
f.lt_iff_lt,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ a < x ∧ f x < f b ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ ↑a ∈ insertTop s ↔ a ∈ s

Tactic:
simp [insertTop]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ⊤ ∈ insertTop s

Tactic:
simp [insertTop]

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

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

Tactic:
rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
      refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
      simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Set.Icc a b).Nonempty ↔ a ≤ b

Tactic:
Set.nonempty_Icc

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : α
m : M
h : a₂ ∈ orbit M a₁
⊢ m • a₂ ∈ orbit M a₁

Tactic:
obtain ⟨x, rfl⟩ := mem_orbit_iff.mp h
  simp [smul_smul]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
let := orbitRel G α
  set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
  refine
    ⟨fun h a a_in_U g g_in_V =>
      h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, ?_⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, ?_⟩
  · simp
  · intro h
    rw [Set.disjoint_left]
    rintro _ ⟨b, hb₁, hb₂⟩ ⟨c, hc₁, hc₂⟩
    obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)
    exact h b hb₁ g hc₁

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
m : ℕ
mn : m < n
⊢ ↑(fs n) m = g m

Tactic:
← h m n mn.le,

Goal state after:
case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
m : ℕ
mn : m < n
⊢ ↑(fs m) m = g m
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : Mᵐᵒᵖ), Commute (op x) a) ∧
      (∀ (b c : Mᵐᵒᵖ), op x * (b * c) = op x * b * c) ∧ ∀ (a b : Mᵐᵒᵖ), a * b * op x = a * (b * op x)) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)

Tactic:
MulOpposite.forall,

Goal state after:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), op x * (op a * op a_1) = op x * op a * op a_1) ∧
        ∀ (a a_1 : M), op a * op a_1 * op x = op a * (op a_1 * op x)) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
hx : x ∈ ⨅ g ∈ s, centralizer {g}
⊢ x ∈ centralizer s

Tactic:
simpa only [mem_iInf, mem_centralizer_singleton_iff, eq_comm (a := x * _)] using! hx

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
c : Con M
w x : M
x✝ : c w x
⊢ c (w ^ 0) (x ^ 0)

Tactic:
simpa using c.refl _

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

Goal state before:
pp: case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
· rintro Hyx Hyx' -
      exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

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

Goal state before:
pp: case tail
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)

Goal state after:
case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s with g i ∈ t, f (g i)

Tactic:
by
  calc
    _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
        prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2]
    _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
⊢ ∀ (a b : FreeGroup α),
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (a * b) =
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ a * Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ b

Tactic:
by rintro ⟨L₁⟩ ⟨L₂⟩; simp

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

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

Tactic:
simp [zpow_add, hx, hy]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
⊢ ∏ x ∈ s.attach, f x = ∏ x ∈ s.attach, extend Subtype.val f 1 ↑x

Tactic:
congr with ⟨x, hx⟩

Goal state after:
case e_f
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
x : ι
hx : x ∈ s
⊢ f ⟨x, hx⟩ = extend Subtype.val f 1 ↑⟨x, hx⟩
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : (leftRel N) a b
hcd : (leftRel N) c d
⊢ (leftRel N) (a * c) (b * d)

Tactic:
rw [leftRel_eq] at hab hcd ⊢

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (fun x y ↦ x⁻¹ * y ∈ N) (a * c) (b * d)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
this : Fintype ι
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

Tactic:
refine iSup_map_mulSingle_le.antisymm fun x hx => ?_

Goal state after:
ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi Set.univ P
⊢ x ∈ ⨆ i, map (MonoidHom.mulSingle M i) (P i)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ (closure ↑S).FG

Tactic:
rw [Submonoid.fg_iff]

Goal state after:
case mp
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ S_1.Finite
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_1
G : Type u_3
inst✝ : Group G
x✝ : FG G
S : Finset G
hS : Subgroup.closure ↑S = ⊤
⊢ Function.Surjective ⇑(FreeGroup.lift Subtype.val)

pp: case refine_2
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG G

Tactic:
· rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]

Goal state after:
case refine_2
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG G
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case pos
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
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
exact mem_closure_of_mem hy₃

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
⊢ ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Tactic:
rw [← sdiff_singleton_eq_erase]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
⊢ ∏ x ∈ s \ {a}, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
⊢ ⁅H₁, H₂⁆.Normal

Tactic:
by
  let base : Set G := { x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x }
  change (closure base).Normal
  suffices h_base : base = Group.conjugatesOfSet base by
    rw [h_base]
    exact Subgroup.normalClosure_normal
  refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_
  simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
  rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
  exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ≤ normalizer ↑⁅H₁, H₂⁆

Tactic:
by
  apply le_normalizer_closure_iff.mpr
  rintro g hg _ ⟨g₁, hg₁, g₂, hg₂, rfl⟩
  apply (mul_mem_cancel_right <| commutator_mem_commutator hg hg₂).mp
  rw [← commutatorElement_mul_left_eq_conj_mul g g₁ g₂]
  exact commutator_mem_commutator (mul_mem hg hg₁) hg₂

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) 1) x = x

Tactic:
one_def,

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) (of 1)) x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) x) 1 = x

Tactic:
one_def,

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) x) (of 1) = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ (lift fun x ↦ 1) ((fun n ↦ n • of default) n) = n

Tactic:
rw [map_zsmul, lift_apply_of]
    exact zsmul_one n

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ (s' * u') • r₃ = (r' * v) • r₁

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' • ↑u' • r₃ = r' • v • r₁
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑(s' * u') * ↑s₃ = r' * v * ↑s₁

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * (↑u' * ↑s₃) = r' * (v * ↑s₁)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
x : OreLocalization S X
⊢ liftExpand (P r₁ s₁) ⋯ x = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯ x

Tactic:
cases x with

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ liftExpand (P r₁ s₁) ⋯ (r₂ /ₒ s₂) = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
x : OreLocalization S X
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
⊢ smul'' r₁ s x = smul'' (r₂ • r₁) ⟨r₂ * ↑s, hs⟩ x

Tactic:
cases x with

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
⊢ smul'' r₁ s (x /ₒ s₂) = smul'' (r₂ • r₁) ⟨r₂ * ↑s, hs⟩ (x /ₒ s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
x : OreLocalization S X
⊢ 1 • x = x

Tactic:
cases x with

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ 1 • (r /ₒ s) = r /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 1 = x

Tactic:
cases x with

Goal state after:
case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 1 = r /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
x y : OreLocalization S R
z : OreLocalization S X
⊢ (x * y) • z = x • y • z

Tactic:
cases x with

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = (r₁ /ₒ s₁) • y • z
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
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
z : Q
⊢ ∃ a, (f.map hy k) a = z

Tactic:
by
  obtain ⟨y, ⟨t, ht⟩, rfl⟩ := k.mk'_surjective z
  obtain ⟨s, hs, rfl⟩ := surj ht
  obtain ⟨x, rfl⟩ := hg y
  use f.mk' x ⟨s, hs⟩
  rw [map_mk']

Goal state after:
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
f : S.LocalizationMap N
x : M
y : ↥S
z : N
⊢ f.mk' x y = z ↔ f x = z * f ↑y

Tactic:
rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]

Goal state after:
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
f : S.LocalizationMap N
a b : M
d : ↥S
⊢ f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b

Tactic:
rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]
  exact (map_units f d).mul_left_inj

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : Mul α
inst✝⁷ : Add α
inst✝⁶ : LE α
inst✝⁵ : Mul β
inst✝⁴ : Add β
inst✝³ : LE β
inst✝² : Mul γ
inst✝¹ : Add γ
inst✝ : LE γ
e : α ≃+*o β
⊢ ∀ {a b : β}, e.symm.toFun a ≤ e.symm.toFun b ↔ a ≤ b

Tactic:
simp [← e.map_le_map_iff']

Goal state after: