mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ l.maximum = ↑(maximum_of_length_pos h)

Tactic:
simp only [coe_maximum_of_length_pos]

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Bot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
P : β → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this✝ : OrderBot { x // P x } := Subtype.orderBot Pbot
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ (SupHom.subtypeVal Psup).toFun ⊥ = ⊥

Tactic:
by simp [Subtype.coe_bot Pbot]

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this✝ : Lattice { x // P x } := Subtype.lattice Psup Pinf
this : BoundedOrder (Subtype P) := Subtype.boundedOrder Pbot Ptop
⊢ (LatticeHom.subtypeVal Psup Pinf).toFun ⊥ = ⊥

Tactic:
by simp [Subtype.coe_bot Pbot]

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

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists' ↔ s <+ t

Tactic:
induction t generalizing s with
  | nil =>
    simp only [sublists'_nil, mem_singleton]
    exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
  | cons a t IH => ?_

Goal state after:
case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ ↑s, i ≤ x) ∧ i ∈ upperBounds (lowerBounds ↑s)
⊢ i = s.min' hs

Tactic:
mem_upperBounds

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ ↑s, i ≤ x) ∧ ∀ x ∈ lowerBounds ↑s, x ≤ i
⊢ i = s.min' hs
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists' = map reverse l.sublists

Tactic:
simp only [sublists_eq_sublists', map_map, map_id'' reverse_reverse, Function.comp_def]

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

Goal state before:
pp: case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (a :: l₁✝).length (a :: l₂✝)

Tactic:
rw [length, sublistsLen_succ_cons]
    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

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

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ∈ t.powerset ↔ s ⊆ t

Tactic:
by
  cases s
  simp [powerset, mem_mk, mem_pmap, mk.injEq, exists_prop, exists_eq_right,
    ← val_le_iff]

Goal state after:
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:
simp [← Ioi_inter_Iio]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ioo ↑a ⊤ = Ioi a

Tactic:
simp [← Ioi_inter_Iio]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} \ {b} ⊆ {a}

Tactic:
sdiff_singleton_subset_iff,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} ⊆ {b, a}
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a ≤ b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a ≤ b

Tactic:
decide

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a < b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a < b

Tactic:
decide

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₂) ∧ (a, b₁) < (a, b₂) ↔ b₁ ⩿ b₂ ∧ b₁ < b₂

Tactic:
mk_wcovBy_mk_iff_right,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a : α
b₁ b₂ : β
⊢ b₁ ⩿ b₂ ∧ (a, b₁) < (a, b₂) ↔ b₁ ⩿ b₂ ∧ b₁ < b₂
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

pp: case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
· use ∅; simpa

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ⇑f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x}

Tactic:
convert! _root_.image_monotone_setOfPred_minimal (f := f) (by simp [f.le_iff_le])
  aesop

Goal state after:
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 + 1)

Tactic:
by
  simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
f : ℕ → α
m n : ℕ
h : m < n
hf : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨m, n, h, hf ▸ refl _⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.WellFoundedOn r ↔ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
by
  have f : RelEmbedding (Subrel r (· ∈ s)) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
    ⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩
  refine ⟨fun h => ?_, f.wellFounded⟩
  rw [WellFounded.wellFounded_iff_has_min]
  intro t ht
  by_cases hst : (s ∩ t).Nonempty
  · rw [← Subtype.preimage_coe_nonempty] at hst
    rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩
    exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩
  · rcases ht with ⟨m, mt⟩
    exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ici a ⊆ Ici b ↔ b ≤ a

Tactic:
by
  simp [← coe_subset]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioc ↑a ↑b
⊢ p x

Tactic:
mem_Ioc

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x ≤ ↑b
⊢ p x
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
obtain ⟨g, hgs | hgt⟩ := Nat.exists_subseq_of_forall_mem_union _ fun x ↦ (f x).2

Goal state after:
case inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), ↑(f (g n)) ∈ s
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
by
  simp [← coe_subset]

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:
by
  aesop (add simp mem_mul)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
intro hs f hf

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨φ, hφm, hφs⟩ := Nat.exists_strictMono_subsequence
    fun n ↦ (hf n).casesOn fun m h ↦ h.casesOn fun hs hmn ↦ Exists.intro m ⟨hmn, hs⟩

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : (fun b ↦ [[b, a]]) b = (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
by
  rw [Finset.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : ∀ (g : M), g * a = a * g
⊢ ∀ (g : M), g * ⅟a = ⅟a * g

Tactic:
exact (Commute.invOf_right <| ha ·)

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:
rw [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.refine_2
α : 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))).2 ≤ (f (g (g' 1))).2

Tactic:
exact hg' (Nat.zero_le 1)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
⊢ f b ≤ f c

Tactic:
have : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c :=
    Prod.Lex.toLex_le_toLex.mp hbc

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
this : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c
⊢ f b ≤ f c
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | x ∈ map (⇑f) s}.Pairwise Commute

Tactic:
simp only [Multiset.mem_map]

Goal state after:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | ∃ a ∈ s, f a = x}.Pairwise Commute
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ normalizer ↑(⨆ i, H i) = ⊤

Tactic:
eq_top_iff,

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ ⊤ ≤ normalizer ↑(⨆ i, H i)
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ f x = ∏ x ∈ t, x ^ f x

Tactic:
symm

Goal state after:
case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t, x ^ f x = ∏ x ∈ t ∪ u, x ^ f x
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ g x = ∏ x ∈ u, x ^ g x

Tactic:
symm

Goal state after:
case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ u, x ^ g x = ∏ x ∈ t ∪ u, x ^ g x
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝² : i ∈ ↑univ
j : ι
a✝¹ : j ∈ ↑univ
a✝ : i ≠ j
⊢ (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i)) i j

Tactic:
exact Pi.mulSingle_apply_commute x i j

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x) → x ∈ closure s

Tactic:
rintro ⟨n, t, hts, -, rfl⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Set M
n : M → ℕ
t : Finset M
hts : ↑t ⊆ s
⊢ ∏ a ∈ t, a ^ n a ∈ closure s
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
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 : ι
⊢ Pi.mulSingle i (x i) i = x i

Tactic:
simp only [Pi.mulSingle_eq_same]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x

Tactic:
disjoint_iff_inter_eq_empty.mp h

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case not
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : L₁✝ = [] ∧ (x✝ = x1 ∧ b✝ = !b1) ∧ (x✝ = x2 ∧ (!b✝) = b2) ∧ L₂✝ = []
⊢ False

Tactic:
rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩

Goal state after:
case not
α : Type u
L : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
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 i = ∏ i ∈ s with g i ∈ t, f i

Tactic:
by
  rw [← prod_disjiUnion, disjiUnion_filter_eq]
  #adaptation_note /-- 2025-09-12 (kmill) copied from private lemma pairwiseDisjoint_fibers -/
  intro x' hx y' hy hne
  simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁

Tactic:
by
  cases H; simp

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

Goal state before:
pp: α : Type u
a₁ : α
b₁ b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, b₂) :: L₁) L₂
⊢ (a₁, b₁).2 = ((a₁, b₁).1, b₂).2

Tactic:
symm

Goal state after:
α : Type u
a₁ : α
b₁ b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, b₂) :: L₁) L₂
⊢ ((a₁, b₁).1, b₂).2 = (a₁, b₁).2
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ (lift f).range = Subgroup.closure (Set.range f)

Tactic:
apply le_antisymm (range_lift_le Subgroup.subset_closure)

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Subgroup.closure (Set.range f) ≤ (lift f).range
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 ↔ x / y ∈ N

Tactic:
refine eq_comm.trans (QuotientGroup.eq.trans ?_)
  rw [nN.mem_comm_iff, div_eq_mul_inv]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ MonoidHom.mrange f = ⊤

Tactic:
MonoidHom.mrange_eq_top

Goal state after:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Function.Surjective ⇑f
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
inst✝⁵ : Monoid M✝
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
ι : Type u_5
inst✝² : Finite ι
M : ι → Type u_6
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), Monoid.FG (M i)
⊢ ⊤.FG

Tactic:
rw [← Submonoid.pi_top Set.univ]
    exact .pi fun i => Monoid.FG.fg_top

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ centralizer Set.univ

Tactic:
← Subgroup.coe_top,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ centralizer ↑⊤
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
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₀)
⊢ v₀ • r₂ /ₒ (u₀ * s₁) = v • r₂ /ₒ (u * s₁)

Tactic:
symm

Goal state after:
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 := ⋯
u₀ : ↥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₀)
⊢ v • r₂ /ₒ (u * s₁) = v₀ • r₂ /ₒ (u₀ * s₁)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ mk (↑a) a = 1

Tactic:
symm

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ 1 = mk (↑a) a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc • rb • r₃ /ₒ (sc * sa * s₁) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
symm

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂)) = rc • rb • r₃ /ₒ (sc * sa * s₁)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : m ∈ upperBounds S → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
mem_upperBounds

Goal state after:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∈ s
⊢ pred^[n] ⟨pred ↑⟨c, hc⟩, h⟩ = ⟨b, hb⟩

pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
· dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
b : WithTop α
h : ⊤ < b
⊢ ⊤ ≤
    match b with
    | none => ↑⊤
    | Option.some a => ↑(pred a)

Tactic:
exact (le_top.not_gt h).elim

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

Goal state before:
pp: n : ℕ∞
⊢ ↑⊤.toNat = ⊤ ↔ ⊤ ≠ ⊤

Tactic:
decide

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
⊢ a ∈ image List.ofFn univ

Tactic:
let hlen := Finset.mem_filter.mp ha

Goal state after:
α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ a ∈ image List.ofFn univ