mathlib-initiative/mathlib-tactics huggingface dataset:
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

pp: case neg
ι : 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:
·

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
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case neg
ι : 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:
·

Goal state after:
case neg
ι : 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
Module: Mathlib.Order.Minimal

Goal state before:
pp: case inl
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

pp: case inr
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : Q x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
·

Goal state after:
case inl
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x ↦ P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x
Module: Mathlib.Order.Minimal

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

pp: case refine_2
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
⊢ Q x
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

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:
·

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t
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:
·

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

pp: case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ y ≤ x → x ≤ y

pp: case refine_2
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ f x ∈ t) x
⊢ ∀ ⦃y : β⦄, (fun x ↦ x ∈ t ∩ range ⇑f) y → y ≤ f x → f x ≤ y

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ y ≤ x → x ≤ y
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
by rw [Ici, ← Finset.mem_def, Finset.mem_Ici]

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

Goal state before:
pp: case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s

pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1

Tactic:
·

Goal state after:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1

Tactic:
·

Goal state after:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = ?m.40 + 1

Tactic:
·

Goal state after:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1

Tactic:
·

Goal state after:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1

Tactic:
·

Goal state after:
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b c : ℕ
a : ↥(Ioc b (b + 1))
⊢ b < b + 1 ∧ b + 1 ≤ b + 1

Tactic:
by lia

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

Goal state before:
pp: s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find ⋯

pp: case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n

Tactic:
·

Goal state after:
s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find ⋯
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n

Tactic:
·

Goal state after:
case hnc
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ a ∈ s, a ≤ n
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
·

Goal state after:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ (a ≤ x + c ∧ x + c < b) ∧ x + c - c = x

Tactic:
by lia

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

Goal state before:
pp: case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}

pp: case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}

Tactic:
·

Goal state after:
case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
·

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
a b x : α
⊢ x ∈ h₀_finset_Ico a b ↔ x ∈ h₁_finset_Ico a b

Tactic:
rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]

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

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
x : ℕ
h : c + 1 - b ≤ x ∧ x < c + 1 - a
⊢ (a ≤ c - x ∧ c - x < b) ∧ c - (c - x) = x

Tactic:
by lia

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

Goal state before:
pp: a b : ℕ
h : a ≤ b
⊢ Ico a b.succ = insert b (Ico a b)

Tactic:
ext x
  simp_rw [mem_insert, mem_Ico]
  lia

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

Goal state before:
pp: case refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}

pp: case refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}

Tactic:
·

Goal state after:
case refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}

Tactic:
·

Goal state after:
case refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
⊢ n ≤ n + a

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inl.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a

pp: case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

pp: case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
·

Goal state after:
case succ.inl.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

pp: case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
·

Goal state after:
case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

pp: case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
·

Goal state after:
case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : ¬hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : ¬hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : ¬hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
·

Goal state after:
case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inl
n : ℕ
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = range 0

pp: case inr
n a : ℕ
ha : a ≠ 0
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = range a

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = range 0
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ n < n + n' - n - m

Tactic:
by lia

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

Goal state before:
pp: case inr.mp
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a

pp: case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Tactic:
·

Goal state after:
case inr.mp
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

pp: case inr.mpr.inr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)
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))

pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
·

Goal state after:
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))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a
Module: Mathlib.Order.OrderIsoNat

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hIncreasing : ∀ (m n : ℕ), m < n → f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

pp: case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hIncreasing : ∀ (m n : ℕ), m < n → f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
⊢ StrictMono (⇑f ∘ ⇑g) ∨ StrictAnti (⇑f ∘ ⇑g)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr.refine_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
m n : ℕ
hmn : m < n
⊢ (⇑f ∘ ⇑g) n ≤ (⇑f ∘ ⇑g) m

pp: case inr.refine_2
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
m n : ℕ
hmn : m < n
⊢ n ≠ m

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
m n : ℕ
hmn : m < n
⊢ (⇑f ∘ ⇑g) n ≤ (⇑f ∘ ⇑g) m
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr.refine_2
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
m n : ℕ
hmn : m < n
⊢ n ≠ m

Tactic:
·

Goal state after:
case inr.refine_2
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
f : ℕ ↪ α := natEmbedding α
g : ℕ ↪o ℕ
hNonincreasing : ∀ (m n : ℕ), m < n → ¬f (g m) < f (g n)
m n : ℕ
hmn : m < n
⊢ n ≠ m
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
·

Goal state after:
case inr.mpr.inr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i