mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype (α ↪ β)

Tactic:
by
  classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)

Tactic:
by
  classical
  have := Fintype.ofFinite (PLift α)
  have := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
⊢ IsPretransitive E G

Tactic:
refine ⟨fun x y ↦ ?_⟩

Goal state after:
E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x y : G
⊢ ∃ g, g • x = y
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: case succ
α : Type u
inst✝ : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹

Tactic:
| succ i hi =>

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

Goal state before:
pp: α : Type u
inst✝ : Group α
i : ℕ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
induction i with

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

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S

Tactic:
by
    rw [pow_succ]
    exact mul_mem (pow_mem hx n) hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set β
⊢ (⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t

Tactic:
by simp_rw [iUnion_prod_const]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i j : I
⊢ Commute (mulSingle i (x i)) (mulSingle j (x j))

Tactic:
by
  obtain rfl | hij := Decidable.eq_or_ne i j
  · rfl
  · exact Pi.mulSingle_commute hij _ _

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inr
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j

Tactic:
simp [h, eqComm]

Goal state after:
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
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K < comap f L ↔ K < L

Tactic:
by simp_rw [lt_iff_le_not_ge, comap_le_comap_of_surjective hf]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : y ∈ normalizer ↑H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ f y ∈ normalizer ↑(map f H)

Tactic:
rw [mem_normalizer_iff_map_conj_eq] at hy ⊢

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map (↑(MulAut.conj (f y))) (map f H) = map f H
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : x ∈ closure s
m : Mᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
by rwa [← op_closure] at hm

Goal state after:
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 ^ (k * ((↑(m + 1) * ↑n - ↑(m + 1) * 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
← Int.mul_sub,

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 ^ (k * (↑(m + 1) * (↑n - 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ ↑a ≤ l.maximum

Tactic:
exact le_maximum_of_mem' h

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

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

Tactic:
List.maximum_eq_coe_iff

Goal state after:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = WithBot.unbotD d ↑y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ (map (cons a) r₁ ++ [a :: l])

Tactic:
← append_assoc,

Goal state after:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) r₁ ++ [a :: l]
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++
      (List.map (cons b) (powersetAux' l✝) ++ List.map (cons b ∘ cons a) (powersetAux' l✝)) ~
    List.map (cons b) (powersetAux' l✝) ++
      (List.map (cons a) (powersetAux' l✝) ++ List.map (cons a ∘ cons b) (powersetAux' l✝))

Tactic:
← append_assoc,

Goal state after:
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++ List.map (cons b) (powersetAux' l✝) ++
      List.map (cons b ∘ cons a) (powersetAux' l✝) ~
    List.map (cons b) (powersetAux' l✝) ++
      (List.map (cons a) (powersetAux' l✝) ++ List.map (cons a ∘ cons b) (powersetAux' l✝))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++ List.map (cons b) (powersetAux' l✝) ++
      List.map (cons b ∘ cons a) (powersetAux' l✝) ~
    List.map (cons b) (powersetAux' l✝) ++
      (List.map (cons a) (powersetAux' l✝) ++ List.map (cons a ∘ cons b) (powersetAux' l✝))

Tactic:
← append_assoc,

Goal state after:
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++ List.map (cons b) (powersetAux' l✝) ++
      List.map (cons b ∘ cons a) (powersetAux' l✝) ~
    List.map (cons b) (powersetAux' l✝) ++ List.map (cons a) (powersetAux' l✝) ++
      List.map (cons a ∘ cons b) (powersetAux' l✝)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists _ _ _ h)

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

Goal state before:
pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))

Tactic:
← append_assoc,

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))

Tactic:
← append_assoc,

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))

Tactic:
intro i'

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
⊢ i' ∈ t → ∀ i_2 ∈ t, Disjoint (f (i, i')) (f (j, i_2))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))

Tactic:
intro i'

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
⊢ i' ∈ s → ∀ i_2 ∈ s, Disjoint (f (i', i)) (f (i_2, j))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a ↦ count b (f a)

Tactic:
· intro i s _ ih
    rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst✝ : Finite ↑s
H : ∀ (t : ↑s), Finite ↑↑t
⊢ Finite ↑(⋃ i, ↑i)

Tactic:
exact @Finite.Set.finite_iUnion _ _ _ _ H

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⋖ b ↔ a < b

Tactic:
unfold CovBy; decide

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ s.sigma t ↔ ⟨x, y⟩ ∈ s.biUnion fun i ↦ map (Embedding.sigmaMk i) (t i)

Tactic:
simp [and_left_comm]

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

Goal state before:
pp: s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s

Tactic:
rw [Nat.sInf_def h]
  exact Nat.find_spec h

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

Goal state before:
pp: case succ
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hk : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
⊢ k = l

Tactic:
rcases hk with ⟨hkn, rfl | hk⟩

Goal state after:
case succ.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
⊢ n + a = l

case succ.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
⊢ k = l
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:
by
  obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
  · refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
    induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
  · exact ⟨g, Or.intro_right _ hnr⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Icc a b) = Icc ↑a ↑b

Tactic:
subtype_Icc_eq

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Icc ↑a ↑b)) = Icc ↑a ↑b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = insert b (Iio b)

Tactic:
Iio_insert

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = Iic b
Module: Mathlib.GroupTheory.Subsemigroup.Center

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

Tactic:
rw [← Semigroup.mem_center_iff]

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

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

Tactic:
rw [← Semigroup.mem_center_iff]

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

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

Tactic:
rw [← Semigroup.mem_center_iff]

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

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn : List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (f n)
hn : n < g 0
⊢ List.SublistForall₂ r (f m) (f n)

Tactic:
if_pos (mn.trans hn)

Goal state after:
case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn : List.SublistForall₂ r (f m) (f n)
hn : n < g 0
⊢ List.SublistForall₂ r (f m) (f n)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
    ∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)

Tactic:
refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩

Goal state after:
ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
⊢ (∀ (a : A i), x i * a = a * x i) ∧
    (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a : A i
⊢ x i * a = a * x i

Tactic:
simpa using h1 (update x i a) i

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

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a / b ∈ S.centralizer

Tactic:
simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer hb)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
m : Gᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
by rwa [← op_closure] at hm

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

Goal state before:
pp: case h.cons.a
α : 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 y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
cases hx <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
Finset.sum,

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n =
    (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
Finset.sum,

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n =
    (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
m : Multiset M
comm : {x | x ∈ m}.Pairwise Commute
h : ∀ x ∈ m, x ∈ S
⊢ m.noncommProd comm ∈ S

Tactic:
by
  induction m using Quotient.inductionOn with | h l => ?_
  simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
  exact Submonoid.list_prod_mem _ h

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).Pairwise fun x y ↦ Commute ((f * g) x) ((f * g) y)

Tactic:
intro x hx y hy h
  apply Commute.mul_left <;> apply Commute.mul_right
  · exact comm_ff.of_refl hx hy
  · exact (comm_gf hy hx h.symm).symm
  · exact comm_gf hx hy h
  · exact comm_gg.of_refl hx hy

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤

Tactic:
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply]

Goal state after:
α : Type u_1
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = conGen fun x y ↦ ∃ c ∈ S, c x y

Tactic:
by
  rw [sSup_def]
  congr! with x y
  simp

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

Goal state before:
pp: α : Type u
L L₁ L₂ : List (α × Bool)
⊢ Red L (L₁ ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
generalize eq : L₁ ++ L₂ = L₁₂

Goal state after:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ Red L L₁₂ → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
by_cases h : a ∈ s

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

case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
simp +contextual [h₀]

Goal state after: