mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
by ext i; exact pow_left_injective hn <| congr_fun hab i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ a ∈ s, f a '' t = image2 f s t

Tactic:
by
  simp only [image2_eq_iUnion, image_eq_iUnion]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ∃ a, ↑u = {a} ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b * a} = {1}
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
motive : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ motive x

Tactic:
by
  induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | one => exact one
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a

Tactic:
change a ∈ Set.ofPred IsUnit ↔ IsUnit a
  rw [Set.mem_ofPred_eq]

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:
by
  rw [eq_top_iff]
  intro x _
  obtain ⟨y, hy⟩ := h x
  exact ⟨y, trivial, hy⟩

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

Goal state before:
pp: case refine_1.refine_4
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
rintro _ _ ⟨i, hi', hi⟩

Goal state after:
case refine_1.refine_4
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x✝ : G
hx✝ : x✝ ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
i : ι
hi' : p i
hi : x✝ ∈ K i
⊢ ∃ i, p i ∧ x✝⁻¹ ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ Injective ⇑f.rangeRestrict ↔ Injective ⇑f

Tactic:
convert! Set.injective_codRestrict _

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
by_cases h : p <;>
  simp +contextual [h]

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

Goal state before:
pp: n : ℕ
⊢ (unpair n).2 ≤ n

Tactic:
by
  simpa using right_le_pair n.unpair.1 n.unpair.2

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H

Tactic:
exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
apply forall_congr'

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ∀ (a : Subgroup G), a < ⊤ → a < normalizer ↑a ↔ normalizer ↑a = a → a = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ H.normalCore ≤ map (↑(MulAut.conj g)) H

Tactic:
grw [← Normal.map_conj_eq H.normalCore g, normalCore_le]

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

Goal state before:
pp: case cons_cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ a * l₁✝.prod ≤ a * l₂✝.prod

Tactic:
ih' h₁.2

Goal state after:
case cons_cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ a * l₂✝.prod ≤ a * l₂✝.prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
by_cases h : p <;>
  simp +contextual [h]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)

Tactic:
· suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

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

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m

Tactic:
intro b

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
⊢ ∀ {m : α} {o : Option α}, b ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r b m
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode (n + 1), encode a = n + 1

Tactic:
refine ⟨some (ofNat α n), ?_, ?_⟩

Goal state after:
case succ.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (ofNat α n) ∈ decode (n + 1)

case succ.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (some (ofNat α n)) = n + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
val✝ : α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) (some val✝) = max (some val✝) ↑a

Tactic:
· simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toLeft + #u.toRight = #u

Tactic:
← card_disjSum,

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #(u.toLeft.disjSum u.toRight) = #u
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists'.length = 2 ^ (a :: l).length

Tactic:
by
    simp +arith only [sublists'_cons, length_append, length_sublists' l,
      length_map, length, Nat.pow_succ']

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ List.map ofList l₁✝.sublists' <+ List.map ofList l₂✝.sublists'

Tactic:
apply Sublist.map

Goal state after:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ l₁✝.sublists' <+ l₂✝.sublists'
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (x ⊆ t ∧ #x = n) ∧ s ⊆ x → ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x

Tactic:
intro ⟨⟨hxt, hxn⟩, hsx⟩

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun a ↦ count b (f a)

Tactic:
rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]

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

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

Tactic:
have := hne.to_subtype

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (⋃ i, s i).Finite ↔ ∀ (i : ι), (s i).Finite

Tactic:
← iUnion_plift_down,

Goal state after:
α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (⋃ i, s i.down).Finite ↔ ∀ (i : ι), (s i).Finite
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(f i)

Tactic:
apply biInf_le _ h

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

Goal state before:
pp: case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, ⨅ i ∈ insert a✝¹ s✝, f i j = ⨅ i ∈ insert a✝¹ s✝, ⨆ j, f i j

Tactic:
simp only [iInf_insert, ← ihs hf.2]

Goal state after:
case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : Monotone (f a✝¹) ∧ ∀ x ∈ s✝, Monotone (f x)
⊢ ⨆ j, f a✝¹ j ⊓ ⨅ x ∈ s✝, f x j = (⨆ j, f a✝¹ j) ⊓ ⨆ j, ⨅ i ∈ s✝, f i j
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

Goal state after:
α : 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
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
Module: Mathlib.Order.Cover

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⩿ s

Tactic:
convert! wcovBy_insert a _
    ext
    simp [ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
rw [← sup_congr (Eq.refl s) hfinvs, ← sup_image]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = (image (invFunOn f (f ⁻¹' ↑s)) s).sup f
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
inst✝ : LE α
x : Subtype P
⊢ Minimal (fun x ↦ True) x ↔ Minimal P ↑x

Tactic:
by
  obtain ⟨x, hx⟩ := x
  simp [Minimal, hx]

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

Goal state before:
pp: case h
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
⊢ IsTop a

Tactic:
intro b

Goal state after:
case h
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
b : α
⊢ b ≤ a
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
· obtain ⟨a, ha⟩ := hs.exists_maximal hn
    use {a}
    suffices IsTop a by simpa [IsCofinal]
    intro b
    obtain ⟨c, hc, hbc⟩ := hs' b
    exact hbc.trans (ha.le hc)

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

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

Tactic:
Finset.mem_Icc

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
    induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

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

Goal state before:
pp: a x : ℕ
⊢ 1 ≤ x ∧ x ≤ a ↔ x ∈ Icc 1 a

Tactic:
Finset.mem_Icc

Goal state after:
a x : ℕ
⊢ 1 ≤ x ∧ x ≤ a ↔ 1 ≤ x ∧ x ≤ a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
← coe_eq_empty,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Icc a b) = ∅ ↔ ¬a ≤ b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
← coe_eq_empty,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ico a b) = ∅ ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
⊢ m ≥ n → P m

Tactic:
hm

Goal state after:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm : m ≥ n
⊢ P m
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b = ∅ ↔ ¬a < b

Tactic:
← coe_eq_empty,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Ioc a b) = ∅ ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
← coe_eq_empty,

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ ↑(Ioo a b) = ∅ ↔ ¬a < b
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a

Tactic:
have : WellQuasiOrderedLE α := ⟨h⟩

Goal state after:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
this : WellQuasiOrderedLE α
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
← coe_eq_empty,

Goal state after:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ ↑(Ioi a) = ∅ ↔ IsMax a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
rw [cons_eq_insert, Ioc_insert_left h]

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),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)

pp: case refine_2
ι : 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)
⊢ ∀ (a : ι) (s_1 : Finset ι) (h : a ∉ s_1),
    (∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s_1, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
          ∃ g, ∀ ⦃a_3 b : ℕ⦄, a_3 ≤ b → ∀ i ∈ Finset.cons a s_1 h, r i ((f ∘ ⇑g) a_3 i) ((f ∘ ⇑g) b i)

Tactic:
· intro f hf
    exists RelEmbedding.refl (· ≤ ·)
    simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

Goal state after:
case refine_2
ι : 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)
⊢ ∀ (a : ι) (s_1 : Finset ι) (h : a ∉ s_1),
    (∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s_1, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
          ∃ g, ∀ ⦃a_3 b : ℕ⦄, a_3 ≤ b → ∀ i ∈ Finset.cons a s_1 h, r i ((f ∘ ⇑g) a_3 i) ((f ∘ ⇑g) b i)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ s.IsPWO ↔ s.IsWF

Tactic:
change WellQuasiOrdered (· ≤ ·) ↔ WellFounded (· < ·)
  rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ 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.lt_of_not_ge hxy'

Goal state after:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
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.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r ((f (g (m - g 0))).head! :: (f (g (m - g 0))).tail) (f (g n'))

Tactic:
← List.cons_head!_tail (hnil (g n'))

Goal state after:
case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r ((f (g (m - g 0))).head! :: (f (g (m - g 0))).tail) ((f (g n')).head! :: (f (g n')).tail)
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ fixedPoints (ConjAct G) G = ↑(center G)

Tactic:
by
  ext x
  simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]

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

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
m : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, x = m
⊢ noncommProd ⟦a✝⟧ comm = m ^ card ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
m : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ a✝, x = m
⊢ a✝.prod = m ^ a✝.length
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ ∀ b ∈ s.erase a, Commute a b

Tactic:
intro b

Goal state after:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
b : α
⊢ b ∈ s.erase a → Commute a b
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
⊢ p (s.noncommProd f comm)

Tactic:
by
  refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_
  obtain (⟨a, ha : a ∈ s, rfl : f a = b⟩) := by simpa using hb
  exact base a ha

Goal state after: