mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
rw [sublists'Aux, Array.foldl_toList]

Goal state after:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ Array.foldl (fun r l ↦ r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x

Tactic:
refine ne_of_eq_of_ne (coe_max' s0).symm ?_
    exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)

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

Goal state before:
pp: case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t

Tactic:
intro h

Goal state after:
case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s

Tactic:
intro h

Goal state after:
case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (hd' :: tl', tail)

Tactic:
intro h

Goal state after:
case mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
Module: Mathlib.Data.List.Sublists

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

Tactic:
Nat.choose_succ_succ,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose (n + 1) + l.length.choose n = l.length.choose n + l.length.choose n.succ
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
h✝ : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ powersetCard n ↑l₁ ≤ powersetCard n ↑l₂

Tactic:
by
    simp only [powersetCard_coe, coe_le]
    exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm

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

Goal state before:
pp: α : Type u
l : List α
⊢ (finRange l.length).sublists.Nodup

Tactic:
exact nodup_sublists.mpr (nodup_finRange _)

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

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ (∅.sup fun b ↦ f b \ a) = ∅.sup f \ a

Tactic:
rw [sup_empty, sup_empty, bot_sdiff]

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

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

Tactic:
intro h

Goal state after:
case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
Module: Mathlib.Data.Finset.Powerset

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

Tactic:
rintro ⟨y, ⟨hyt, hyn⟩, rfl⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ (y ∪ s ⊆ t ∧ #(y ∪ s) = n) ∧ s ⊆ y ∪ s
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
⊢ P (ULift.{u, 0} (Fin (card α))) → Trunc (P α)

Tactic:
intro h

Goal state after:
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
⊢ Trunc (P α)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
⊢ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t
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 ∧ #t = n

Tactic:
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: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ ⨆ (h : p), f h = sSup ∅

Tactic:
by
  rw [iSup]
  congr
  rwa [range_eq_empty_iff, isEmpty_Prop]

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite
⊢ ∀ i ∉ {i | (s i).Nonempty}, s i = ∅

Tactic:
by simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a

Tactic:
intro h

Goal state after:
case mp
ι : 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 ∈ s, f x < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i → ∀ x ∈ s, a < f x

Tactic:
intro h

Goal state after:
case mp
ι : 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 ∈ s, a < f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ x, ∀ y ∈ range f, y ≤ x
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ∃ x, ∀ y ∈ range fun b ↦ ⨆ c, f (b, c), y ≤ x

Tactic:
obtain ⟨B, hB⟩ := hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∃ x, ∀ y ∈ range fun b ↦ ⨆ c, f (b, c), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ x, ∀ y ∈ range f, y ≤ x
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
⊢ ∃ x, ∀ y ∈ range fun c ↦ f (b, c), y ≤ x

Tactic:
obtain ⟨B, hB⟩ := hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∃ x, ∀ y ∈ range fun c ↦ f (b, c), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : b = x), f x h

Tactic:
refine le_ciSup₂ ⟨f b rfl, ?_⟩ b rfl
  rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩
  rfl

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y → x.1 = y.1 ∨ x.2 = y.2

Tactic:
intro h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
h : x ⩿ y
⊢ x.1 = y.1 ∨ x.2 = y.2
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
i : ι
hi : ↑r < ↑(f i)
⊢ ∃ y ∈ range f, r < y

Tactic:
exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1

Tactic:
cases x

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⩿ y ↔ (fst✝, snd✝).1 ⩿ y.1 ∧ (fst✝, snd✝).2 = y.2 ∨ (fst✝, snd✝).2 ⩿ y.2 ∧ (fst✝, snd✝).1 = y.1
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1

Tactic:
cases x

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⋖ y ↔ (fst✝, snd✝).1 ⋖ y.1 ∧ (fst✝, snd✝).2 = y.2 ∨ (fst✝, snd✝).2 ⋖ y.2 ∧ (fst✝, snd✝).1 = y.1
Module: Mathlib.Order.Cover

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

Tactic:
intro h

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Cover

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

Tactic:
intro h

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := ⋯
⊢ ↑((t.preimage Subtype.val ⋯).sup id) = ↑⟨t.sup id, ⋯⟩

Tactic:
simp only [sup_coe, id_eq]

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
⊢ ((t.preimage Subtype.val ⋯).sup fun x ↦ ↑x) = t.sup id
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ ¬Minimal P x ↔ ∃ y, y < x ∧ P y

Tactic:
not_minimal_iff hx,

Goal state after:
α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ (∃ y, P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ y, y < x ∧ P y
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
by
  refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
  · obtain ⟨y, hyx, hy⟩ := h h'.prop
    rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]
  obtain ⟨z, hzy, hz⟩ := h hy
  exact (h'.le_of_le hz (hzy.trans hyx)).trans hzy

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
⊢ Minimal (fun x ↦ x ∈ f '' s) (f x)

Tactic:
by
  refine ⟨mem_image_of_mem f hx.prop, ?_⟩
  rintro _ ⟨y, hy, rfl⟩
  rw [hf hx.prop hy, hf hy hx.prop]
  exact hx.le_of_le hy

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = (⨆ k, ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)

Tactic:
← Nat.lt_succ_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < (n + 1).succ), u k = (⨆ k, ⨆ (_ : k < n.succ), u k) ⊔ u (n + 1)
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)

Tactic:
← Nat.lt_succ_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < (n + 1).succ), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n.succ), u (k + 1)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
⊢ ℕ ≃o ↑s

Tactic:
classical
  exact
    RelIso.ofSurjective
      (RelEmbedding.orderEmbeddingOfLTEmbedding
        (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
      Nat.Subtype.ofNat_surjective

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

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ⊤

Tactic:
cases x

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ ≤ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ ≤ ⊤
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }
    by_cases hbad : Infinite bad
    · refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
      have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
      rw [Nat.orderEmbeddingOfSet_range bad] at h
      exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
    · rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
      obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
      have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_ofPred_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia
      let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
      exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

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

Goal state before:
pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ↑a✝

Tactic:
cases x

Goal state after:
case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ ≤ ↑a✝

case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ x ∧ x ≤ ⊤

Tactic:
cases x

Goal state after:
case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ ⊤ ∧ ⊤ ≤ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ ↑a✝ ∧ ↑a✝ ≤ ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ x ∧ x ≤ ↑a✝

Tactic:
cases x

Goal state after:
case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ ⊤ ∧ ⊤ ≤ ↑a✝

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝² ≤ ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ⊤

Tactic:
cases x

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
⊢ (⊤ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ < ⊤

case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ < ⊤
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ↑a✝

Tactic:
cases x

Goal state after:
case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ⊤ ∧ ⊤ < ↑a✝

case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ ↑a✝ ∧ ↑a✝ < ↑a✝¹