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

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
by
  rw [revzip] at h
  induction l using List.reverseRecOn generalizing l₁ l₂ with
  | nil =>
    have : l₁ = [] ∧ l₂ = [] := by simpa using h
    simp [this]
  | append_singleton l' a ih =>
    rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *
    simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
    · rw [← append_assoc]
      exact (ih _ _ h).append_right _
    · rw [append_assoc]
      apply (perm_append_comm.append_left _).trans
      rw [← append_assoc]
      exact (ih _ _ h).append_right _

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u

Tactic:
have : Finite u := Finite.to_subtype hu

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
this : Finite ↑u
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄, i ⊆ s → ∀ ⦃j : Finset α⦄, j ⊆ s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
rintro i hi j hj

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Set α⦄, i ∈ 𝒫 s → ∀ ⦃j : Set α⦄, j ∈ 𝒫 s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
rintro i hi j hj

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]
  exact exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Fintype β
inst✝¹ : DecidableEq α
f : β → Set α
inst✝ : (w : β) → Fintype ↑(f w)
⊢ (⋃ x, f x).toFinset = Finset.univ.biUnion fun x ↦ (f x).toFinset

Tactic:
by
  ext v
  simp only [mem_toFinset, mem_iUnion, Finset.mem_biUnion, Finset.mem_univ, true_and]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, ∃ y ∈ f '' ↑s, x ≤ y

pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, y ≤ x

Tactic:
· simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
      exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]
    intro i
    split_ifs
    · exact ⟨_, by assumption, le_rfl⟩
    · assumption

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, y ≤ x
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
refine ⟨range f, finite_range f, fun x hx => ?_⟩

Goal state after:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ range f, t i
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ ⨆ x ∈ ↑(s.sigma t), f x = ⨆ x ∈ ↑s, ⨆ x_1 ∈ ↑(t x), f ⟨x, x_1⟩

Tactic:
Finset.coe_sigma,

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ ⨆ x ∈ (↑s).sigma fun i ↦ ↑(t i), f x = ⨆ x ∈ ↑s, ⨆ x_1 ∈ ↑(t x), f ⟨x, x_1⟩
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
classical
  have hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x := hf.invOn_invFunOn.2
  rw [← sup_congr (Eq.refl s) hfinvs, ← sup_image]
  congr
  exact (image_eq_preimage_of_leftInvOn_injOn hf.invOn_invFunOn.2 hf.2.1).symm

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

Goal state before:
pp: α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
⊢ s.restrict ∘ ⇑(Equiv.piCongrLeft π e) =
    ⇑(Equiv.piCongrLeft (fun b ↦ π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict

Tactic:
ext x b

Goal state after:
α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
x : (a : α) → π (e a)
b : ↥s
⊢ (s.restrict ∘ ⇑(Equiv.piCongrLeft π e)) x b =
    (⇑(Equiv.piCongrLeft (fun b ↦ π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict) x b
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b ∈ s, a ≤ b ∧ ?m.24 b

Tactic:
by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩

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

Goal state before:
pp: a : ℕ
⊢ Ico ⊥ a = range a

Tactic:
← Iio_eq_Ico,

Goal state after:
a : ℕ
⊢ Iio a = range a
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
⊢ Nat.find ⋯ = k + 1

Tactic:
find_eq_iff

Goal state after:
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_infinite h fun hf => _

Goal state after:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ {x | P x}.Finite → False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : OrderBot α
⊢ Unique ↥(Iic ⊥)

Tactic:
rw [Iic_bot]
  infer_instance

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
⊢ IsAntichain (fun x1 x2 ↦ x1 ≤ x2) (Set.range (f ∘ ⇑g))

Tactic:
rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf
      obtain h | rfl | h := lt_trichotomy m n
      · exact hc _ _ (g.strictMono h) hf
      · contradiction
      · exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set ↑s := {x | ↑x ≤ a}
h : t.Nonempty := Exists.intro ⟨a, ha⟩ le_rfl
y : α
hy : (fun x ↦ x ∈ s) y
hle : y ≤ ↑(⋯.min t h)
⊢ ↑(⋯.min t h) ≤ y

Tactic:
by_contra hnle

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set ↑s := {x | ↑x ≤ a}
h : t.Nonempty := Exists.intro ⟨a, ha⟩ le_rfl
y : α
hy : (fun x ↦ x ∈ s) y
hle : y ≤ ↑(⋯.min t h)
hnle : ¬↑(⋯.min t h) ≤ y
⊢ False
Module: Mathlib.GroupTheory.Submonoid.Center

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

Tactic:
Submonoid.coe_subtype,

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑((Units.map (Submonoid.center M).subtype) u * r)
Module: Mathlib.GroupTheory.Submonoid.Center

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

Tactic:
Submonoid.coe_subtype,

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑↑u * ↑r
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h.refine_1
α : 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))).1 = (f (g (g' 1))).1

Tactic:
exact (hhc (g' 0)).symm.trans (hhc (g' 1))

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩

Tactic:
· dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *
      grind

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

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd * tl.prod) = hd * (tl.prod * a)

Tactic:
← IH,

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd * tl.prod) = hd * (a * tl.prod)

case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute
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
  | empty => simp
  | cons x s hnotMem ih =>
    rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
    exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯

Tactic:
rintro Hxy Hxy' -
    refine Function.hfunext ?_ ?_
    · rw [c.eq.2 hx, c.eq.2 hy]
    · rintro Hyx Hyx' -
      exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
⊢ (cons a s h).prod = fun f ↦ f a * ∏ x ∈ s, f x

Tactic:
funext f
  rw [Finset.prod_cons h]

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

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
val✝ inv✝ : c.Quotient
x y : M
h₁ : Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y = 1
h₂ : Quot.mk (⇑c.toSetoid) y * Quot.mk (⇑c.toSetoid) x = 1
⊢ p { val := Quot.mk (⇑c.toSetoid) x, inv := Quot.mk (⇑c.toSetoid) y, val_inv := h₁, inv_val := h₂ }

Tactic:
exact H x y (c.eq.1 h₁) (c.eq.1 h₂)

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 (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) =
    (∏ x ∈ (s.toLeft.disjSum s.toRight).toLeft, f (Sum.inl x)) *
      ∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x)

Tactic:
Finset.toLeft_disjSum,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) =
    (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_1
M : Type u_1
inst✝ : Monoid M
x✝ : FG M
S : Finset M
hS : Submonoid.closure ↑S = ⊤
⊢ Function.Surjective ⇑(FreeMonoid.lift Subtype.val)

Tactic:
rwa [← MonoidHom.mrange_eq_top, ← Submonoid.closure_eq_mrange]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Monoid M
α : Type
w✝ : Finite α
φ : FreeMonoid α →* M
hφ : Function.Surjective ⇑φ
⊢ FG M

Tactic:
exact Monoid.fg_of_surjective _ hφ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
G : Type u_3
inst✝ : Group G
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG G

Tactic:
· intro ⟨α, _, φ, hφ⟩
    exact Group.fg_of_surjective hφ

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1

Tactic:
rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : f a = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
⊢ base = Group.conjugatesOfSet base

Tactic:
refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
rw [commutator_le]

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ∀ g₁ ∈ H₁.prod K₁, ∀ g₂ ∈ H₂.prod K₂, ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case h₁
G : Type u_1
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G

Tactic:
rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
    exact ⟨g₁, g₂, rfl⟩

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑⁅p, q⁆ = 1

Tactic:
commutatorElement_def

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑(p * q * p⁻¹ * q⁻¹) = 1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ s • (t • r, ⟨t * ↑s, hst⟩).fst = (↑s * t) • (r, s).fst

Tactic:
rw [mul_smul, Submonoid.smul_def]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
a : WithTop α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ StrictMono fun x ↦ a * x

Tactic:
lift a to α using hinf
  rintro b c hbc
  lift b to α using hbc.ne_top
  match c with
  | ⊤ => simp [← coe_mul, mul_top h₀.ne']
  | (c : α) =>
  simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
  exact mul_lt_mul_of_pos_left hbc h₀

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
h : ¬IsMin a
⊢ IsSuccPrelimit a ↔ IsSuccLimit a

Tactic:
simp [isSuccLimit_iff, h]

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : OrderTop α
⊢ succ ⊤ = ⊤

Tactic:
rw [succ_eq_iff_isMax, isMax_iff_eq_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
n : ℕ
hn : pred^[n] c = b
⊢ ∃ n, pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
use n

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
n : ℕ
hn : pred^[n] c = b
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) ≤ f a) → Monotone f

Tactic:
by
  simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α) a)
a : α
⊢ Shrink.rec f ((equivShrink α) a) = f a

Tactic:
by
  simp only [Shrink.rec, eqRec_eq_cast, cast_eq_iff_heq]
  rw [Equiv.symm_apply_apply]

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h : ∀ (m : Fin n), get ⟨v, hv⟩ m = get ⟨w, hw⟩ m
⊢ (↑⟨v, hv⟩).length = (↑⟨w, hw⟩).length

Tactic:
rw [hv, hw]

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
⊢ Countable (Sigma π)

Tactic:
choose g hg using fun a => exists_injective_nat (π a)

Goal state after:
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
g : (a : α) → π a → ℕ
hg : ∀ (a : α), Injective (g a)
⊢ Countable (Sigma π)
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ b ∈ univ.erase i, #(s b)

Tactic:
card_filter_piFinset_eq_of_mem _ _ h

Goal state after:
case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ ∏ j ∈ univ.erase i, #(s j) = ∏ b ∈ univ.erase i, #(s b)
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ b ∈ univ.erase i, #(s b)

Tactic:
rw [card_filter_piFinset_eq_of_mem _ _ h]

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.pred ⋯)) a

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero
        (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
      rw [← List.insertIdx_eraseIdx_of_ge]
      · simp; rfl
      · simpa
      · simpa [Nat.lt_succ_iff] using hij

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f = g

Tactic:
rw [← toRelEmbedding_inj]
  ext
  exact h _

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous fun x ↦ (f x, g x)

Tactic:
rw [← scottContinuousOn_univ] at ⊢ hf hg
  exact ScottContinuousOn.prodMk (by grind) hf hg

Goal state after: