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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map (fun x ↦ f (inl x)) s.val + Multiset.map (fun x ↦ f (inr x)) t.val) =
    op (Multiset.fold op b₁ (Multiset.map (fun x ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun x ↦ f (inr x)) t.val))

Tactic:
fold_add

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
    rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).sublists = do
    let x ← l₂.sublists
    map (fun x_1 ↦ x_1 ++ x) l₁.sublists

Tactic:
simp only [sublists, foldr_append]

Goal state after:
α : Type u
l₁ l₂ : List α
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, g i
b : ι
hb : b ∈ ⋃ i ∈ s, g i
hab : a ≠ b
⊢ (Disjoint on f) a b

Tactic:
Set.mem_iUnion

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ i, ∃ (_ : i ∈ s), a ∈ g i
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
⊢ (Disjoint on f) a b
Module: Mathlib.Data.Finset.Powerset

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

Tactic:
rw [mem_ssubsets, ssubset_iff_subset_ne]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s : Finset β
p : β → Prop
inst✝ : DecidablePred p
f : (b : β) → p b → α
g : (b : β) → ¬p b → α
b : β
h₀ : b ∈ s
h₁ : p b
⊢ f b h₁ ≤ s.sup fun i ↦ if h : p i then f i h else g i h

Tactic:
by
  grind [le_sup_of_le]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s : Finset β
p : β → Prop
inst✝ : DecidablePred p
f : (b : β) → p b → α
g : (b : β) → ¬p b → α
b : β
h₀ : b ∈ s
h₁ : ¬p b
⊢ g b h₁ ≤ s.sup fun i ↦ if h : p i then f i h else g i h

Tactic:
by
  grind [le_sup_of_le]

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : ¬(fun x ↦ x.sup f) t < f a ⊔ t.sup f
⊢ f a ≤ t.sup f

Tactic:
rwa [right_lt_sup, not_not] at this

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

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

Tactic:
iSup

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ sSup (range fun h ↦ f h) = sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ⨆ b, ⨆ c, f (b, c) ≤ c

Tactic:
ciSup_le_iff h₁

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (i : β), ⨆ c, f (i, c) ≤ c
Module: Mathlib.Order.Interval.Set.WithBotTop

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

Tactic:
← preimage_coe_Ioc,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Ioc ↑a ↑b = Ioc ↑a ↑b
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:
by
  simp_rw [nonempty_iff_ne_empty, sigmaLift]
  split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ ¬Minimal P x ↔ ∃ y, y < x ∧ P y

Tactic:
simp_rw [not_minimal_iff hx, lt_iff_le_not_ge, and_comm]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
t : Set β
f : α → β
inst✝ : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
rw [← mapsTo_univ_iff] at hf
  obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht
  exact ⟨a, b, h⟩

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

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

Tactic:
by
  rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]

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:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < 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:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < 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:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < 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:
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]

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

Goal state before:
pp: a : ℕ
⊢ Ico 0 a = range a

Tactic:
← Nat.bot_eq_zero,

Goal state after:
a : ℕ
⊢ Ico ⊥ a = range a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ x ∈ Ioc a ⊤ ↔ a < x

Tactic:
by rw [mem_Ioc, and_iff_left le_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
a b x : α
⊢ a ≤ x ∧ x ≤ b ↔ x ∈ h₁_finset_Icc a b

Tactic:
h₁_finset_mem_Icc

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
a b x : α
⊢ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
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 : (s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

pp: case neg
α : 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 : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
· 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⟩

Goal state after:
case neg
α : 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 : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m ↦ m • a) g ∈ U
hab : f ((fun m ↦ m • a) g) = f a
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U

Tactic:
Set.mem_iUnion

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
hb : (fun m ↦ m • a) g ∈ U
hab : f ((fun m ↦ m • a) g) = f a
⊢ ∃ i, a ∈ (fun x ↦ i • x) '' U
Module: Mathlib.GroupTheory.GroupAction.Defs

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

Tactic:
Set.mem_iUnion

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

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ (s \ {a}).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
simp only [← wellFoundedOn_insert (a := a), insert_sdiff_singleton, mem_insert_iff, true_or,
    insert_eq_of_mem]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b

Tactic:
exact Set.eq_of_mem_uIcc_of_mem_uIcc

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
simp only [lt_iff_le_not_ge, not_and, not_not] at hxz

Goal state after:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x ≤ z → z ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ stabilizer G a ≤ stabilizer G (a • b)

Tactic:
simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]; rintro a h; rw [h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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
m n : ℕ
mn : m ≤ n
⊢ ↑(fs m) m = ↑(fs n) m

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn; clear mn
    induction k with
    | zero => rfl
    | succ k ih =>
      rw [ih, (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
        (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
      rfl

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ (orbitRel (ConjAct G) G) g h = IsConj g h

Tactic:
orbitRel_apply,

Goal state after:
G : Type u_3
inst✝ : Group G
g h : G
⊢ (g ∈ orbit (ConjAct G) h) = IsConj g h
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g k : G
⊢ k * g = g * k ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
exact Iff.symm mul_inv_eq_iff_eq_mul

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer ↑(closure s) = ⨅ g ∈ s, centralizer {g}

Tactic:
centralizer_closure,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer s = ⨅ g ∈ s, centralizer {g}
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:
by simpa using c.refl _

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
L : List (α × Bool)
⊢ Red (p :: L ++ L₁) (p :: L ++ L₂) ↔ Red L₁ L₂

Tactic:
simp [append_append_left_iff L, cons_cons_iff]

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

Goal state before:
pp: case mp
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
c : Con M
s t : { d // c ≤ d }
⊢ { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t →
    s ≤ t

Tactic:
intro h x y hs

Goal state after:
case mp
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
c : Con M
s t : { d // c ≤ d }
h :
  { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      s ≤
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      t
x y : M
hs : ↑s x y
⊢ ↑t x y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
⊢ (∏ a ∈ s with p a, if p a then f a else 1) = ∏ a ∈ s, if p a then f a else 1

Tactic:
refine prod_subset (filter_subset _ s) fun x hs h => ?_

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∉ {a ∈ s | p a}
⊢ (if p x then f x else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h₁ : a ∉ s → f a = 1
this✝ : DecidableEq ι
this : a ∉ s
b : ι
hb : b ∈ s
⊢ b ≠ a

Tactic:
by rintro rfl; exact this hb

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Function.Surjective ⇑(map f)

Tactic:
rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]

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'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤

Tactic:
exact Submonoid.monotone_map le_top

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
x : α
h : ∀ (f g : F) (x : α), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x
⊢ g x ≤ f x → f x⁻¹ ≤ g x⁻¹

Tactic:
by simpa using h g f x⁻¹

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x 1

Tactic:
rw [← mul_one 1]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk x (1 * 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝

Tactic:
rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤

Tactic:
exact coe_lt_top _

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤

Tactic:
exact coe_lt_top _

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
x : α
⊢ IsSuccPrelimit ↑x ↔ ↑x = ⊤ ∨ ∃ y, ↑x = ↑y ∧ IsSuccPrelimit y

Tactic:
simp [IsSuccPrelimit, WithTop.forall]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)

Tactic:
rcases le_total n m with h | h

Goal state after:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax (succ^[n] a)

case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)

Tactic:
by
  rcases le_total n m with h | h
  · exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)
  · rw [h_eq]
    exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

Goal state after:
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:
rw [mem_upperBounds] at IH hm

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.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑(n + 1) < x

Tactic:
rw [Nat.cast_add_one, ← add_assoc]
    exact hx.add_one_lt (hx.add_natCast_lt hy n)

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type v
inst✝ : Small.{w, v} α
x y : Shrink.{w, v} α
w : (equivShrink α).symm x = (equivShrink α).symm y
⊢ x = y

Tactic:
simpa using w

Goal state after:
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
⊢ Small.{u, w} β

Tactic:
by_cases hβ : Nonempty β
  · refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)
    obtain ⟨a, ha⟩ := h b
    exact ⟨a, by rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]⟩
  · simp only [not_nonempty_iff] at hβ
    infer_instance

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
c : α
hc : a < c
⊢ False

Tactic:
← coe_lt_coe,

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
c : α
hc : ↑a < ↑c
⊢ False
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
⊢ ∀ (a : PredOrder (WithTop α)), False

Tactic:
by
    intro
    cases h : pred (⊤ : WithTop α) with
    | top => exact hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a
    | coe a =>
      obtain ⟨c, hc⟩ := exists_gt a
      rw [← coe_lt_coe, ← h] at hc
      exact (le_pred_of_lt (coe_lt_top c)).not_gt hc

Goal state after: