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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop n xs = (List.drop (xs.length - n') xs).reverse.reverse

Tactic:
h₀,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop (xs.length - n') xs = (List.drop (xs.length - n') xs).reverse.reverse
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ filter p (filter q s) = filter q (filter p s)

Tactic:
simp [and_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n

Tactic:
contrapose!
    exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a s = count a (s - t) + min (count a s) (count a t)

Tactic:
count_sub,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a s = count a s - count a t + min (count a s) (count a t)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂

Tactic:
nth_rw 1 [h, take_eq_left_iff]

Goal state after:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).inits = (a :: s).inits ++ map (fun l ↦ a :: s ++ l) t.inits.tail

Tactic:
by simp [inits_append s t, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
ι : Type u_4
s : Set ι
f : ι → Finset α
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
by
  simp [Set.PairwiseDisjoint, Set.Pairwise, not_imp_comm (a := _ = _),
    not_disjoint_iff_nonempty_inter]

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

Goal state before:
pp: n : ℕ
⊢ Injective predAbove

Tactic:
intro i j hij

Goal state after:
n : ℕ
i j : Fin n
hij : i.predAbove = j.predAbove
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_of_lt] <;> omega

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m = n
f : Fin m → α
⊢ ofFn f = ofFn fun i ↦ f (Fin.cast ⋯ i)

Tactic:
subst h
  simp_rw [Fin.cast_refl, id]

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

Goal state before:
pp: case grind
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h✝ : ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
this : #(X ∪ Y) = #X + #(Y \ X)
⊢ False

Tactic:
finish

Goal state after:
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ #univ ≤ #s

Tactic:
by rw [hs, Finset.card_univ]

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ x = b

Tactic:
hx b

Goal state after:
α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ x = x
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑t
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (x : α), x ∈ {a ∈ t.toFinset | a ∈ s} ↔ x ∈ s ∩ t

Tactic:
simp [and_comm]

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
⊢ ∃ a, a ∉ s

Tactic:
by_contra! h; exact infinite_univ (hs.subset fun a _ ↦ h _)

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
by
  split_ifs
  · grind [find_eq_zero]
  · grind [find_of_not_zero]

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

Goal state before:
pp: case H₂
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ Pairwise (fun x y ↦ x ≠ y → R x y) l

Tactic:
exact hl.imp @fun a b h _ ↦ by exact h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Tactic:
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
    simp [map_take, take_take, Nat.min_eq_left]

Goal state after:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l✝ : List α
n m : ℕ
⊢ l✝.rotate (n + m) = (l✝.rotate n).rotate m

Tactic:
rw [rotate_rotate]

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

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
induction s using Multiset.induction <;> simp [Nat.mul_mod, *]

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

Goal state before:
pp: α : Type u
x : α
l : List α
⊢ (x :: l).cyclicPermutations.length = l.length + 1

Tactic:
by simp [cyclicPermutations_cons]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
subst h
    rw [Pi.cons_same]

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g a ∈ t a

Tactic:
exact hg a

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)

Tactic:
cases f using Fin.snocCases
  simp [Function.comp_def]

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 β
⊢ Finite (α ↪ β)

Tactic:
rcases isEmpty_or_nonempty (α ↪ β) with _ | h
  · infer_instance
  · refine h.elim fun f => ?_
    have : Finite α := Finite.of_injective _ f.injective
    exact Finite.of_injective _ DFunLike.coe_injective

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:
by
  induction i with
  | zero => simp
  | succ i hi => simp [pow_succ, hi]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' univ = univ

Tactic:
image_univ_of_surjective hf.surjective

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ (∃ x, x ∈ H ∧ ¬x ∈ K) → ↑H ⊆ ↑L

Tactic:
exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)

Tactic:
show unpair (b * b + a) = (a, b)

Goal state after:
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)

Tactic:
rw [boddDiv2, ih]
    cases hn : n.bodd <;> simp [hn]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ ∃ y, encode y = n

Tactic:
Ne,

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ ¬decode₂ α n = none ↔ ∃ y, encode y = n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
H : ι → Subgroup G
⊢ ⨅ i, normalizer ↑(H i) ≤ normalizer ↑(⨅ i, H i)

Tactic:
grind [le_normalizer_iff, mem_iInf, mem_normalizer_iff]

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

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
s : Set G
H : Subgroup G
a : G
⊢ a * 1 * a⁻¹ ∈ H

Tactic:
rw [mul_one, mul_inv_cancel]; exact H.one_mem

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a : α
h : a ∈ x • s
ha : a ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b ↔ Lex r (fun i ↦ Function.swap (s i)) b a

Tactic:
by
  constructor <;>
    · rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
      · exact Lex.left _ _ h
      · exact Lex.right _ _ h

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
rw [closure_singleton_eq, mem_mrange]; rfl

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.succ % n)).toNat) = x ^ (k * (↑(m % n)).toNat) * x ^ k

Tactic:
iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]

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

Goal state before:
pp: case succ.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (ofNat α n) ∈ Option.map some (decode n)

Tactic:
decode_eq_ofNat,

Goal state after:
case succ.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (ofNat α n) ∈ Option.map some (some (ofNat α n))
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∀ a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x), a ∈ s

Tactic:
by intro a ha; simpa using! (List.mem_filter.mp ha).2

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ idxOf m l ≤ idxOf a l

Tactic:
rw [_root_.le_antisymm hma (h a hal)]

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

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

Tactic:
simp [List.maximum_eq_bot.mp hy]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
a x : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max ⊥ l

Tactic:
induction l with
  | nil => exact absurd hx not_mem_nil
  | cons y l IH =>
    obtain hl | hl := hx
    · simp only [foldr]
      exact le_max_of_le_left h
    · exact le_max_of_le_right (IH (by assumption))

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
by
  rw [sdiff_eq, sdiff_eq, map_inf, map_compl']

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

Goal state before:
pp: α : Type u
a : α
⊢ ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
by
  intro r₁ r₂
  rw [sublists'Aux, Array.foldl_toList]
  have := List.foldl_hom Array.toList (g₁ := fun r l => r.push (a :: l))
    (g₂ := fun r l => r ++ [a :: l]) (l := r₁) (init := r₂.toArray) (by simp)
  simpa using this

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

Goal state before:
pp: case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ (s.erase x).max ≠ ↑x

Tactic:
· rw [s0, max_empty]
    exact WithBot.bot_ne_coe

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Multiset.map val (powersetCard 1 s).val = Multiset.map val (map { toFun := singleton, inj' := ⋯ } s).val

Tactic:
simp [Multiset.powersetCard_one]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i

Tactic:
refine
    (biUnion_sdiff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_sdiff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)

Goal state after:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction s using cons_induction <;> simp [*]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ sSup (range fun x ↦ a) = a

Tactic:
range_const,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ sSup {a} = a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι

Tactic:
Ne,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ¬⨅ i, ↑(f i) = ⊤ ↔ Nonempty ι
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ (x ∈ t.sigma fun a ↦ s.preimage (Sigma.mk a) ⋯) ↔ x ∈ {a ∈ s | a.fst ∈ t}

Tactic:
simp [and_comm]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
by
  classical
    rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
    rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ici ↑a) ↔ a ≤ x

Tactic:
simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LT α
⊢ univ.IsWF ↔ WellFoundedLT α

Tactic:
simp [IsWF, wellFoundedOn_iff, isWellFounded_iff]

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

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

Tactic:
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ ReflTransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
le_iff_transGen_wcovBy,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y ↔ ReflTransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inl
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : IsEmpty α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

pp: case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Tactic:
· exact subsingleton_of_subsingleton.partiallyWellOrderedOn

Goal state after:
case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

Tactic:
rw [mk_eq_mk_iff_isConj] at H
    exact H.eq_of_left_mem_center hx

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
⊢ g ∈ centralizer s ↔ ∀ h ∈ s, ⁅g, h⁆ = 1

Tactic:
refine forall₂_congr fun _ _ ↦ ?_
  rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]

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

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ l, p x
⊢ p l.prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.Nodup
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
rw [← List.dedup_eq_self] at hl
  simp [noncommProd, hl]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
classical
  simpa only [← Multiset.map_erase_of_mem _ _ h] using!
    Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

Goal state after:
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 × Quotient s
⊢ (fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯)
      ((fun x ↦
          match x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
        q) =
    q

Tactic:
rcases q with ⟨qa, qb⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
qa : Quotient r
qb : Quotient s
⊢ (fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯)
      ((fun x ↦
          match x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
        (qa, qb)) =
    (qa, qb)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Monoid M
s : Finset M
⊢ Submonoid.closure ↑(s.preimage Subtype.val ⋯) = ⊤

Tactic:
Finset.coe_preimage,

Goal state after:
M : Type u_1
N : Type u_2
inst✝ : Monoid M
s : Finset M
⊢ Submonoid.closure (Subtype.val ⁻¹' ↑s) = ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Subgroup.closure ↑(s.preimage Subtype.val ⋯) = ⊤

Tactic:
Finset.coe_preimage,

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Subgroup.closure (Subtype.val ⁻¹' ↑s) = ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
G : Type u_3
H : Type u_4
inst✝⁵ : Group G
inst✝⁴ : AddGroup H
inst✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG M
inst✝ : FG N
⊢ (⊤.prod ⊤).FG

Tactic:
exact ‹FG M›.fg_top.prod ‹FG N›.fg_top

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
G : Type u_3
H : Type u_4
inst✝⁵ : Group G
inst✝⁴ : AddGroup H
inst✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
⊢ ⊤.FG

Tactic:
by
    rw [← Subgroup.top_prod_top]
    exact ‹FG G›.out.prod ‹FG G'›.out

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, center G⁆ = ⊥

Tactic:
simp [commutator_eq_bot_iff_le_centralizer]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, f ⁅g₁, g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
map_commutatorElement

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
ih : of s * of t = of t * of s
⊢ of s * -of t = -of t * of s

Tactic:
| neg t ih =>

Goal state after:
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⟩).snd = ↑s * t * ↑(r, s).snd

Tactic:
by rw [← mul_assoc]

Goal state after: