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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ (a : G), (a ∈ H ↔ f.symm x * a * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a) ∈ H ↔ f.symm (x * f.toEquiv a * x⁻¹) ∈ H)

Tactic:
intro

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
a✝ : G
⊢ (a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a✝) ∈ H ↔ f.symm (x * f.toEquiv a✝ * x⁻¹) ∈ H)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
hH : H.Normal
f : G →* N
x✝ : G
⊢ x✝ ∈ Subgroup.comap f H → ∀ (g : G), g * x✝ * g⁻¹ ∈ Subgroup.comap f H

Tactic:
by simp +contextual [Subgroup.mem_comap, hH.conj_mem]

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

Goal state before:
pp: α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ a • s / b • t = (a / b) • (s / t)

Tactic:
← image_smul,

Goal state after:
α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ (fun x ↦ a • x) '' s / (fun x ↦ b • x) '' t = (fun x ↦ (a / b) • x) '' (s / t)
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
← op_closure

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : x ∈ closure s
m : Mᵐᵒᵖ
hm : m ∈ (closure s).op
⊢ MulOpposite.unop m ∈ closure s
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
← op_closure

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : x ∈ closure s
⊢ { unop' := x } ∈ (closure s).op
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ ∀ {a_1 b : M}, a_1 ∈ {1, a} → b ∈ {1, a} → a_1 * b ∈ {1, a}

Tactic:
rintro _ _ (rfl | rfl) (rfl | rfl)

Goal state after:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ 1 * b✝ ∈ {1, b✝}

case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
z : α
⊢ (1 • y) • z = 1 • y • z

Tactic:
rw [one_smul, one_smul]

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

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ 1 • y • z = y • 1 • z

Tactic:
rw [one_smul, one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l) → m ∈ argmax f l

Tactic:
by
      rintro ⟨hml, ham, hma⟩
      rcases harg : argmax f l with - | n
      · simp_all
      · have :=
          Nat.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
            (index_of_argmax harg hml (ham _ (argmax_mem harg)))
        rw [(idxOf_inj hml).1 this, Option.mem_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
by
  simp_rw [disjoint_left, mem_map]
  rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l l' : List α
h : l ~ l'
⊢ l.maximum = l'.maximum

Tactic:
induction h with grind [maximum_cons]

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

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

Tactic:
min_eq_inf_withTop,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = (image (⇑ofDual) s).inf WithTop.some
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min

Tactic:
min_eq_inf_withTop,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).inf WithTop.some
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ sublistsLen 1 (a :: s) = map (fun x ↦ [x]) (a :: s).reverse

Tactic:
sublistsLen_succ_cons,

Goal state after:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ sublistsLen (0 + 1) s ++ map (cons a) (sublistsLen 0 s) = map (fun x ↦ [x]) (a :: s).reverse
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)

Tactic:
sublistsLen_succ_cons,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) <+ (a :: l).sublists'

Tactic:
sublistsLen_succ_cons,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ (a :: l).sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ l'.length = n + 1

Tactic:
sublistsLen_succ_cons,

Goal state after:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
⊢ l'.length = n + 1
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)

Tactic:
induction s using Multiset.induction generalizing n with

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

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++ flatMap (fun a ↦ sublistsLen a.succ (h :: tl)) (range (tl.length + 1)) ~
    (h :: tl).sublists'

Tactic:
sublistsLen_succ_cons,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++
      flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    (h :: tl).sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
⊢ (s ×ˢ t).PairwiseDisjoint f

Tactic:
rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ (∀ x ∈ ∅, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, ∅.sup id ≤ x

Tactic:
simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff,
        sup_empty, forall_true_iff, notMem_empty]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst✝ : Finite ι
this : Fintype (PLift ι)
⊢ Finite ↑(range f)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ≠ s ∧ t ⊆ s ↔ t ⊂ s

Tactic:
ssubset_iff_subset_ne,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ≠ s ∧ t ⊆ s ↔ t ⊆ s ∧ t ≠ s
Module: Mathlib.Data.Set.Pairwise.Lattice

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

Tactic:
exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')

Tactic:
by
  refine
      ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩ <;>
    simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff] <;>
    intro i' hi' j' hj'
  · exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)
  · exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ f b \ a) = s✝.inf f \ a
⊢ ((cons a✝ s✝ h✝).inf fun b ↦ f b \ a) = (cons a✝ s✝ h✝).inf f \ a

Tactic:
rw [inf_cons, inf_cons, ih, inf_sdiff]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a < s.sup (WithBot.some ∘ f) ↔ ∃ b ∈ s, a < f b

Tactic:
Finset.lt_sup_iff

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : IsEmpty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

Tactic:
· rw [iSup_of_empty']

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ x, t ↑x)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ x ∈ range f, ↑x).Finite

Tactic:
exact h.biUnion fun y _ => y.finite_toSet

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

Goal state before:
pp: case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t

Tactic:
· rintro ⟨i, -, H⟩
      exact H

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ (range fun i ↦ ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}

Tactic:
intro

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sSup ∅}
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ (range fun i ↦ ⨅ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sInf ∅}

Tactic:
intro

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sInf ∅}
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case h_empty
α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
inst✝ : Finite ι
κ : PEmpty.{v + 1} → Type w
f : (a : PEmpty.{v + 1}) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
| h_empty =>

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
⊢ ⨅ i, f i = n ↔ (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
by
  have : OrderBot α := WellFoundedLT.toOrderBot α
  constructor
  · rintro rfl
    exact ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩
  · rintro ⟨⟨i, rfl⟩, h⟩
    exact le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

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

Goal state before:
pp: case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)) →
    x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩

Tactic:
rintro ⟨⟨⟩, ⟨⟩, hx⟩

Goal state after:
case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ x ∈ sigmaLift f ⟨x.1, a⟩ ⟨x.1, b⟩
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1

Tactic:
refine ⟨i, mem_cons_self .., ?_⟩

Goal state after:
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∀ ⦃j : ι⦄, (fun x ↦ x ∈ cons i s hi) j → f i ≤ f j → f j ≤ f i
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ {x ∈ Finset.Ico a b | b ≤ x}.val = ∅

Tactic:
Finset.Ico_filter_le_of_right_le

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ ∅.val = ∅
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
⊢ Unique ↥(Iic ⊥)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
⊢ ¬Infinite α

Tactic:
intro

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
  · refine ⟨g, fun m n hle => ?_⟩
    obtain hlt | rfl := hle.lt_or_eq
    exacts [h1 m n hlt, refl_of r _]
  · obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)
    cases h2 m n hlt hle

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ i ∈ ∅,
        r i ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) a i) ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) b i)

Tactic:
simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : OrderBot α
⊢ Unique ↥{⊥}

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ i ∈ ∅,
        r i ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) a i) ((f ∘ ⇑(RelEmbedding.refl fun x1 x2 ↦ x1 ≤ x2)) b i)

Tactic:
simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Ioc_eq_empty_iff,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : ℕ → α
⊢ ((∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ¬IsBadSeq r s f

Tactic:
by simp [IsBadSeq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ SMulCommClass (↥(center M)) (↥(center M)) M

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
⊢ center ((i : ι) → A i) = univ.pi fun i ↦ center (A i)

Tactic:
classical
  ext x
  simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
  refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
  exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {↑x}))ˣ
⊢ ConjAct.toConjAct ((Units.map (Submonoid.centralizer {↑x}).subtype) u) • x = x

Tactic:
simp only [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul]

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {↑x}))ˣ
⊢ (Units.map (Submonoid.centralizer {↑x}).subtype) u * x = x * (Units.map (Submonoid.centralizer {↑x}).subtype) u
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
← op_closure

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

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

Tactic:
← op_closure

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
⊢ { unop' := x } ∈ (closure s).op
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x y : G
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
ihx : C x
ihy : C y
⊢ C (x * y)

Tactic:
| mul x y _ _ ihx ihy =>

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g * n * g⁻¹ ∈ H

Tactic:
← h g,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g * n * g⁻¹ ∈ MulAut.conj g • H
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

Tactic:
by
  simpa only [disjoint_comm (a := a)] using disjoint_list_sum_left

Goal state after: