mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ f head = d

Tactic:
have H := congr_arg length hb

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (of (f head) * (map f) a✝¹).length = (of d).length
⊢ f head = d
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mpr.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ ∃ a, (map f) a = 1

Tactic:
use 1; rfl

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
⊢ [].prod ≤ [].prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
h₁ : ∀ (i : ι), i ∈ [] → f i ≤ g i
h₂ : ∃ i, i ∈ [] ∧ f i < g i
⊢ (map f []).prod < (map g []).prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ [].prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x : M
h₁ : x ∈ []
⊢ x ≤ [].prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
hpl : ∀ (a : α), a ∈ [] → p a
⊢ f [].prod ≤ (map f []).prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
hl_nonempty : [] ≠ []
hl : ∀ (a : α), a ∈ [] → p a
⊢ f [].prod ≤ (map f []).prod

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f [].sum ≤ foldr max 0 (map f [])

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f [].prod ≤ (map f []).sum

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
hd : α
tl : List α
IH : f tl.prod ≤ (map f tl).sum
⊢ f hd + f tl.prod ≤ (map f (hd :: tl)).sum

Tactic:
IH

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
hd : α
tl : List α
IH : f tl.prod ≤ (map f tl).sum
⊢ f hd + (map f tl).sum ≤ (map f (hd :: tl)).sum
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inl.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inl ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩

pp: case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

pp: case inr.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩

Tactic:
· simpa using h.ne_of_mem ha hb

Goal state after:
case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

case inr.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ Injective fun x ↦ ↑x.snd

Tactic:
rintro ⟨i, x, hx⟩ ⟨j, -, hx'⟩ rfl

Goal state after:
α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
x : α
hx : x ∈ s i
j : ι
hx' : (fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩ ∈ s j
⊢ ⟨i, ⟨x, hx⟩⟩ = ⟨j, ⟨(fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩, hx'⟩⟩
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ [] → m ∈ foldl (argAux r) o [] → ¬r a m

Tactic:
| nil =>

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

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a} ⊔ closure {b} ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
mem_sup

Goal state after:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
⊢ ([] ++ l₂).maximum = max [].maximum l₂.maximum

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ [] → ↑a ≤ b
⊢ [].maximum ≤ b

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : [] ≠ []
⊢ ↑(foldr max ⊥ []) = [].maximum

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a : α
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max b []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)

Tactic:
exact .symm <| apply_sup'_eq_sup'_comp _ _ fun _ _ ↦ hf.map_max

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

Goal state before:
pp: case nil
α : Type u
s : List α
⊢ s ∈ [].sublists' ↔ s <+ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
l₁ l₂ : List α
⊢ powersetAux' [] ~ powersetAux' []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
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₂)
      [] =
    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) [[]] [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
⊢ [].reverse.sublists = map reverse [].sublists'

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ sublistsLen 1 (a :: s) = map (fun x ↦ [x]) (a :: s).reverse

Tactic:
rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]; rfl

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

Goal state before:
pp: case succ.nil
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
⊢ powersetCardAux (n + 1) [] ~ powersetCardAux (n + 1) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists'.zip [].sublists'.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
⊢ ∀ x_1 ∈ s, y ∈ x_1 → x ≠ y → r x y

Tactic:
T

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
⊢ T ∈ s → y ∈ T → x ≠ y → r x y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
⊢ flatMap (fun n ↦ sublistsLen n []) (range ([].length + 1)) ~ [].sublists'

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u
l : List α
⊢ flatMap (fun n ↦ sublistsLen n l) (range (l.length + 1)) ~ l.sublists'

Tactic:
by
  induction l with
  | nil => simp [range_succ]
  | cons h tl l_ih =>
    simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
    refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
    simp_rw [← List.map_flatMap, ← cons_append]
    rw [← List.singleton_append, ← List.sublistsLen_zero tl]
    refine Perm.append ?_ (l_ih.map _)
    rw [List.range_succ, flatMap_append, flatMap_singleton,
      sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
      ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
      ← flatMap_cons (f := fun n => sublistsLen n tl), ← range_succ_eq_map]
    exact l_ih

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite
⊢ ∀ i ∉ {i | (s i).Nonempty}, s i = ∅

Tactic:
simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.sup' hs id = sSup ↑s

Tactic:
by
  rw [sup'_eq_csSup_image s hs, Set.image_id]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
by
  by_cases! hf : ¬BddAbove (range f)
  · rw [ciSup_of_not_bddAbove hf, ciSup_of_not_bddAbove <| mt bbdAbove_range_left_of_sup hf]
    exact le_sup_left
  by_cases! hg : ¬BddAbove (range g)
  · rw [ciSup_of_not_bddAbove hg, ciSup_of_not_bddAbove <| mt bbdAbove_range_right_of_sup hg]
    exact le_sup_right
  exact ciSup_sup_eq hf hg |>.le

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x

Tactic:
by
  simpa using! _root_.iSup_insert

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ InjOn f (f ⁻¹' ↑∅)

Tactic:
by simp [InjOn]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : WithTop α
⊢ ¬a ⋖ ⊤

Tactic:
simp [covBy_top_iff]

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

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

Tactic:
by
  rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_sdiff_Ico_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    a ≤ x ∧ x ≤ b

Tactic:
by
    cases a <;> cases b <;> cases x <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    a ≤ x ∧ x < b

Tactic:
by
    cases a <;> cases b <;> cases x <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    a < x ∧ x ≤ b

Tactic:
by
    cases a <;> cases b <;> cases x <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a b x : WithTop α
⊢ (x ∈
      match a, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    a < x ∧ x < b

Tactic:
by
    cases a <;> cases b <;> cases x <;> simp

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x : N
hx : x ∈ s
⊢ (fun x ↦ r • x) x = r ^ 1 • x

Tactic:
pow_one

Goal state after:
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x : N
hx : x ∈ s
⊢ (fun x ↦ r • x) x = r • x
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
rintro ⟨g⟩ hg

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ Quot.mk (⇑(IsConj.setoid G)) g ∈ ConjClasses.mk '' ↑(Subgroup.center G)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a : N), Commute (e x) a

Tactic:
intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (b c : N), e x * (b * c) = e x * b * c

Tactic:
intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)

Tactic:
intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

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

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g = a⁻¹ * g * a
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : ConjAct.ofConjAct ↑u * x * (ConjAct.ofConjAct ↑u)⁻¹ = x
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : ConjAct.ofConjAct ↑u * x = x * ConjAct.ofConjAct ↑u
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
x✝¹ : G
x✝ : x✝¹ ∈ s
⊢ x✝¹ * g = g * x✝¹ ↔ g * x✝¹ * g⁻¹ * x✝¹⁻¹ = 1

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
s : Set G
x✝¹ : G
x✝ : x✝¹ ∈ s
⊢ x✝¹ * g = g * x✝¹ ↔ g * x✝¹ * g⁻¹ = 1 * x✝¹
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
x✝¹ : G
x✝ : x✝¹ ∈ s
⊢ x✝¹ * g = g * x✝¹ ↔ g * x✝¹ * g⁻¹ = 1 * x✝¹

Tactic:
mul_inv_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
s : Set G
x✝¹ : G
x✝ : x✝¹ ∈ s
⊢ x✝¹ * g = g * x✝¹ ↔ g * x✝¹ = 1 * x✝¹ * g
Module: Mathlib.Data.Finset.NoncommProd

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

Tactic:
| nil =>

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

Goal state before:
pp: case h.nil
α : Type u_3
inst✝ : Monoid α
a : α
comm : {x | x ∈ a ::ₘ ⟦[]⟧}.Pairwise Commute
⊢ a * [].prod = [].prod * a

Tactic:
| nil =>

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝ : CommMonoid M
⊢ ∏ _x ∈ s, 1 = 1

Tactic:
simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]

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

Goal state before:
pp: case nil
α : Type u_6
a : Multiset α
⊢ Disjoint [].sum a ↔ ∀ b ∈ [], Disjoint b a

Tactic:
| nil =>

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ c (f x) (f y) ↔ c.mk' (f x) = c.mk' (f y)

Tactic:
← c.eq

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ ↑(f x) = ↑(f y) ↔ c.mk' (f x) = c.mk' (f y)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

Tactic:
| nil =>

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
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ ¬p x

Tactic:
by simpa using h hs

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * g 1

Tactic:
_root_.map_one,

Goal state after:
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f 1 * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
_root_.map_one,

Goal state after:
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ 1 * g (of x)⁻¹ = g (of x)⁻¹
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
⊢ (List.map f []).prod = ∏ m ∈ [].toFinset, f m ^ count m []

Tactic:
| nil =>

Goal state after:
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
c : Con G
x✝ : G
h : x✝ ∈ {x | c x 1}
⊢ x✝⁻¹ ∈ {x | c x 1}

Tactic:
simpa using c.inv h

Goal state after: