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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)

Tactic:
have := Classical.decEq γ
    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
    simp only [Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ Fin.find p hᵢ = natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)

Tactic:
by
  have hⱼ : ∃ j : Fin n, p (j.natAdd m) :=
    ⟨(Fin.cast (Nat.add_comm _ _) (Fin.find p hᵢ)).subNat _ hm, by simp [Fin.find_spec]⟩
  refine (find_eq_iff _).2 ⟨Fin.find_spec hⱼ, fun i hi ↦ ?_⟩
  cases i using addCases with | left i => _ | right i => _
  · exact Fin.find_min hᵢ (Fin.lt_def.mpr <| (Fin.castAdd_lt _ _).trans_le hm)
  · rw [Fin.natAdd_lt_natAdd_iff] at hi
    exact Fin.find_min hⱼ hi

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → Pairwise R (a :: b :: l)

Tactic:
pairwise_cons_cons_iff_of_trans

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → R a b ∧ Pairwise R (b :: l)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ
⊢ IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢

Goal state after:
case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
⊢ IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
classical
  exact Decidable.List.Lex.ne_iff H

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x y : α
⊢ IsChain R [x, y] ↔ R x y

Tactic:
simp only [IsChain.singleton, isChain_cons_cons, and_true]

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b

Tactic:
rw [List.isChain_cons_cons] at ha

Goal state after:
case cons.cons
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
⊢ l.rotate' (n + 1) ~ l

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ [].rotate' (n + 1) ~ []

case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
⊢ l.rotate (n + 1) = [] ↔ l = []

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case succ.nil
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
⊢ [].rotate (n + 1) = [] ↔ [] = []

case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
⊢ ([].rotate (n + 1)).reverse.rotate (n + 1) = [].reverse

case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case succ.nil
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
⊢ map f ([].rotate (n + 1)) = (map f []).rotate (n + 1)

case succ.cons
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~r l

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case nil
α : Type u
n : ℕ
⊢ [].rotate n ~r []

case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ ∃ n_1, n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case nil
α : Type u
n : ℕ
⊢ ∃ n_1, n_1 ≤ [].length ∧ [].rotate n_1 = [].rotate n

case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ (a :: l).length

Tactic:
simpa using h.le

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

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k = v i

Tactic:
by
  classical
    apply Subset.antisymm
    · simp [iInter_subset]
    · intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
⊢ y ∈ f '' ⋂ i, s i

Tactic:
refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default ∈ s i
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝ : Subsingleton M
x y : Submonoid M
i : M
⊢ i ∈ x ↔ i ∈ y

Tactic:
simp [← Subsingleton.elim 1 i]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

Tactic:
by
  rw [← preimage_iUnion₂, biUnion_of_singleton]

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:
inv_singleton,

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

Goal state before:
pp: α : Type u_2
m : Type u_5
n : Type u_6
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
inst✝ : One α
σ : n ≃ m
i : m
x : α
⊢ mulSingle i x ∘ ⇑σ = mulSingle (σ.symm i) x

Tactic:
by
  ext x
  aesop (add simp Pi.mulSingle_apply)

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

Goal state before:
pp: α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
rw [sInter_eq_biInter]
  exact image2_iInter₂_subset_left ..

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {a}⁻¹ = {b}

Tactic:
inv_singleton,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {a⁻¹} = {b}
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ b ∈ t, (fun a ↦ (a, b)) '' s

Tactic:
iUnion_image_right,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = image2 Prod.mk s t
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)

Tactic:
· rintro x (hx | hx)
    · exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
    · exact Subsemigroup.closure_le.mpr subset_closure hx

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⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

Goal state after:
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⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K✝ K : Subgroup G
s : Set G
hs : s = ↑K
x✝ : G
hx : x✝ ∈ s
⊢ x✝⁻¹ ∈ s

Tactic:
simpa [hs] using hx

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ n * g ∈ S ↔ g * n ∈ S

Tactic:
by rw [h, mul_assoc, mul_inv_cancel_right]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

Tactic:
convert! H.bot_or_nontrivial

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ Nontrivial ↥H
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s ∪ {1}) = closure s

Tactic:
closure_union_one

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure s = closure s
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
⊢ IsMulCommutative ↥(map f H)

Tactic:
refine .of_setLike_mul_comm ?_

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
⊢ ∀ a ∈ map f H, ∀ b ∈ map f H, a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
refine .of_setLike_mul_comm ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a
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
H : Subgroup G
⊢ comap f (map f H) = H ⊔ f.ker

Tactic:
by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
  intro x hx; simp only [mem_map, mem_comap] at hx
  rcases hx with ⟨y, hy, hy'⟩
  rw [← mul_inv_cancel_left y x]
  exact mul_mem_sup hy (by simp [mem_ker, hy'])

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊔ K).subgroupOf (H ⊔ K) = ⊤

pp: case hA
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

pp: case hA'
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K

Tactic:
subgroupOf_self

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ⊤ = ⊤

case hA
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hA'
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
⊢ Surjective ⇑(f.submonoidMap M')

Tactic:
rintro ⟨_, x, hx, rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, (f.submonoidMap M') a = ⟨f x, ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: a : ℤ
⊢ AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a

Tactic:
simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]

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
hg : g ∈ normalizer s
⊢ g ∈ normalizer ↑(closure s)

Tactic:
rw [mem_normalizer_iff_conj_image_eq] at hg

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ g ∈ normalizer ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

Tactic:
suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]

Goal state after:
case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * (y * x⁻¹ * y⁻¹) ∈ H₁
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
refine .of_setLike_mul_comm ?_

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → x = y

Tactic:
Subtype.ext_iff

Goal state after:
α : Type u_1
β : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → ↑x = ↑y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b

Tactic:
Lex.forall,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : α × β), ∃ b, toLex a < b
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b

Tactic:
Lex.forall,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : α × β), ∃ b, toLex a < b
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
let k := Nat.find H

Goal state after:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
⊢ ∃ n, ¬p n ∧ p (n + 1)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
⊢ closure {0} = ⊥

Tactic:
by
  simp [eq_bot_iff_forall, mem_closure_singleton, nsmul_zero]

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

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

Tactic:
by
  simp only [maximum, argmax_concat, id]
  cases argmax id l
  · exact (max_eq_right bot_le).symm
  · simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
⊢ Nonempty (α ≃ β)

Tactic:
cases nonempty_denumerable α

Goal state after:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝ : Denumerable α
⊢ Nonempty (α ≃ β)
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✝³ : EquivLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (a ⊔ b) ≤ c ↔ f a ⊔ f b ≤ c

Tactic:
simp only [← le_map_inv_iff, sup_le_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a ↑s) (min a (s.min' H))

Tactic:
exact (isLeast_min' _ _).insert _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Tactic:
replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
    intro x hx y hy hxy
    rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
    rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
    exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.inr
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ a :: l₁' ++ l₂ ~ a :: l

Tactic:
· exact (IH _ _ h).cons _

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : p (f a✝) ∧ ∀ x ∈ s✝, p (f x)
⊢ p (f a✝ ⊔ s✝.sup f)

Tactic:
exact hp _ hs.1 _ (ih hs.2)

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

Goal state before:
pp: case refine_2
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯
⊢ a ∈ s.powerset

Tactic:
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩

Goal state after:
case refine_2
α : Type u_1
s a : Finset α
ha✝ : a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯
i : ℕ
_hi : i ∈ range (#s + 1)
ha : a ∈ powersetCard i s
⊢ a ∈ s.powerset
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂

Tactic:
· rintro i j ⟨his, hi⟩ ⟨hjs, hj⟩
    exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (image f s).min' ⋯ ∈ image f s

Tactic:
exact min'_mem (image f s) _

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

Goal state before:
pp: case empty
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
hf : ∀ i ∈ ∅, Monotone (f i)
⊢ ⨆ j, ⨅ i ∈ ∅, f i j = ⨅ i ∈ ∅, ⨆ j, f i j

Tactic:
simp [iSup_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : b = x), f x h

Tactic:
refine le_ciSup₂ ⟨f b rfl, ?_⟩ b rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ∈ upperBounds (⋃ i, range (f i))
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
rw [sigmaLift, dif_neg h]

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ ∅ ↔ ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)