mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
· simp at h₁
    simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
    apply add_lt_add
    · exact Nat.mul_self_lt_mul_self h
    · apply Nat.add_lt_add_right; assumption

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s ↔ ⇑(MulAut.conj g) '' s = s

Tactic:
simp_rw [mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, MulAut.conj_apply]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ min (map f l).prod (map g l).prod

Tactic:
by
  rw [le_min_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply min_le_left
  · apply min_le_right

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

Goal state before:
pp: case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
· obtain ⟨v, hv⟩ := exists_gt x.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]

Goal state after:
case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (k * (m.succ % n * (n - 1)))

Tactic:
mul_comm k,

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (m.succ % n * (n - 1) * k)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
⊢ m ∈ some n

Tactic:
· have :=
          Nat.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
            (index_of_argmax harg hml (ham _ (argmax_mem harg)))
        rw [(idxOf_inj hml).1 this, Option.mem_def]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
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:
simp [Subtype.coe_top Ptop]

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

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

Tactic:
rw [← sublists'_reverse, reverse_reverse]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ powersetCardAux 0 l = [0]

Tactic:
simp [powersetCardAux_eq_map_coe]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l : List α
⊢ powersetCardAux (n + 1) (a :: l) = powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l)

Tactic:
simp [powersetCardAux_eq_map_coe]

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 β
f : β → α
⊢ IsLUB (f '' ↑s) (s.sup f)

Tactic:
simp +contextual [IsLUB, IsLeast, upperBounds, lowerBounds, le_sup]

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

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l = l.toFinset.sup id

Tactic:
← coe_fold_r,

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ ↑l = l.toFinset.sup id
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun n ↦ sublistsLen n tl) (map succ (range tl.length)) ~ tl.sublists'

Tactic:
← flatMap_cons (f := fun n => sublistsLen n tl),

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n tl) (0 :: map succ (range tl.length)) ~ tl.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x

Tactic:
simpa only [mem_iUnion, exists_prop] using hy

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 α
this : card PEmpty.{?u.57 + 1} = card (ULift.{?u.61, 0} (Fin 0))
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
apply Trunc.bind (truncEquivOfCardEq this)

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))
⊢ PEmpty.{?u.57 + 1} ≃ ULift.{?u.61, 0} (Fin 0) → Trunc (P (ULift.{u, 0} (Fin 0)))
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: case succ
α✝ : 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 α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))

Tactic:
apply Trunc.bind (truncEquivOfCardEq this)

Goal state after:
case succ
α✝ : 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 α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
⊢ Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ) → Trunc (P (ULift.{u, 0} (Fin (n + 1))))
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:
by simp [← Ioi_inter_Iic]

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

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Tactic:
rcases h i j with ⟨k, hik, hjk⟩

Goal state after:
case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
k : ι
hik : f i ⊆ f k
hjk : f j ⊆ f k
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
rw [max_eq_left le]

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
have : Nonempty ι := ⟨i⟩

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)
Module: Mathlib.Order.Cover

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

Tactic:
exact Or.inl h2.symm

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ¬IsEmpty ι ↔ Nonempty ι

Tactic:
not_isEmpty_iff

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ Nonempty ι ↔ Nonempty ι
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ a ⋖ b

Tactic:
have : Nonempty ι := ⟨i⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
this : Nonempty ι
⊢ a ⋖ b
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
exact sigma_nonempty

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
⊢ s.Infinite

Tactic:
let f (n : ℕ) : α := Nat.recOn n (h default).choose fun _ a ↦ (h a).choose

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ s.Infinite
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:
simp only [not_imp_not]

Goal state after:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico (max a c) b

Tactic:
by
  rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]

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

Goal state before:
pp: case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ k ∉ Ici (k + 1)

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1

Tactic:
mem_Ici

Goal state after:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ sInf s = k + 1

Tactic:
sInf_def (⟨_, H⟩ : s.Nonempty),

Goal state after:
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ Nat.find ⋯ = k + 1
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < (n + 1).succ), u k = (⨆ k, ⨆ (_ : k < n.succ), u k) ⊔ u (n + 1)

Tactic:
iSup_lt_succ

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
k : ℕ
⊢ ¬IsEmpty { f_1 // f k ∈ Set.range ⇑f_1 }

Tactic:
not_isEmpty_iff

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
k : ℕ
⊢ Nonempty { f_1 // f k ∈ Set.range ⇑f_1 }
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
⊢ ¬IsEmpty ((fun x1 x2 ↦ x1 > x2) ↪r r)

Tactic:
not_isEmpty_iff

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r r)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ center.commMonoid.toMonoid = (center M).toMonoid

Tactic:
by
  with_reducible_and_instances rfl

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

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

Tactic:
by
  refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer
  exact fun x hx y hy ↦ hx y <| Set.subset_centralizer_centralizer hy

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h.left
α : 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
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ g 0 < g n

Tactic:
by_contra hx

Goal state after:
case h.left
α : 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
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
hx : ¬g 0 < g n
⊢ False
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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)
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
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
n : ℕ
⊢ (ofLex f (g n)).2 ∈ {y | toLex ((ofLex f (g 0)).1, y) ∈ s}

Tactic:
hhc n

Goal state after:
α : 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)
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
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
n : ℕ
⊢ (ofLex f (g n)).2 ∈ {y | toLex ((ofLex f (g n)).1, y) ∈ s}
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.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹ = Submonoid.powers g ⊔ Submonoid.powers g⁻¹

Tactic:
Submonoid.powers_eq_closure,

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹ = Submonoid.closure {g} ⊔ Submonoid.powers g⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹ = Submonoid.closure {g} ⊔ Submonoid.powers g⁻¹

Tactic:
Submonoid.powers_eq_closure,

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹ = Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹}
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ s.noncommProd f ⋯ = s.prod f

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
x✝ : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
⊢ f y = f (g x)

Tactic:
(mem_filter.1 hx).2

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
x✝ : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
⊢ f y = f y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
x✝ : ι
H : x✝ ∈ {a}
⊢ x✝ ∈ s

Tactic:
mem_singleton.1 H

Goal state after:
case refine_1
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
x✝ : ι
H : x✝ ∈ {a}
⊢ a ∈ s
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
⊢ mk ⁻¹' {↑1} = ↑N

Tactic:
by
  rw [← image_singleton, preimage_image_mk_eq_mul]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (lift f) x = prod ((map f) x)

Tactic:
by
  rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
· rw [ha h₁, hb h₂, mul_one]
    exact
      _root_.trans
        (prod_congr rfl fun c hc =>
          h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
        prod_const_one

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
f : ↥s → M
⊢ ∏ x, f x = ∏ x ∈ s, extend Subtype.val f 1 x

Tactic:
univ_eq_attach,

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
⊢ ∏ x ∈ s.attach, f x = ∏ x ∈ s, extend Subtype.val f 1 x
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
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
by
  classical
  rw [← insert_erase ha]
  simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
  rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

Goal state after: