mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: case cons
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s).Finite), motive (↑s) hs
hs : (↑(Finset.cons a s ha)).Finite
⊢ motive (↑(Finset.cons a s ha)) hs

Tactic:
| cons a s ha ih =>

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
⊢ l₁.flatten <+ l₂.flatten

Tactic:
by
  induction h with grind

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

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only

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

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

Tactic:
rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Tactic:
refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0

case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((tl ++ [hd]).rotate n).reverse.rotate (n + 1) = (hd :: tl).reverse

Tactic:
← rotate_rotate,

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ (((tl ++ [hd]).rotate n).reverse.rotate n).rotate 1 = (hd :: tl).reverse
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ 0 + n.choose k.succ = 0

Tactic:
choose_eq_zero_of_lt hnk1

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ 0 + 0 = 0
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k)! = (n - k) * (n - k.succ)!

Tactic:
rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0

Tactic:
have H₁ {x y z : α} : count (x, y) (map (z, ·) l) = if z = x then count y l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    have H₂ {x y z : α} : count (x, y) (map (·, z) l) = if z = y then count x l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    simp only [(offDiag_cons_perm _ _).count_eq, count_append, ihl, H₁, H₂, count_cons, beq_iff_eq]
    have := Nat.le_mul_self (count c l)
    split_ifs <;> simp_all <;> grind

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ List.count a l + List.count a l ≤ List.count a l * List.count a l

Tactic:
← Nat.two_mul

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 2 * List.count a l ≤ List.count a l * List.count a l
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔ FactorsThrough f s.domRestrict

Tactic:
FactorsThrough

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.domRestrict a = s.domRestrict b → f a = f b
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _

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

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (insert a s).pi t = (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)

Tactic:
apply eq_of_veq
  rw [← (pi (insert a s) t).2.dedup]
  refine
    (fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                    Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_notMem ha)
  subst s'; rw [pi_cons]
  congr; funext b
  exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

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
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j

Tactic:
image_iInter hf

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
⊢ {a} ^ 0 = {a ^ 0}

Tactic:
by simp [singleton_one]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' s ^ 0 = (⇑f '' s) ^ 0

Tactic:
by simp [singleton_one]

Goal state after:
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
⊢ map f ⊤ = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ ⊤ ≤ map f ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ f (x / y) * f y = f y

Tactic:
mem_ker.mp h,

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ 1 * f y = f y
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ x ∈ S, x = 1

Tactic:
simp +contextual [iff_def, S.one_mem]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ S = ⊥

Tactic:
rw [eq_bot_iff_forall]
  intro y hy
  simpa using congr_arg ((↑) : S → M) <| Subsingleton.elim (⟨y, hy⟩ : S) 1

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

Goal state before:
pp: case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b

Tactic:
simpa [pair, h] using le_trans (le_mul_self _) (Nat.le_add_right _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ Encodable (ULower α)

Tactic:
delta ULower; infer_instance

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
n : G
h : n ∈ normalClosure s
g : G
⊢ g * n * g⁻¹ ∈ normalClosure s

Tactic:
refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
    · exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
    · simp
    · rw [← conj_mul]
      exact mul_mem ihx ihy
    · rw [← conj_inv]
      exact inv_mem ihx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ StrictMono ⇑toLex

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ map (FreeMonoid.lift f) (closure (Set.range FreeMonoid.of)) = closure (Set.range f)

Tactic:
map_mclosure,

Goal state after:
M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ closure (⇑(FreeMonoid.lift f) '' Set.range FreeMonoid.of) = closure (Set.range f)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ motive x

Tactic:
have : x ∈ closure s := by simp [hs]
  induction this using closure_induction_left with
  | one => exact one
  | mul_left x hx y _ ih => exact mul_left x hx y ih

Goal state after:
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) ∈ decode (n + 1)

Tactic:
decode_option_succ,

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ (a :: tl ++ [hd]).maximum = max (↑a) (tl ++ [hd]).maximum

Tactic:
maximum_concat,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (a :: tl).maximum ↑hd = max (↑a) (tl ++ [hd]).maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (max (↑a) tl.maximum) ↑hd = max (↑a) (tl ++ [hd]).maximum

Tactic:
maximum_concat,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (max (↑a) tl.maximum) ↑hd = max (↑a) (max tl.maximum ↑hd)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
by funext s; simp [cons_swap]

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

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

Tactic:
simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _

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

Goal state before:
pp: α : 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₂
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
by funext s; simp [cons_swap]

Goal state after:
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
⊢ Disjoint (⨆ i' ∈ t, f (i, i')) (⨆ i' ∈ t, f (j, i'))

Tactic:
iSup_disjoint_iff,

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_1 ∈ t, Disjoint (f (i, i_1)) (⨆ i' ∈ t, f (j, i'))
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
⊢ Disjoint (⨆ i_1 ∈ s, f (i_1, i)) (⨆ i ∈ s, f (i, j))

Tactic:
iSup_disjoint_iff,

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_1 ∈ s, Disjoint (f (i_1, i)) (⨆ i ∈ s, f (i, j))
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ #(powersetCard n s) = 0

Tactic:
card_powersetCard,

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ (#s).choose n = 0
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ (f a✝ ⊔ s✝.sup f) = a ⊓ f a✝ ⊔ s✝.sup fun i ↦ a ⊓ f i

Tactic:
inf_sup_left,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ f a✝ ⊔ a ⊓ s✝.sup f = a ⊓ f a✝ ⊔ s✝.sup fun i ↦ a ⊓ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
⊢ ((∀ b ∈ t, f b < a) → t.sup f < a) → (∀ b ∈ cons c t hc, f b < a) → (cons c t hc).sup f < a

Tactic:
by
      simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs✝ : s.Nonempty
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : a ⊓ s✝.sup' hs f = s✝.sup' hs fun i ↦ a ⊓ f i
⊢ a ⊓ (f a✝ ⊔ s✝.sup' hs f) = a ⊓ f a✝ ⊔ s✝.sup' hs fun i ↦ a ⊓ f i

Tactic:
inf_sup_left,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs✝ : s.Nonempty
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : a ⊓ s✝.sup' hs f = s✝.sup' hs fun i ↦ a ⊓ f i
⊢ a ⊓ f a✝ ⊔ a ⊓ s✝.sup' hs f = a ⊓ f a✝ ⊔ s✝.sup' hs fun i ↦ a ⊓ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ s.sup' hs f ⊓ a = s.sup' hs fun i ↦ f i ⊓ a

Tactic:
rw [inf_comm, sup'_inf_distrib_left]

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.sup' hs fun i ↦ a ⊓ f i) = s.sup' hs fun i ↦ f i ⊓ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ ⨆ i ∈ s, i = sSup s

Tactic:
by
  rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']
  · convert! h
    rw [← sSup_range, Subtype.range_coe]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ ReflTransGen (ReflGen fun x1 x2 ↦ x1 ⋖ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
reflTransGen_reflGen

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
⊢ (ReflTransGen fun x1 x2 ↦ x1 ⋖ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2
Module: Mathlib.Order.Cover

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑a ⋖ ⊤ ↔ ∃ b, IsMax b ∧ ↑a = ↑b

Tactic:
simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
by rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Ico (n✝ - 0 - n✝) (n✝ - 0 + 1 - 0) = Ico 0 (n✝ + 1)

Tactic:
Nat.sub_zero,

Goal state after:
case succ
n✝ : ℕ
⊢ Ico (n✝ - n✝) (n✝ + 1) = Ico 0 (n✝ + 1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
wellQuasiOrdered_iff_exists_monotone_subseq

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ WellQuasiOrdered fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
rw [wellQuasiOrdered_iff_exists_monotone_subseq]

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this : ∀ (s : Finset ι) (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ioc, coe_Icc]
  exact Set.Ioc_subset_Icc_self

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ a✝ * b✝ ∈ (↑S)⁻¹

Tactic:
rw [mem_inv, mul_inv_rev]

Goal state after:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ b✝⁻¹ * a✝⁻¹ ∈ ↑S
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) →
    WellQuasiOrdered (Subrel r fun x ↦ x ∈ s)

Tactic:
wellQuasiOrdered_iff_exists_monotone_subseq

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) →
    ∀ (f : ℕ → { x // x ∈ s }), ∃ g, ∀ (m n : ℕ), m ≤ n → Subrel r (fun x ↦ x ∈ s) (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
obtain ⟨z, hxz, hz⟩ := (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 hxy

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

Tactic:
change _ * g⁻¹⁻¹ = _
  rw [inv_inv]
  rfl

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ normalizer {g}
⊢ g * h = h * g

Tactic:
exact mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H

pp: case refine_2
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ (MulAut.conj ↑h • P).subgroupOf H ≤ MulAut.conj h • P.subgroupOf H

Tactic:
· rintro - ⟨g, hg, rfl⟩
    exact ⟨g, hg, rfl⟩

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ (MulAut.conj ↑h • P).subgroupOf H ≤ MulAut.conj h • P.subgroupOf H
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Tactic:
by
  delta Finset.prod
  apply Multiset.prod_hom_rel <;> assumption

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

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ sSup s = EqvGen.setoid (sSup (@r α '' s))

Tactic:
rw [sSup_eq_eqvGen, sSup_image]

Goal state after:
α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y ↦ ∃ r ∈ s, r x y) = EqvGen.setoid (⨆ a ∈ s, ⇑a)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
have hu : s' ⊆ s := by grind

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
⊢ FreeGroup ℤ

Tactic:
revert x
    exact ↑(map fun _ => (1 : ℤ))

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
⊢ FG M → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
rw [fg_iff_exists_freeMonoid_hom_surjective]

Goal state after:
case mp
M : Type u_1
inst✝ : Monoid M
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ