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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
k : Fin (l.rotate n).length
⊢ (l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩

Tactic:
by
  simp [getElem_rotate]

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ (n • m + m).prod = m.prod ^ n * m.prod ^ 1

Tactic:
pow_one,

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ (n • m + m).prod = m.prod ^ n * m.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l.reverse ~r l' → l ~r l'.reverse

Tactic:
intro h
      simpa using h.reverse

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

Goal state before:
pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'

Tactic:
intro h
      simpa using h.reverse

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0

Tactic:
split_ifs <;> simp_all <;> grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
· apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑∅ ≃ ↑(∅ ^ Fintype.card G)

Tactic:
empty_pow (ne_of_gt hG)

Goal state after:
case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑∅ ≃ ↑∅
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S * S ^ (n + 1), b * a⁻¹ ∈ S ^ (n + 1)

Tactic:
← h₂,

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S * (S ^ n * {a}), b * a⁻¹ ∈ S ^ n * {a}
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

Tactic:
rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
by
  rw [← image_inv_eq_inv, image_eq_empty]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ {a⁻¹} ∪ s⁻¹ = insert a⁻¹ s⁻¹

Tactic:
insert_eq

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ {a⁻¹} ∪ s⁻¹ = {a⁻¹} ∪ s⁻¹
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
have hl := congr_fun h l

Goal state after:
case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
simp [← mul_assoc, h₁, h₂]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) → ∃ x, x ∈ H ∧ P x

Tactic:
rintro ⟨x, x_in, hx⟩

Goal state after:
case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x⁻¹
⊢ ∃ x, x ∈ H ∧ P x
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x) → ∃ x, x ∈ H ∧ P x⁻¹

Tactic:
rintro ⟨x, x_in, hx⟩

Goal state after:
case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ x, x ∈ H ∧ P x⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑(e.trans e.symm)) K = K

Tactic:
MulEquiv.self_trans_symm,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑(MulEquiv.refl G)) K = K
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K

Tactic:
by rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
⊢ (∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H) → ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H

Tactic:
intro h n

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
n : N
⊢ f n ∈ H ↔ f (x * n * x⁻¹) ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
⊢ x ∈ comap f (normalizer ↑H) → x ∈ normalizer ↑(comap f H)

Tactic:
simp only [mem_normalizer_iff, mem_comap]
  intro h n
  simp [h (f n)]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ comap f (normalizer ↑H) = normalizer ↑(comap f H)

Tactic:
apply le_antisymm (le_normalizer_comap f)

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑(comap f H) ≤ comap f (normalizer ↑H)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
this : x ∈ closure s
⊢ motive x

Tactic:
induction this using closure_induction_right with

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
this : 0 < k
⊢ p (k - 1 + 1)

Tactic:
rwa [Nat.sub_add_cancel this]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
d : α
⊢ l.max?.getD d = WithBot.unbotD d l.maximum

Tactic:
cases hy : l.maximum with
  | bot => simp [List.maximum_eq_bot.mp hy]
  | coe y =>
    rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

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

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (min a b) = f a ⊓ f b

Tactic:
inf_eq_left.2 h,

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a = f a ⊓ f b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
← mem_coe

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ ↑s
Module: Mathlib.Data.List.Sublists

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

Tactic:
← sublists_reverse,

Goal state after:
α : Type u
l : List α
⊢ l.sublists = l.reverse.reverse.sublists
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
by
  classical
  obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
  exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₂✝ <+ sublistsLen (n + 1) l₂✝ ++ map (cons a) (sublistsLen n l₂✝)

Tactic:
apply sublist_append_left

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)

Tactic:
let := Subtype.orderBot Pbot

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (i, i').1

Tactic:
convert! le_iSup₂ (α := α) i' hi.2; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
⊢ {x ∈ powersetCard n t | s ⊆ x} = image (fun x ↦ x ∪ s) (powersetCard (n - #s) (t \ s))

Tactic:
ext x
  simp only [mem_filter, mem_powersetCard, mem_image]
  constructor
  · intro ⟨⟨hxt, hxn⟩, hsx⟩
    exact ⟨x \ s, ⟨fun y hy => mem_sdiff.mpr ⟨hxt (mem_sdiff.mp hy).1, (mem_sdiff.mp hy).2⟩,
           by rw [card_sdiff_of_subset hsx, hxn]⟩, sdiff_union_of_subset hsx⟩
  · rintro ⟨y, ⟨hyt, hyn⟩, rfl⟩
    refine ⟨⟨union_subset (hyt.trans sdiff_subset) hst, ?_⟩, subset_union_right⟩
    rw [card_union_of_disjoint (disjoint_of_subset_left hyt disjoint_sdiff_self_left), hyn]
    lia

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

Goal state before:
pp: case zero
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]

Goal state after:
case zero
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty.{?u.57 + 1} = card (ULift.{?u.61, 0} (Fin 0))
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁ : WithBot α
h₁ : WithBot.recBotCoe True p a₁
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (a₁ ⊔ a₂)

Tactic:
match a₁, a₂ with
  | ⊥, _ => rwa [bot_sup_eq]
  | (a₁ : α), ⊥ => rwa [sup_bot_eq]
  | (a₁ : α), (a₂ : α) => exact hp a₁ h₁ a₂ h₂

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

Goal state before:
pp: case inr
α : 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)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ sSup (g ∘ f '' s) = sSup ((fun x ↦ g (f x)) '' s)

Tactic:
comp_def

Goal state after:
case inr
α : 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)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ sSup ((fun x ↦ g (f x)) '' s) = sSup ((fun x ↦ g (f x)) '' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < ↑(f i)

Tactic:
by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), ¬x ∈ s → ¬P (insert x s)

Tactic:
by
  simp only [not_imp_not]
  exact ⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
    fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
Ici,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ (Finset.Ici a).val ↔ a ≤ x
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})

Tactic:
exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ico]
  exact Set.Ioo_subset_Ico_self

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}

Tactic:
rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
use PartiallyWellOrderedOn.exists_monotone_subseq
  rw [PartiallyWellOrderedOn, wellQuasiOrdered_iff_exists_monotone_subseq]
  exact fun H f ↦ H _ fun n ↦ (f n).2

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc a b

Tactic:
inf_eq_left.2 h,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a (a ⊔ b) = Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

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

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
← Semigroup.mem_center_iff

Goal state after:
M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x

Tactic:
exact ⟨f, hf1⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ ∀ (g : G), g * z = z * g

Tactic:
← Semigroup.mem_center_iff

Goal state after:
G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ z ∈ Set.center G
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : center G = ⊤
⊢ ∀ (a b : G), a * b = b * a

Tactic:
by
      rw [eq_top_iff'] at h
      intro x y
      apply Subgroup.mem_center_iff.mp _ x
      exact h y

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
← Semigroup.mem_center_iff

Goal state after:
M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑(r * (Units.map (Submonoid.center M).subtype) u) = ↑((Units.map (Submonoid.center M).subtype) u * r)

Tactic:
rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ (ConjClasses.mk g).carrier

Tactic:
ConjClasses.mem_carrier_iff_mk_eq,

Goal state after:
G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ ConjClasses.mk h = ConjClasses.mk g
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 : ↑u • x = x
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x

Tactic:
ConjAct.smul_def,

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 * (ConjAct.ofConjAct ↑u)⁻¹ = x
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
replace h₀ : ∀ b ∈ s, f b = 1 := by grind
    simp +contextual [h₀]

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a

Tactic:
by
  classical
  conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
  conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
  exact prod_congr rfl (by simpa)

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ Injective ⇑(lift N φ HN) ↔ N = φ.ker

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, QuotientGroup.ker_lift, Subgroup.map_eq_bot_iff]

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ φ.ker ≤ (mk' N).ker ↔ N = φ.ker
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ (map N M f h).ker = Subgroup.map (mk' N) (Subgroup.comap f (mk' M).ker)

Tactic:
MonoidHom.comap_ker

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ (map N M f h).ker = Subgroup.map (mk' N) ((mk' M).comp f).ker
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ ↑s * m = ↑s * n

Tactic:
mul_comm (s : R) n,

Goal state after:
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ ↑s * m = n * ↑s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case step
M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)

Tactic:
case step =>
    intro n _
    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

Goal state after: