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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f ∈ f '' ↑s

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Unique ι
s : ι → α
⊢ ⨆ i, s i = s default

Tactic:
have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
  simp only [this, ciSup_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : ConditionallyCompletePartialOrderSup β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']

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
a✝ : α
⊢ (a✝ ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sSup ∅}

Tactic:
simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]

Goal state after:
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
a✝ : α
⊢ ∀ (x : ι), (if x ∈ s then f x else sSup ∅) = a✝ → a✝ = sSup ∅ ∨ ∃ x ∈ s, f x = a✝
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, f a✝¹ j ⊓ ⨅ x ∈ s✝, f x j = (⨆ j, f a✝¹ j) ⊓ ⨆ j, ⨅ i ∈ s✝, f i j

Tactic:
exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

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

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

Tactic:
← preimage_coe_Icc,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Icc ↑a ↑b = Icc ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

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

Tactic:
← preimage_coe_Ioo,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Ioo ↑a ↑b = Ioo ↑a ↑b
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
rw [← hs.coe_toFinset, sUnion_eq_biUnion] at hsc
  have := DirectedOn.exists_mem_subset_of_finset_subset_biUnion hn hc hsc
  exact hs.coe_toFinset ▸ this

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 (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i

Tactic:
← ht

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⟩)
⊢ g ↑t ≤ ⨆ i, g ↑i
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)

Tactic:
rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_covBy_mk_iff_left.2 h
    · exact mk_covBy_mk_iff_right.2 h

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty, sigmaLift]

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
Module: Mathlib.Order.Minimal

Goal state before:
pp: case inl
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩

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

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

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

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 * (n / a)) % a = i

Tactic:
· lia

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

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 * (n / a)) % a = i
Module: Mathlib.Order.Interval.Finset.Nat

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

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 * (n / a)) % a = i

Tactic:
· lia

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 + a * (n / a)) % a = i
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case mp
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b

pp: case mpr
a b x : ℕ
⊢ a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x

Tactic:
· lia

Goal state after:
case mpr
a b x : ℕ
⊢ a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Tactic:
tfae_have 3 → 1 := by
    refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
    exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩

Goal state after:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
tfae_3_to_1 : {b | TransGen r b a}.WellFoundedOn r → Acc r a
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
⊢ Iic ⊤ = univ

Tactic:
by
  ext a; simp only [mem_Iic, le_top, mem_univ]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : BoundedOrder α
inst✝ : Fintype α
⊢ Icc ⊥ ⊤ = univ

Tactic:
Icc_bot,

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : BoundedOrder α
inst✝ : Fintype α
⊢ Iic ⊤ = univ
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 : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑((fun m ↦ m • b) g) ∈ orbit ↥H ↑b

Tactic:
exact MulAction.mem_orbit _ g

Goal state after:
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 : α
b : ↑(orbit G x)
g : ↥H
⊢ ↑g • b ∈ orbit (↥H) b

Tactic:
exact MulAction.mem_orbit _ g

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Tactic:
rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]

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 α
b : ↑x.orbit
g : ↥H
⊢ ↑g • b ∈ MulAction.orbit (↥H) b

Tactic:
exact MulAction.mem_orbit _ g

Goal state after:
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 : Quotient G α
b : ↑x.orbit
g : ↥H
⊢ ↑((fun m ↦ m • b) g) ∈ MulAction.orbit ↥H ↑b

Tactic:
exact MulAction.mem_orbit _ g

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer ⊆ S.centralizer

Tactic:
exact fun x hx y hy ↦ hx y <| Set.subset_centralizer_centralizer hy

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M

Tactic:
div_eq_mul_inv

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
g' : ℕ ↪o ℕ
hg' : Monotone fun n ↦ (ofLex f (g (g' n))).2
⊢ f (g (g' 0)) ≤ f (g (g' 1))

Tactic:
· refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩
      · exact (hhc (g' 0)).symm.trans (hhc (g' 1))
      · exact hg' (Nat.zero_le 1)

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
g : ↥H
⊢ 1 • g = g

Tactic:
by simp [HSMul.hSMul]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer ↑H)), r • 1 = 1

Tactic:
by simp [HSMul.hSMul]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer ↑H)) (x y : ↥H), r • (x * y) = r • x * r • y

Tactic:
by simp [HSMul.hSMul]

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

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 (hd :: tl) = (hd :: tl).prod

Tactic:
List.prod_cons,

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 (hd :: tl) = hd * tl.prod
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

Tactic:
refine
      closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x✝¹ : G
hx✝ : x✝¹ ∈ (closure S).toSubmonoid
x : G
x✝ : x ∈ closure S
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a

Tactic:
induction s using Quotient.inductionOn with | _ s
   =>  _ 

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
a : α
s : List α
comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a

Tactic:
List.prod_cons,

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd * tl.prod) = hd * tl.prod * a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
f : ι → M
inst✝¹ : CommMonoid M
inst✝ : IsEmpty ι
s : Finset ι
⊢ ∏ i ∈ s, f i = 1

Tactic:
rw [eq_empty_of_isEmpty s, prod_empty]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)

Tactic:
← h₂ _ hx,

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (g y)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι → M i

pp: case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i), (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = ?convert_3 x_1

pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd ?convert_3 ⋯ = x i

Tactic:
· intro j
    exact Pi.mulSingle j (x j) i

Goal state after:
case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i),
    (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i

case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ sInf (@r α '' s) x✝¹ x✝

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Goal state after:
α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ ∀ i ∈ s, i x✝¹ x✝
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
w✝ x✝ y✝ z✝ : M
h1 : f w✝ = f x✝
h2 : f y✝ = f z✝
⊢ f (w✝ * y✝) = f (x✝ * z✝)

Tactic:
rw [map_mul, h1, h2, map_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x * y⁻¹ ∈ N ↔ x / y ∈ N

Tactic:
div_eq_mul_inv

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x * y⁻¹ ∈ N ↔ x * y⁻¹ ∈ N
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
G' : Type u_5
inst✝ : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
rw [fg_iff_submonoid_fg] at *

Goal state after:
G : Type u_3
inst✝¹ : Group G
G' : Type u_5
inst✝ : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
rw [mul_le_iff_le_one_left']
      exact (one_lt_of_ne_one hz₃).not_ge

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (lift (⇑g ∘ f)) a = g ((lift f) a)

Tactic:
by
  rw [← AddMonoidHom.comp_apply g (lift f)]
  refine (lift_unique _ _ ?_).symm
  intro a
  change g ((lift f) (of a)) = g (f a)
  simp only [lift_apply_of]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= f >>= g = 0 >>= fun x ↦ f x >>= g

Tactic:
by iterate 3 rw [zero_bind]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ (map (fun i ↦ ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (map (fun i ↦ f i a) m).prod

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
⊢ x * of L2 * of L3 = x * (of L2 * of L3)

Tactic:
induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]

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
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
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * ↑s₂ ∈ S
⊢ P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩

Tactic:
have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂

Goal state after:
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
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * ↑s₂ ∈ S
this : P r₁ s₁ r₂ s₂ = P (1 • r₁) ⟨1 * ↑s₁, ⋯⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
⊢ P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ f (f.sec (f x)).1 = f (↑(f.sec (f x)).2 * x)

Tactic:
rw [sec_spec', map_mul]

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

Goal state before:
pp: case mpr
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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
⊢ z = w

Tactic:
obtain ⟨_, _⟩ := f.surj z

Goal state after:
case mpr
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
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝ : M × ↥S
h✝ : z * f ↑w✝.2 = f w✝.1
⊢ z = w
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
x : M
y : ↥S
⊢ (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
rw [map, lift_mk', mul_inv_left]

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
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k.toMonoidHom.comp g) x = (k.toMonoidHom.comp g) ↑y * k.mk' (g x) ⟨g ↑y, ⋯⟩
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 : M
b c : ↥S
⊢ a * ↑(b * c) = a * ↑c * ↑b

Tactic:
by rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
⊢ StrictMono fun x ↦ ↑a * x

Tactic:
rintro b c hbc

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
b c : WithTop α
hbc : b < c
⊢ (fun x ↦ ↑a * x) b < (fun x ↦ ↑a * x) c