mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
⊢ Injective fun g ↦ ↑g.1 * ↑g.2

Tactic:
by
  intro x y hxy
  rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
  replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
  rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy

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
y : M
hy : y ∈ S
⊢ y = 1

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

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 [← iInf_subtype'', characteristic_iInf, h]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(map (↑(MulAut.conj h)) (closure s))

Tactic:
exact fun g hg ↦ ⟨_, hH _ (inv_mem hh) g hg, by simp [mul_assoc]⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
x✝² x✝¹ : α
x✝ : Set β
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
simp only [← image_smul, image_image, ← mul_smul]

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
a b : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
hb : b ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ (a * b) • x - x ∈ I

Tactic:
by simpa [mul_smul] using add_mem (ha (b • x)) (hb x)

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hl_nonempty : l ≠ []
hl : ∀ (a : α), a ∈ l → p a
⊢ f l.prod ≤ (map f l).prod

Tactic:
induction l with
  | nil => simp at hl_nonempty
  | cons a l ih =>
    rw [prod_cons, map_cons, prod_cons]
    by_cases hl_empty : l = []
    · simp [hl_empty]
    have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
    have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
    have hp_a : p a := hl a mem_cons_self
    grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]

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

Goal state before:
pp: case mp
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

pp: case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b

Tactic:
· rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
    · exact Or.inl hij
    · exact Or.inr ⟨rfl, hab⟩

Goal state after:
case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

Tactic:
simpa using h.symm.ne_of_mem ha hb

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

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
← Set.singleton_union,

Goal state after:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure ({a} ∪ {b}) ↔ ∃ m n, a ^ m * b ^ n = c
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
⊢ encode (ofNat α n) = n

Tactic:
obtain ⟨a, h, e⟩ := decode_inv (α := α) n
  rwa [ofNat_of_decode h]

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:
rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]

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

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (max a b) = f a ⊔ f b

pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b

Tactic:
· rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = s.inf (WithTop.some ∘ ⇑ofDual)

Tactic:
exact congr_fun WithTop.map_id _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = s.inf (WithTop.some ∘ ⇑toDual)

Tactic:
exact congr_fun WithTop.map_id _

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)

Tactic:
by
  simp [powersetAux']

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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ f a

Tactic:
rw [hfa]

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ (image f s).max' hne
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) l'.revzip (List.map (fun x ↦ (x, ↑l - x)) l')

Tactic:
forall₂_map_right_iff

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun a c ↦ a = (c, ↑l - c)) l'.revzip l'
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
by
  have := Classical.decEq α
  rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
  exact powersetAux_perm_powersetAux'.map _

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

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetCardAux n l ↔ ⟦a⟧ ≤ ↑l ∧ card ⟦a⟧ = n

Tactic:
simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
      coe_eq_coe, coe_le, Subperm, coe_card]
    exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

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

Goal state before:
pp: α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux n l₁ ~ powersetCardAux n l₂

Tactic:
by
  induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
  induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    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 _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

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 : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False

Tactic:
exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ {x ∈ s | f x ∈ t} ⊆ s ∧ #({x ∈ s | f x ∈ t}) = n

Tactic:
rw [← card_map f, this, h.2]

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ {x ∈ s | f x ∈ t} ⊆ s ∧ n = n
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

Tactic:
rw [iSup_of_empty', iSup_of_empty']

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

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

Tactic:
exact @Set.fintypeiUnion _ _ _ _ _ H

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

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

Tactic:
rw [iSup_of_empty', iSup_of_empty']

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x✝ : α
⊢ x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)

Tactic:
simpa using le_ciInf_iff hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
have := hne.to_subtype
  rw [image_eq_range] at hf
  exact gc.l_ciSup hf

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case inr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ≤ b ∧ b ≤ a
inhabited_h : Inhabited ι
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
exact ⟨default, fun j hj ↦ ⟨h.left j, h.right j⟩⟩

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case singleton
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Finset ι
i : ι
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ {i}) f i_1

Tactic:
exact ⟨i, by simp⟩

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
by rintro rfl; rfl

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
by rintro rfl; rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c

Tactic:
add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl),

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ List.range' a (b + 1 - a) ↔ a ≤ x ∧ x ≤ b

Tactic:
List.mem_range'_1

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ List.range' a (b - a) ↔ a ≤ x ∧ x < b

Tactic:
List.mem_range'_1

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ List.range' (a + 1) (b - a) ↔ a < x ∧ x ≤ b

Tactic:
List.mem_range'_1

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ List.range' (a + 1) (b - a - 1) ↔ a < x ∧ x < b

Tactic:
List.mem_range'_1

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x

Tactic:
by rw [mem_filter, mem_Ici, lt_iff_le_and_ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }

Tactic:
have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
hIoi : h₀_finset_Ioi = h₁_finset_Ioi
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
⊢ s.Finite

Tactic:
by
  by_contra! hi
  obtain ⟨m, n, hmn, h⟩ := hr fun n => hi.natEmbedding _ n
  exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    hs.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : s.WellFoundedOn r
ht : t.WellFoundedOn r
⊢ (s ∪ t).WellFoundedOn r

Tactic:
rw [wellFoundedOn_iff_no_descending_seq] at *

Goal state after:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
⊢ ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s ∪ t
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case mul
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝ : x ∈ closure s
hy✝ : y ∈ closure s
hx : ∃ n, r ^ n • x ∈ closure (r • s)
hy : ∃ n, r ^ n • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)

Tactic:
obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy

Goal state after:
case mul
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝¹ : x ∈ closure s
hy✝¹ : y ∈ closure s
hx✝ : ∃ n, r ^ n • x ∈ closure (r • s)
hy✝ : ∃ n, r ^ n • y ∈ closure (r • s)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u_1
γ : Type u_2
α : Type u_3
inst✝² : SMul γ α
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ m • m' • a = a

Tactic:
hb,

Goal state after:
M : Type u_1
γ : Type u_2
α : Type u_3
inst✝² : SMul γ α
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ m • a = a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ (WellQuasiOrdered fun x1 x2 ↦ x1 ≤ x2) ↔ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
← wellQuasiOrderedLE_def,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ WellQuasiOrderedLE { x // x ∈ s } ↔ WellFounded fun x1 x2 ↦ x1 < x2
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a : N), Commute (e x) a

Tactic:
(intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm])

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

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (b c : N), e x * (b * c) = e x * b * c

Tactic:
(intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm])

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

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)

Tactic:
(intros; apply e.symm.injective; simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm])

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Tactic:
Set.mem_center_iff,

Goal state after:
M : Type u_2
inst✝ : Mul M
x : M
⊢ IsMulCentral (op x) ↔ IsMulCentral x
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H * ↑N
⊢ x⁻¹ ∈ ↑H * ↑N

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := hx
    simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f g h i : ι → M
⊢ (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a

Tactic:
by
  simp_rw [prod_mul_distrib, mul_mul_mul_comm]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ ⦃a b : List (α × Bool)⦄, Red.Step a b → Red.Step (invRev a) (invRev b)

Tactic:
by
        intro a b h
        cases h
        simp [invRev]

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

Goal state before:
pp: case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℕ
hx : (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) ↑x) = ↑x
⊢ (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) (↑x + 1)) = ↑x + 1

Tactic:
simpa [zpow_add_one] using hx

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ closure ↑(Finset.univ.biUnion fun i ↦ Finset.image (⇑(MonoidHom.mulSingle M i)) (s i)) = Submonoid.pi Set.univ P

Tactic:
simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
⊢ Function.RightInverse ⇑(lift (MonoidHom.id H)) ⇑of

Tactic:
by
      rintro ⟨a⟩
      rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
x : α
⊢ (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)

Tactic:
simp only [lift_apply_of, Pi.add_apply]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y : FreeAbelianGroup α
s : α
⊢ of s * y = y * of s

Tactic:
| of s =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁ = g₂ → g₁.trans f = g₂.trans f

Tactic:
by rintro rfl; rfl

Goal state after: