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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (s.bind f) (t.bind g)

Tactic:
apply rel_join

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
Module: Mathlib.Data.List.Rotate

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

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

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ (a'' ∈ a ::ₘ a' ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)

Tactic:
rw [Multiset.cons_swap]

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ {f | ∀ (i : ι), f i ∈ t i}.Finite

Tactic:
by
  simpa [Set.pi] using Finite.pi ht

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
rw [forall_isConj]

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ (ConjClasses.mk a_1).carrier ↔ ConjClasses.mk a = ConjClasses.mk a_1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)

Tactic:
exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ H ≤ K ∨ H ≤ L

Tactic:
rw [or_iff_not_imp_left, SetLike.not_le_iff_exists, ← SetLike.coe_subset_coe]

Goal state after:
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ (∃ x, x ∈ H ∧ ¬x ∈ K) → ↑H ⊆ ↑L
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
⊢ map 1 K ≤ ⊥

Tactic:
rintro x ⟨y, _, rfl⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
y : G
left✝ : y ∈ ↑K
⊢ 1 y ∈ ⊥
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 = f y

pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ x / y ∈ f.ker

Tactic:
· rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ map f ⊤ ≤ ⊥ ↔ f = 1

Tactic:
map_le_iff_le_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ ⊤ ≤ comap f ⊥ ↔ f = 1
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
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

Tactic:
map_le_iff_le_comap,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ H ≤ comap f (map f K) ↔ H ≤ K ⊔ f.ker
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
hf : Injective ⇑f
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K

Tactic:
map_le_iff_le_comap,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
⊢ H ≤ comap f (map f K) ↔ H ≤ K
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ⊓ H₂ ≤ ⊥ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1

Tactic:
by simp only [SetLike.le_def, mem_inf, mem_bot, and_imp]

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

Goal state before:
pp: a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b

Tactic:
by_cases h₁ : a₁ < b

Goal state after:
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ pair a₁ b < pair a₂ b

case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm '' t

Tactic:
by
  rw [e.symm.image_eq_preimage_symm]; rfl

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

Goal state before:
pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2

Goal state after:
case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
v : β
htv : x.2 < v
hvu : v < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2

Goal state after:
case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
v : β
htv : x.2 < v
hvu : v < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
by
  simp [mem_sup]
  aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : α
⊢ x✝ ∈ u.toLeft → x✝ ∈ v.toLeft

Tactic:
by simpa only [mem_toLeft] using @h _

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).inf WithTop.some

Tactic:
inf_image

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.snd l.revzip = l.reverse

Tactic:
← unzip_snd,

Goal state after:
α : Type u
l : List α
⊢ l.revzip.unzip.snd = l.reverse
Module: Mathlib.Data.Finset.Max

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

Tactic:
inf_image

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s)) (min a (s.min' H))

Tactic:
rw [coe_insert]
    exact (isLeast_min' _ _).insert _

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (do
      let x ← [[], [a]]
      map (fun x_1 ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
bind_eq_flatMap,

Goal state after:
α : Type u
l : List α
a : α
⊢ flatMap (fun x ↦ map (fun x_1 ↦ x_1 ++ x) l.sublists) [[], [a]] = l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.List.Sublists

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

Tactic:
sublists'_cons

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (do
      let x ← (map f l).sublists
      [x, f a :: x]) =
    map (map f) (a :: l).sublists

Tactic:
bind_eq_flatMap,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (map f l).sublists = map (map f) (a :: l).sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (map (map f) l.sublists) =
    map (map f) do
      let x ← l.sublists
      [x, a :: x]

Tactic:
bind_eq_flatMap,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (map (map f) l.sublists) = map (map f) (flatMap (fun x ↦ [x, a :: x]) l.sublists)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ (a :: l₂✝).sublists'

Tactic:
sublists'_cons

Goal state after:
case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ (a :: l₂✝).sublists'

Tactic:
rw [sublists'_cons]
    exact ih.trans (List.sublist_append_left ..)

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

Goal state before:
pp: case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' ++ map (List.cons a) l₁✝.sublists' <+ (a :: l₂✝).sublists'

Tactic:
sublists'_cons

Goal state after:
case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' ++ map (List.cons a) l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
sublists'_cons

Goal state after:
α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ (↑s.powerset).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]
  rintro i hi j hj
  simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]
  refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩ <;>
    rintro rfl <;>
    cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ⊆ t

Tactic:
by
    rw [cons_subset_cons, map_subset_map]

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
⊢ sSup s ∈ s

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : (↑s).Nonempty
⊢ sSup ↑s ∈ ↑s
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ ⨆ i, f i ≤ a

Tactic:
exact ciSup_le' h

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ a ⩿ b ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x

Tactic:
wcovBy_iff

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⩿ x
⊢ ∃ i_1, a i_1 ⩿ Function.update a i x i_1 ∧ ∀ (j : ι), j ≠ i_1 → a j = Function.update a i x j

Tactic:
exact ⟨i, by simpa +contextual⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⋖ x
⊢ ∃ i_1, a i_1 ⋖ Function.update a i x i_1 ∧ ∀ (j : ι), j ≠ i_1 → a j = Function.update a i x j

Tactic:
exact ⟨i, by simpa +contextual⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ a ⩿ b ↔ ∃ i x, x ⩿ b i ∧ a = Function.update b i x

Tactic:
wcovBy_iff

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, x ⩿ b i ∧ a = Function.update b i x
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⩿ b i
⊢ ∃ i_1, Function.update b i x i_1 ⩿ b i_1 ∧ ∀ (j : ι), j ≠ i_1 → Function.update b i x j = b j

Tactic:
exact ⟨i, by simpa +contextual⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⋖ b i
⊢ ∃ i_1, Function.update b i x i_1 ⋖ b i_1 ∧ ∀ (j : ι), j ≠ i_1 → Function.update b i x j = b j

Tactic:
exact ⟨i, by simpa +contextual⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ ↑s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ ↑s) b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
f : ℕ → α
hStrictMono : StrictMono f
⊢ False

pp: case inr
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
f : ℕ → α
hStrictAnti : StrictAnti f
⊢ False

Tactic:
· exact not_strictMono_of_wellFoundedGT f hStrictMono

Goal state after:
case inr
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
f : ℕ → α
hStrictAnti : StrictAnti f
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Set.Ioc a b).Nonempty ↔ a < b
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_Ioc,

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

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ ↑(Ioc a b₁) ⊆ ↑(Ioo a b₂)

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ ↑(Ioo a b₂)
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:
coe_Ioc,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ {b} ∪ Set.Ico a b = Set.Icc a b

Tactic:
Set.union_comm,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Set.Ico a b ∪ {b} = Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a ↑(Ioc a b) = ↑(Icc a b)

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Set.Ioc a b) = ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ {a} ∪ Set.Ioc a b = Set.Icc a b

Tactic:
Set.union_comm,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Set.Ioc a b ∪ {a} = Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ {a} ∪ Set.Ioo a b = Set.Ico a b

Tactic:
Set.union_comm,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ Set.Ioo a b ∪ {a} = Set.Ico a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Set.Ioo a b) = ↑(Ioc a b)

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Set.Ioo a b) = Set.Ioc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ {b} ∪ Set.Ioo a b = Set.Ioc a b

Tactic:
Set.union_comm,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ Set.Ioo a b ∪ {b} = Set.Ioc a b
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case h
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)
⊢ r ^ ny • (y * r ^ nx • x) ∈ closure (r • s)

Tactic:
← smul_mul_assoc

Goal state after:
case h
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)
⊢ r ^ ny • y * r ^ nx • x ∈ closure (r • s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
j : ι
hj : j ∈ s
hi : f j ∈ image f s
⊢ f j ≤ s.sup f

Tactic:
exact le_sup hj

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ ↑(Ioc a b) ∪ ↑(Ioc b c) = ↑(Ioc a c)

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a b ∪ ↑(Ioc b c) = ↑(Ioc a c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a b ∪ ↑(Ioc b c) = ↑(Ioc a c)

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a b ∪ Set.Ioc b c = ↑(Ioc a c)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a b ∪ Set.Ioc b c = ↑(Ioc a c)

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ a ∈ f ⁻¹' f '' U

Tactic:
rw [Set.mem_preimage, Set.mem_image]

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ ∃ x ∈ U, f x = f a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_2
α : 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' : ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} fun n ↦ if n < g 0 then f n else (f (g (n - g 0))).tail
⊢ False

Tactic:
IsBadSeq

Goal state after:
case inr.refine_2
α : 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))
⊢ False