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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
⊢ motive s

Tactic:
· have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
    simp only [mem_image] at H
    rcases H with ⟨a, has, hfa⟩
    rw [← insert_erase has]
    refine insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)
    rw [hfa]
    exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)

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

Goal state before:
pp: α : Type u_1
⊢ Function.Injective powerset

Tactic:
intro a₁ a₂ a
  exact le_antisymm
    (powerset_le_powerset_iff_le.mp (le_of_eq a))
    (powerset_le_powerset_iff_le.mp (le_of_eq a.symm))

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 : α
T : Set α
hT : T ∈ s
hy : y ∈ T
hne : x ≠ y
⊢ r x y

Tactic:
obtain ⟨U, hU, hSU, hTU⟩ := hd S hS T hT

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 α
hT : T ∈ s
hy : y ∈ T
hne : x ≠ y
U : Set α
hU : U ∈ s
hSU : S ⊆ U
hTU : T ⊆ U
⊢ r x y
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
k : ι
hik : f i ⊆ f k
hjk : f j ⊆ f k
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Tactic:
exact ⟨k, hik hi, hj.trans hjk⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
by
  by_cases! h : Exists p
  · have : Nonempty <| Exists p := ⟨h⟩
    refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi
    rintro _ ⟨_, ⟨j, rfl⟩, ⟨hj, rfl⟩⟩
    rfl
  · cases isEmpty_or_nonempty ι <;>
      simp [h, iSup_of_empty', ciSup_const]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₂, b₂)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
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, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⋖ b

Tactic:
rintro ⟨i, hi, h⟩

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)
⊢ a ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⩿ x ∧ b = Function.update a i x

Tactic:
rintro ⟨i, hi, h⟩

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ i x, a i ⩿ x ∧ b = Function.update a i x
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⋖ x ∧ b = Function.update a i x

Tactic:
rintro ⟨i, hi, h⟩

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ i x, a i ⋖ x ∧ b = Function.update a i x
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, x ⩿ b i ∧ a = Function.update b i x

Tactic:
rintro ⟨i, hi, h⟩

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ i x, x ⩿ b i ∧ a = Function.update b i x
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, x ⋖ b i ∧ a = Function.update b i x

Tactic:
rintro ⟨i, hi, h⟩

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ i x, x ⋖ b i ∧ a = Function.update b i x
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
e : α ≃ β
s : Finset β
⊢ Finset.image (⇑e.symm) s = s.preimage ⇑e ⋯

Tactic:
grind [Finset.mem_preimage]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
f : ↑s ≃o ↑t
hx : Minimal (fun x ↦ x ∈ s) x
⊢ Minimal (fun x ↦ x ∈ t) ↑(f ⟨x, ⋯⟩)

Tactic:
by
  simpa only [show t = range (Subtype.val ∘ f) by simp, mem_univ, minimal_true_subtype, hx,
    true_imp_iff, image_univ] using! OrderEmbedding.minimal_mem_image
    (f.toOrderEmbedding.trans (OrderEmbedding.subtype (· ∈ t))) (s := univ) (x := ⟨x, hx.prop⟩)

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 ∈ s ∧ k ∉ s

Tactic:
eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs,

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

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.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a

Tactic:
simp_rw [mem_erase, mem_Ico]

Goal state after:
a b x : ℕ
⊢ a.succ ≤ x ∧ x < b ↔ x ≠ a ∧ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrderTop α
⊢ h₀ = h₁

Tactic:
by
    obtain ⟨h₀_finset_Ioi, h₀_finset_Ici, h₀_finset_mem_Ici, h₀_finset_mem_Ioi⟩ := h₀
    obtain ⟨h₁_finset_Ioi, h₁_finset_Ici, h₁_finset_mem_Ici, h₁_finset_mem_Ioi⟩ := h₁
    have hIci : h₀_finset_Ici = h₁_finset_Ici := by
      ext a b
      rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
    have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
    simp_rw [hIci, hIoi]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
⊢ ∀ (a : { x // x ∈ range f }), Acc (Subrel r fun x ↦ x ∈ range f) a
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ WellQuasiOrdered r ↔ WellQuasiOrdered s

Tactic:
apply (Equiv.arrowCongr (.refl ℕ) f).forall_congr

Goal state after:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ ∀ (a : ℕ → α),
    (∃ m n, m < n ∧ r (a m) (a n)) ↔
      ∃ m n, m < n ∧ s (((Equiv.refl ℕ).arrowCongr ↑f) a m) (((Equiv.refl ℕ).arrowCongr ↑f) a n)
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ b ∈ Ioc a ⟨y, ⋯⟩ ↔ a < b

Tactic:
simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
    exact fun _ => b.property

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s

Tactic:
closure_inv,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ (closure s)⁻¹ ↔ x⁻¹ ∈ closure s
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt] at hs

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G)) g)

Tactic:
rw [mem_carrier_iff_mk_eq]

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ConjClasses.mk (h * g * h⁻¹) = Quot.mk (⇑(IsConj.setoid G)) g
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
⊢ center ((i : ι) → A i) = univ.pi fun i ↦ center (A i)

Tactic:
ext x
  simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
  refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
  exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩

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

Goal state before:
pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y_1 ∈ ↑C, x * y_1 = y * z

Tactic:
refine ⟨y, ⟨?_, hy⟩, z, hz, rfl⟩

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y ∈ ↑A
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
⊢ (fun x ↦
        match x with
        | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
      ((fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯) q) =
    q

Tactic:
induction q using Quotient.inductionOn'

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
a✝ : α × β
⊢ (fun x ↦
        match x with
        | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
      ((fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯) (Quotient.mk'' a✝)) =
    Quotient.mk'' a✝
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
⊢ (fun x ↦ Quotient.mk'' fun i ↦ (x i).out) ((fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) q) = q

Tactic:
induction q using Quotient.inductionOn'

Goal state after:
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
⊢ (fun x ↦ Quotient.mk'' fun i ↦ (x i).out) ((fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) (Quotient.mk'' a✝)) =
    Quotient.mk'' a✝
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ (QuotientGroup.con f.ker) x✝ y✝ ↔ (Con.ker f) x✝ y✝

Tactic:
QuotientGroup.con,

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ { toSetoid := leftRel f.ker, mul' := ⋯ } x✝ y✝ ↔ (Con.ker f) x✝ y✝
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ ↑x = 1 ↔ x ∈ N

Tactic:
by
  refine QuotientGroup.eq.trans ?_
  rw [mul_one, Subgroup.inv_mem_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ (QuotientGroup.con c.subgroup) x y ↔ c x y

Tactic:
QuotientGroup.con,

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ { toSetoid := leftRel c.subgroup, mul' := ⋯ } x y ↔ c x y
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ MonoidHom.mrange e

Tactic:
MonoidHom.mrange_eq_map e

Goal state after:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
⊢ 0 * a + 0 * a = 0 * a

Tactic:
simp [← add_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), ⊤⁆, centralizer ↑(commutator G)⁆ = ⊥

Tactic:
rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ g (f.sec 1).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec 1).2)⁻¹ = 1

Tactic:
by rw [mul_inv_left, mul_one]; exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])

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

Goal state before:
pp: case h.left
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * ↑s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂

Tactic:
rw [smul_smul, mul_assoc (c := v₀), ← hs₄]
    simp only [smul_smul, mul_assoc]

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ (∀ (x y : M), f x = f y ↔ g x = g y) → Injective ⇑(f.lift hg)

Tactic:
· intro H z w h
    obtain ⟨_, _⟩ := f.surj z
    obtain ⟨_, _⟩ := f.surj w
    rw [← f.mk'_sec z, ← f.mk'_sec w]
    exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : IsPredLimit x
⊢ IsPredLimit ↑x

Tactic:
simpa [WithTop.isPredPrelimit_iff, isPredLimit_iff, WithTop.exists] using h

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

Goal state before:
pp: α : Type u_1
a : α
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
⊢ IsMin a

Tactic:
intro b hb
  rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
  · exact le_rfl
  · rw [iterate_succ_apply'] at h
    exact (not_isSuccPrelimit_succ _ h).elim

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

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ (∃ x, ¬succ x ≠ a) ↔ a ∈ range succ

Tactic:
not_ne_iff,

Goal state after:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ (∃ x, succ x = a) ↔ a ∈ range succ
Module: Mathlib.Logic.Small.Basic

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

Tactic:
refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)
    obtain ⟨a, ha⟩ := h b
    exact ⟨a, by rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
a✝ : Y
h : f (succ (f.symm a✝)) ≤ a✝
⊢ IsMax a✝

Tactic:
rw [← f.symm.isMax_apply]
    refine max_of_succ_le ?_
    simp [f.le_symm_apply, h]

Goal state after:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ a * c

Tactic:
obtain rfl | hne := eq_or_ne a ⊤

Goal state after:
case inl
c : ℕ∞
hc : c ≠ 0
⊢ ⊤ ≤ ⊤ * c

case inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
⊢ a ≤ a * c
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

Tactic:
apply prod_congr rfl

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
⊢ ∀ x ∈ s, Function.update f i b x = f x
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
a : α
s : Sym α n
⊢ (a :: symEquivSym' s) = symEquivSym' (a ::ₛ s)

Tactic:
rcases s with ⟨⟨l⟩, _⟩
  rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| n

Tactic:
rw [← s.2, ← Multiset.card_attach]

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| (↑s).attach.card
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
x✝¹ x✝ : { x // x.length = 1 }
val✝¹ : List α
property✝ : val✝¹.length = 1
val✝ : List α
h : val✝.length = 1
perm : ⟨val✝¹, property✝⟩ ≈ ⟨val✝, h⟩
⊢ (↑⟨val✝¹, property✝⟩).head ⋯ = (↑⟨val✝, h⟩).head ⋯

Tactic:
obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
s : Sym α 1
x✝¹ x✝ : { x // x.length = 1 }
val✝ : List α
property✝ : val✝.length = 1
a : α
h : [a].length = 1
perm : ⟨val✝, property✝⟩ ≈ ⟨[a], h⟩
⊢ (↑⟨val✝, property✝⟩).head ⋯ = (↑⟨[a], h⟩).head ⋯
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
val✝ : Multiset α
l : List α
h : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk (⇑(List.isSetoid α)) l, h⟩) =
    ⟨Quot.mk (⇑(List.isSetoid α)) l, h⟩

Tactic:
obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h

Goal state after:
case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b : α
val✝ : Multiset α
a : α
h : Multiset.card (Quot.mk ⇑(List.isSetoid α) [a]) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩) =
    ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i, f ↑i = ∏ i ∈ range n, f i

Tactic:
by rw [← attach_eq_univ, prod_attach]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y ≤ x
⊢ (sumLexIicIoi x).symm y = toLex (Sum.inl ⟨y, h⟩)

Tactic:
by
  rw [symm_apply_eq, sumLexIicIoi_apply_inl]

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit ⊥

Tactic:
exact isSuccPrelimit_bot

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = ma * mb

Tactic:
simp only [← ha.2, ← hb.2]

Goal state after:
α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = a.get ⋯ * b.get ⋯
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
⊢ f z ≤ f y

Tactic:
have hz' := hz

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
hz' : z ∈ bot x f
⊢ f z ≤ f y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) → ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

Tactic:
introv h

Goal state after:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z
i : ℕ
⊢ (c₀ i) (c₁ i) ≤ z