mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
m : Multiset α
ih : filter p m = m.bind fun a ↦ if p a then {a} else 0
⊢ filter p (a ::ₘ m) = (a ::ₘ m).bind fun a ↦ if p a then {a} else 0

Tactic:
simp [filter_cons, ih]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
κ : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
O : Type u_7
M : Type u_8
n : ℕ
hn : n ≠ 0
x y : Multiset M
h : (fun a ↦ n • a) x = (fun a ↦ n • a) y
x✝ : M
⊢ n * count x✝ x = n * count x✝ y

Tactic:
simp only [← Multiset.count_nsmul, h]

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

Goal state before:
pp: α : Type u
l' l : List α
h : l' ∈ l.cyclicPermutations
⊢ l'.length = l.length

Tactic:
by
  obtain ⟨k, hk, rfl⟩ := get_of_mem h
  simp

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations ↔ l ~r l'

Tactic:
by
  constructor
  · simp_rw [mem_iff_get, get_cyclicPermutations]
    rintro ⟨k, rfl⟩
    exact .forall _ _
  · rintro ⟨k, rfl⟩
    rw [cyclicPermutations_rotate, mem_rotate]
    apply mem_cyclicPermutations_self

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k

pp: case succ
k n✝ : ℕ
⊢ (n✝ + 1).ascFactorial k = k ! * (n✝ + 1 + k - 1).choose k

Tactic:
· cases k
    · rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
    · simp only [zero_ascFactorial, Nat.zero_add, succ_sub_succ_eq_sub,
        Nat.sub_zero, choose_succ_self, Nat.mul_zero]

Goal state after:
case succ
k n✝ : ℕ
⊢ (n✝ + 1).ascFactorial k = k ! * (n✝ + 1 + k - 1).choose k
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:
classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
⊢ False

Tactic:
by
      obtain ⟨x⟩ := id hn
      refine absurd (?_ : x ∈ ⊥) notMem_bot
      simp [h]

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

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

Tactic:
rw [← preimage_iUnion₂, biUnion_of_singleton]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹ = ∅ ↔ s = ∅

Tactic:
rw [← image_inv_eq_inv, image_eq_empty]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Tactic:
rw [insert_eq, union_inv, inv_singleton, insert_eq]

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

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

Tactic:
← image_swap_prod,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' t ×ˢ s = ((fun b a ↦ (a, b)) '' t).seq s
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
x : N
a✝ : x ∈ ⊤
y : G
hy : f y = x
⊢ x ∈ map f ⊤

Tactic:
exact ⟨y, trivial, hy⟩

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
K : Subgroup G
f : G →* N
⊢ (f.domRestrict K).range = map f K

Tactic:
by
  simp_rw [SetLike.ext_iff, mem_range, mem_map, domRestrict_apply, SetLike.exists,
    exists_prop, forall_const]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)

Tactic:
simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]

Goal state after:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inl M N) = ⊥

Tactic:
ext x
  simp [mem_mker]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inr M N) = ⊥

Tactic:
ext x
  simp [mem_mker]

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

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k

Tactic:
simp [← div2_val, div2_bit]

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b n / 2 ^ 1 / 2 ^ m).bodd = (n / 2 ^ m).bodd

Tactic:
simp [← div2_val, div2_bit]

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

Goal state before:
pp: α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
⊢ encode a = encode ↑a

Tactic:
cases a; rfl

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

Goal state before:
pp: ⊢ Countable ℕ+

Tactic:
by delta PNat; infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Characteristic
⊢ (⨆ i ∈ s, H i).Characteristic

Tactic:
by
  simp [← iSup_subtype'', characteristic_iSup, h]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ normalizer s ≤ normalizer ↑(closure s)

Tactic:
intro g hg

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ normalizer s
⊢ g ∈ normalizer ↑(closure s)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ {a, b} * s = a • s ∪ b • s

Tactic:
rw [insert_eq, union_mul, singleton_mul, singleton_mul]; rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ Commute x y

Tactic:
suffices x * y * x⁻¹ * y⁻¹ = 1 by
    change x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa
  apply hdis.le_bot
  constructor
  · suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
    exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)
  · change x * y * x⁻¹ * y⁻¹ ∈ H₂
    apply H₂.mul_mem _ (H₂.inv_mem hy)
    apply hH₂.conj_mem _ hy

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
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
⊢ 1 ∈ {σ | ∀ (x : M), σ • x - x ∈ I}

Tactic:
simp [zero_mem]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊓ ⇑g) ⊤ = ⊤

Tactic:
rw [Pi.inf_apply, map_top, map_top, inf_top_eq]

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

Goal state before:
pp: α : Type u
β : Type u_1
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap ((a :: l₁).zip (b :: l₂)) = (b :: l₂).zip (a :: l₁)

Tactic:
simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]

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

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists).zip (List.map ofList l.sublists).reverse
⊢ x.1 + x.2 = ↑l

Tactic:
← map_reverse,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists).zip (List.map ofList l.sublists.reverse)
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists').zip (List.map ofList l.sublists').reverse
⊢ x.1 + x.2 = ↑l

Tactic:
← map_reverse,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists').zip (List.map ofList l.sublists'.reverse)
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
by
  rw [← mem_coe]
  exact ((isGLB_iff_isLeast i s hs).mp his).1

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

Goal state before:
pp: case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    l'.sublists.zip (map (fun x ↦ x ++ [a]) l'.sublists).reverse ++
      (map (fun x ↦ x ++ [a]) l'.sublists).zip l'.sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
← map_reverse,

Goal state after:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    l'.sublists.zip (map (fun x ↦ x ++ [a]) l'.sublists.reverse) ++
      (map (fun x ↦ x ++ [a]) l'.sublists).zip l'.sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

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

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

Tactic:
← map_reverse,

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

case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ (∅.sup fun b ↦ a \ f b) = a \ ∅.inf f

Tactic:
rw [sup_empty, inf_empty, sdiff_top]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun b ↦ a \ f b) = a \ s.inf f

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => rw [sup_empty, inf_empty, sdiff_top]
  | cons _ _ _ h => rw [sup_cons, inf_cons, h, sdiff_inf]

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ x, t ↑x ⋯).Finite

Tactic:
apply finite_iUnion fun i : s => ht i.1 i.2

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

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i → ∀ x ∈ s, a < f x

pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i

Tactic:
· intro h x hx
    refine h.trans_le (csInf_le ?_ ?_)
    · classical
      refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
      intro
      simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind
    · simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    have : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down

Goal state after:
α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
rw [h, Nat.sInf_empty, zero_add]

Goal state after:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ n = sInf {m | p m}
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
⊢ ∃ f, StrictMono f ∨ StrictAnti f

Tactic:
let f := Infinite.natEmbedding α

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
⊢ ∃ f, StrictMono f ∨ StrictAnti f
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hg : (∀ (m n : ℕ), m < n → f (g m) < f (g n)) ∨ ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ ∃ f, StrictMono f ∨ StrictAnti f

Tactic:
refine ⟨f ∘ g, ?_⟩

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hg : (∀ (m n : ℕ), m < n → f (g m) < f (g n)) ∨ ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
by
  simp_rw [Finset.range_eq_Ico, map_eq_image]
  convert! (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm
  ext x
  simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]
  constructor
  · lia
  · rintro h
    exact ⟨x - a, by lia⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α

Tactic:
rw [wellQuasiOrderedLE_iff, and_iff_left_iff_imp]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
⊢ WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ m = n

Tactic:
refine (H _ _ h ?_).elim

Goal state after:
case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f m) (f n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n

Tactic:
refine (H _ _ h ?_).elim

Goal state after:
case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f m)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case tail
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ c✝ : α
a✝ : TransGen (fun x1 x2 ↦ x1 ⩿ x2) x b✝
h₁ : b✝ ⩿ c✝
h₂ : x ≤ b✝
⊢ x ≤ c✝

Tactic:
exact h₂.trans h₁.le

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G

Tactic:
simp [eq_top_iff', isMulCommutative_iff, mem_center_iff, eq_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * c * z

Tactic:
← h.comm,

Goal state after:
M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ z * a * c = a * c * z
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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', Monotone fun n ↦ (ofLex f (g (g' n))).2

Tactic:
simp_rw [isPWO_iff_exists_monotone_subseq] at hβ

Goal state after:
α : 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)
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
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
⊢ ∃ g', Monotone fun n ↦ (ofLex f (g (g' n))).2
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ a * g = g * a

Tactic:
ha g hg

Goal state after:
M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ a * g = a * g
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ normalizer ↑H ⊓ normalizer ↑K ≤ normalizer ↑(H ⊔ K)

Tactic:
intro g hg

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : g ∈ normalizer ↑H ⊓ normalizer ↑K
⊢ g ∈ normalizer ↑(H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
intro g hg

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : g ∈ ⨅ i, normalizer ↑(H i)
⊢ g ∈ normalizer ↑(⨆ i, H i)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(K ⊔ H)

Tactic:
rw [sup_comm]
  exact normalizer_le_normalizer_sup_of_normalizer_le_left hHnK

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:
by rw [Finset.sum, Multiset.map_map]; rfl

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:
by rw [Finset.sum, Multiset.map_map]; rfl

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

Goal state before:
pp: M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ (List.map Subtype.val l).prod ∈ S

Tactic:
rw [← coe_list_prod]

Goal state after:
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ ↑l.prod ∈ S
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ u, x ^ g x = ∏ x ∈ t ∪ u, x ^ g x

Tactic:
· refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

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

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), s x y

Tactic:
by
  rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
  simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ s

Tactic:
exact sInf_le h

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

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → s x y

Tactic:
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)

Goal state after:
α : Type u_1
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → s a y
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:
sSup_def

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ conGen (sSup (DFunLike.coe '' S)) = conGen fun x y ↦ ∃ c ∈ S, c x y
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
generalize hL : ((a, b) :: L₁ : List _) = L
    rintro @⟨_ | ⟨p, s'⟩, e, a', b'⟩ <;> simp_all

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
a : α
b : Bool
⊢ ¬Step [(a, b)] L

Tactic:
by simp [Step.cons_left_iff, not_step_nil]

Goal state after: