awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n ≤ i + a * (n / a + 1)
inr₁ : i + a * (n / a + 1) < n + a
inr₂ : (i + a * (n / a + 1)) % a = i
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n ≤ i + a + a * (n / a)
⊢ n ≤ i + a * (n / a + 1)

Tactic:
rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]

Premises used: add_assoc, HDiv.hDiv, add_comm, mul_one, Nat.mul_add
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)

Tactic:
hn.symm.le.trans (Nat.add_le_add_right ?_ _)

Premises used: Nat.add_le_add_right, Eq.le, LE.le.trans, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n % a ≤ i + a
⊢ n ≤ i + a + a * (n / a)

Tactic:
refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)

Premises used: Nat.add_le_add_right, Eq.le, LE.le.trans, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a

Tactic:
simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le

Premises used: Nat.zero_le, LT.lt.le, zero_add, Nat.mod_lt, Nat.add_le_add, Ne.bot_lt
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
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

Tactic:
lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Nat.add_lt_add_right, lt_of_lt_of_le
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n % a + a * (n / a + 1) ≤ n + a
⊢ i + a * (n / a + 1) < n + a

Tactic:
refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Nat.add_lt_add_right, lt_of_lt_of_le
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n % a + (a * (n / a) + a * 1) ≤ n + a
inr₁ : n % a + (a * (n / a) + a) ≤ n + a
inr₂ : n % a + a * (n / a) + a ≤ n + a
inr₃ inr₄ : n + a ≤ n + a
⊢ n % a + a * (n / a + 1) ≤ n + a

Tactic:
rw [Nat.mul_add, mul_one, ← add_assoc, hn]

Premises used: add_assoc, mul_one, Nat.mul_add
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : i % a = i
inr₁ inr₂ : i = i
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

Premises used: Nat.mod_eq_of_lt, Nat.add_mul_mod_self_left
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
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:
⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : n ≤ i + a * (n / a)
inr₁ : i + a * (n / a) < n + a
inr₂ : (i + a * (n / a)) % a = i
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : i % a = i
inr₁ inr₂ : i = i
⊢ (i + a * (n / a)) % a = i

Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

Premises used: Nat.mod_eq_of_lt, Nat.add_mul_mod_self_left
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
⊢ val (image (fun (x : ℕ) ↦ x % a) (Finset.Ico n (n + a))) = (Finset.range a).val

Tactic:
congr_arg Finset.val (image_Ico_mod n a)

Premises used: Nat.image_Ico_mod, Finset.val, congr_arg
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
h :
  Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ x % a) (Multiset.Ico n (n + a)))
    (val (image (fun (x : ℕ) ↦ x % a) (Finset.Ico n (n + a))))
⊢ Multiset.map (fun (x : ℕ) ↦ x % a) (Multiset.Ico n (n + a)) = Multiset.range a

Tactic:
convert! congr_arg Finset.val (image_Ico_mod n a)

Premises used: Nat.image_Ico_mod, Finset.val, congr_arg
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ x % a) (Multiset.Ico n (n + a)))
    (val (image (fun (x : ℕ) ↦ x % a) (Finset.Ico n (n + a))))

Tactic:
((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm

Premises used: Iff.mpr, Multiset.dedup, Finset.Ico, Finset.nodup, Multiset.Ico, Multiset.ofList, Multiset.nodup_map_iff_inj_on, Multiset.Nodup.dedup, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
h : ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ x % a) (Multiset.Ico n (n + a)))
    (val (image (fun (x : ℕ) ↦ x % a) (Finset.Ico n (n + a))))

Tactic:
refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm

Premises used: Iff.mpr, Finset.Ico, Finset.nodup, Multiset.nodup_map_iff_inj_on, Multiset.Nodup.dedup, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
⊢ ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y

Tactic:
mod_injOn_Ico _ _

Premises used: Set.Mem, setOf, Multiset.Mem, Set.InjOn, Nat.mod_injOn_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
⊢ ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y

Tactic:
exact mod_injOn_Ico _ _

Premises used: Nat.mod_injOn_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h : ∀ (x : ℕ), x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)
⊢ (range' a b).toFinset = Ico a (a + b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
h : x ∈ range' a b ↔ x ∈ Ico a (a + b)
h₁ : a ≤ x ∧ x < a + b ↔ x ∈ Ico a (a + b)
h₂ h₃ : a ≤ x ∧ x < a + b ↔ a ≤ x ∧ x < a + b
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)

Tactic:
rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]

Premises used: List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
h : ∀ (x : ℕ), x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
⊢ (range' 1 a).toFinset = Icc 1 a

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a x : ℕ
h : x ∈ range' 1 a ↔ x ∈ Icc 1 a
h₁ : 1 ≤ x ∧ x < 1 + a ↔ x ∈ Icc 1 a
h₂ : 1 ≤ x ∧ x < a + 1 ↔ x ∈ Icc 1 a
h₃ : 1 ≤ x ∧ x ≤ a ↔ x ∈ Icc 1 a
h₄ h₅ : 1 ≤ x ∧ x ≤ a ↔ 1 ≤ x ∧ x ≤ a
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a

Tactic:
rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]

Premises used: List.mem_toFinset, Finset.mem_Icc, add_comm, List.mem_range'_1, Nat.lt_succ_iff
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
h : ∀ (x : ℕ), x ∈ (range a).toFinset ↔ x ∈ Finset.range a
⊢ (range a).toFinset = Finset.range a

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a x : ℕ
h : x ∈ range a ↔ x ∈ Finset.range a
h₁ : x < a ↔ x ∈ Finset.range a
h₂ h₃ : x < a ↔ x < a
⊢ x ∈ (range a).toFinset ↔ x ∈ Finset.range a

Tactic:
rw [List.mem_toFinset, List.mem_range, Finset.mem_range]

Premises used: List.mem_toFinset, List.mem_range, Finset.mem_range
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
zero : image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) (range 0) = range 0
succ : ∀ (n : ℕ), image (fun (j : ℕ) ↦ n + 1 - 1 - j) (range (n + 1)) = range (n + 1)
⊢ image (fun (j : ℕ) ↦ n - 1 - j) (range n) = range n

Tactic:
cases n
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
zero : Eq (α := Finset ℕ) (image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) ∅) ∅
zero₁ zero₂ : Eq (α := Finset ℕ) ∅ ∅
⊢ image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) (range 0) = range 0

Tactic:
rw [range_zero, image_empty]

Premises used: Finset.image_empty, Finset.range_zero
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
succ : Ico (n + 1 - 1 + 1 - (n + 1)) (n + 1 - 1 + 1 - 0) = Ico 0 (n + 1)
⊢ image (fun (j : ℕ) ↦ n + 1 - 1 - j) (range (n + 1)) = range (n + 1)

Tactic:
rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]

Premises used: Nat.zero_le, Nat.Ico_image_const_sub_eq_Ico, Finset.range_eq_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
succ : Ico (n - 0 - n) (n - 0 + 1 - 0) = Ico 0 (n + 1)
succ₁ : Ico (n - n) (n + 1) = Ico 0 (n + 1)
⊢ Ico (n + 1 - 1 + 1 - (n + 1)) (n + 1 - 1 + 1 - 0) = Ico 0 (n + 1)

Tactic:
simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]

Premises used: Nat.sub_self, Nat.sub_zero, Nat.succ_sub_succ
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
simp_rw : Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
simp_rw [Finset.range_eq_Ico, map_eq_image]

Premises used: Finset.map_eq_image, Finset.range_eq_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ Ico a (a + b)

Tactic:
(Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm

Premises used: Nat.zero_le, Nat.le_add_right, Finset.Ico_union_Ico_eq_Ico, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h : image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b) = Ico a (a + b)
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)

Tactic:
convert! (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm

Premises used: Nat.zero_le, Nat.le_add_right, Finset.Ico_union_Ico_eq_Ico, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h :
  ∀ (x : ℕ),
    Membership.mem (γ := Finset ℕ) (image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)) x ↔ x ∈ Ico a (a + b)
⊢ image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b) = Ico a (a + b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
h : (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b
⊢ Membership.mem (γ := Finset ℕ) (image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)) x ↔ x ∈ Ico a (a + b)

Tactic:
simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]

Premises used: Finset.mem_image, addLeftEmbedding_apply, Finset.mem_range, Nat.Ico_zero_eq_range, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
h : (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b
h₁ : a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
h : a ≤ x ∧ x < a + b
⊢ x - a < b ∧ a + (x - a) = x

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
h : a ≤ x ∧ x < a + b
⊢ ∃ a_1 < b, a + a_1 = x

Tactic:
exact ⟨x - a, by lia⟩
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
hP : ¬BddAbove (α := ℕ) {x : ℕ | P x}
n : ℕ
⊢ P n

Tactic:
let ⟨_, hm, hl⟩ := not_bddAbove_iff.1 hP n
  decreasingInduction (fun _ _ => h _) hm hl.le

Premises used: LT.lt.le, Nat.decreasingInduction, Iff.mp, not_bddAbove_iff, _private.0.Nat.decreasing_induction_of_not_bddAbove.match_1
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
apply : ∀ (n : ℕ), (fun (n : ℕ) ↦ ∀ m ≥ n, P m) (n + 1) → (fun (n : ℕ) ↦ ∀ m ≥ n, P m) n
apply₁ : ¬BddAbove (α := ℕ) {x : ℕ | (fun (n : ℕ) ↦ ∀ m ≥ n, P m) x}
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl

Premises used: le_rfl, Nat.decreasing_induction_of_not_bddAbove
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm : m ≥ n
inl : ∀ (hm : n ≥ n), P n
inr : ∀ (hm : n < m), P m
⊢ P m

Tactic:
rcases hm.eq_or_lt with rfl | hm

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 n : ℕ
ih : ∀ m ≥ n + 1, P m
hm : n ≥ n
⊢ P n

Tactic:
step n ih
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 n : ℕ
ih : ∀ m ≥ n + 1, P m
hm : n ≥ n
⊢ P n

Tactic:
exact step n ih
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm_1 : m ≥ n
hm : n < m
⊢ P m

Tactic:
ih m hm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm_1 : m ≥ n
hm : n < m
⊢ P m

Tactic:
exact ih m hm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n b : ℕ
hb : Membership.mem (γ := Set ℕ) (upperBounds {x : ℕ | (fun (n : ℕ) ↦ ∀ m ≥ n, P m) x}) b
rcases : ∀ (n : ℕ) (hn : ∀ m > n, P m), False
⊢ False

Tactic:
rcases base with ⟨n, hn⟩
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 b : ℕ
hb : Membership.mem (γ := Set ℕ) (upperBounds {x : ℕ | (fun (n : ℕ) ↦ ∀ m ≥ n, P m) x}) b
n : ℕ
hn : ∀ m > n, P m
specialize : ∀ (m : ℕ) (hm : m ≥ n + b + 1), m > n
specialize₁ : ∀ (hb : n + b + 1 ≤ b), False
⊢ False

Tactic:
specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 b : ℕ
hb : Membership.mem (γ := Set ℕ) (upperBounds {x : ℕ | (fun (n : ℕ) ↦ ∀ m ≥ n, P m) x}) b
n : ℕ
hn : ∀ m > n, P m
m : ℕ
hm : m ≥ n + b + 1
⊢ m > n

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n_1 b n : ℕ
hn : ∀ m > n, P m
hb : n + b + 1 ≤ b
⊢ False

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
hP : Set.Infinite (α := ℕ) {x : ℕ | P x}
n : ℕ
⊢ P n

Tactic:
Nat.decreasing_induction_of_not_bddAbove h (mt BddAbove.finite hP) n

Premises used: mt, BddAbove.finite, Nat.decreasing_induction_of_not_bddAbove
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ (y : ℕ), x < y ∧ P y
n : ℕ
apply : ∀ (hf : Set.Finite (α := ℕ) {x : ℕ | P x}), False
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_infinite h fun hf => _

Premises used: Nat.decreasing_induction_of_infinite
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ (y : ℕ), x < y ∧ P y
n : ℕ
hf : Set.Finite (α := ℕ) {x : ℕ | P x}
obtain :
  ∀ (m : ℕ) (hP : Membership.mem (γ := Set ℕ) {x : ℕ | P x} m)
    (hm : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {x : ℕ | P x} x) y → m ≤ y → y ≤ m), False
⊢ False

Tactic:
obtain ⟨m, hP, hm⟩ := hf.exists_maximal ⟨seed, hs⟩

Premises used: Set.Finite.exists_maximal, Exists.intro
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ (y : ℕ), x < y ∧ P y
n : ℕ
hf : Set.Finite (α := ℕ) {x : ℕ | P x}
m : ℕ
hP : Membership.mem (γ := Set ℕ) {x : ℕ | P x} m
hm : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {x : ℕ | P x} x) y → m ≤ y → y ≤ m
obtain : ∀ (y : ℕ) (hl : m < y) (hy : P y), False
⊢ False

Tactic:
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_gt <| not_lt_iff_le_imp_ge.2 <| hm hs) hP

Premises used: Iff.mpr, le_of_not_gt, not_lt_iff_le_imp_ge
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ (y : ℕ), x < y ∧ P y
n : ℕ
hf : Set.Finite (α := ℕ) {x : ℕ | P x}
m : ℕ
hP : Membership.mem (γ := Set ℕ) {x : ℕ | P x} m
hm : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {x : ℕ | P x} x) y → m ≤ y → y ≤ m
y : ℕ
hl : m < y
hy : P y
⊢ False

Tactic:
hl.not_ge (hm hy hl.le)

Premises used: LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ (y : ℕ), x < y ∧ P y
n : ℕ
hf : Set.Finite (α := ℕ) {x : ℕ | P x}
m : ℕ
hP : Membership.mem (γ := Set ℕ) {x : ℕ | P x} m
hm : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {x : ℕ | P x} x) y → m ≤ y → y ≤ m
y : ℕ
hl : m < y
hy : P y
⊢ False

Tactic:
exact hl.not_ge (hm hy hl.le)

Premises used: LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
f : ℕ → ℕ
hf : ∀ (x : ℕ), seed ≤ x → P x → x < f x ∧ P (f x)
n : ℕ
⊢ P n

Tactic:
seed.cauchy_induction' h hs (fun x hl hx => ⟨f x, hf x hl hx⟩) n

Premises used: Nat.cauchy_induction', Exists.intro
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
apply : ∀ (x : ℕ) (hl : seed.succ ≤ x) (hP : P x), x < (fun (x : ℕ) ↦ k * x) x
⊢ P n

Tactic:
apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩

Premises used: HMul.hMul, Nat.cauchy_induction, And.intro
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x : ℕ
hl : seed.succ ≤ x
_ : P x → x < (fun (x : ℕ) ↦ k * x) x
⊢ ∀ (hP : P x), x < (fun (x : ℕ) ↦ k * x) x

Tactic:
_
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x : ℕ
hl : seed.succ ≤ x
hP : P x
⊢ 1 * x < k * x

Tactic:
(Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk

Premises used: Iff.mpr, LT.lt.trans_le, Nat.succ_pos, Nat.mul_lt_mul_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x : ℕ
hl : seed.succ ≤ x
hP : P x
h₁ : x = 1 * x
⊢ x < (fun (x : ℕ) ↦ k * x) x

Tactic:
convert! (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk

Premises used: Iff.mpr, LT.lt.trans_le, Nat.succ_pos, Nat.mul_lt_mul_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x : ℕ
hl : seed.succ ≤ x
hP : P x
h₁ h₂ : x = x
⊢ x = 1 * x

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (2 * x)
n : ℕ
⊢ P n

Tactic:
Nat.cauchy_induction_mul h 2 seed Nat.one_lt_two hs hm n

Premises used: Nat.one_lt_two, Nat.cauchy_induction_mul, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
M : Type u_1
inst : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h rwa rwa₁ rwa₂ rwa₃ : P (x ^ n * x)
⊢ P (x ^ (n + 1))

Tactic:
rwa [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
M : Type u_1
inst : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h rwa rwa₁ rwa₂ rwa₃ : P (x * x ^ n)
⊢ P (x ^ (n + 1))

Tactic:
rwa [_root_.pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
⊢ (↑(Ico (succ a) b) : Set α) = (↑(Ioo a b) : Set α)

Tactic:
simpa using Set.Ico_succ_left_eq_Ioo _ _

Premises used: Set.Ico_succ_left_eq_Ioo
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ (↑(Icc (succ a) b) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simpa using Set.Icc_succ_left_eq_Ioc_of_not_isMax ha _

Premises used: Set.Icc_succ_left_eq_Ioc_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ (↑(Ico a (succ b)) : Set α) = (↑(Icc a b) : Set α)

Tactic:
simpa using Set.Ico_succ_right_eq_Icc_of_not_isMax hb _

Premises used: Set.Ico_succ_right_eq_Icc_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ (↑(Ioo a (succ b)) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simpa using Set.Ioo_succ_right_eq_Ioc_of_not_isMax hb _

Premises used: Set.Ioo_succ_right_eq_Ioc_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ (↑(Ico (succ a) (succ b)) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simpa using Set.Ico_succ_succ_eq_Ioc_of_not_isMax hb _

Premises used: Set.Ico_succ_succ_eq_Ioc_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
h : a ≤ b
⊢ (↑(insert a (Icc (succ a) b)) : Set α) = (↑(Icc a b) : Set α)

Tactic:
simpa using Set.insert_Icc_succ_left_eq_Icc h

Premises used: Set.insert_Icc_succ_left_eq_Icc
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
h : a ≤ succ b
⊢ (↑(insert (succ b) (Icc a b)) : Set α) = (↑(Icc a (succ b)) : Set α)

Tactic:
simpa using Set.insert_Icc_right_eq_Icc_succ h

Premises used: Set.insert_Icc_right_eq_Icc_succ
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ (↑(insert b (Ico a b)) : Set α) = (↑(Ico a (succ b)) : Set α)

Tactic:
simpa using Set.insert_Ico_right_eq_Ico_succ_of_not_isMax h hb

Premises used: Set.insert_Ico_right_eq_Ico_succ_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
h : a < b
⊢ (↑(insert a (Ico (succ a) b)) : Set α) = (↑(Ico a b) : Set α)

Tactic:
simpa using Set.insert_Ico_succ_left_eq_Ico h

Premises used: Set.insert_Ico_succ_left_eq_Ico
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ (↑(insert (succ b) (Ioc a b)) : Set α) = (↑(Ioc a (succ b)) : Set α)

Tactic:
simpa using Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax h hb

Premises used: Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
-- Module: Mathlib.Order.Interval.Finset.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : SuccOrder α
a b : α
h : a < b
⊢ (↑(insert (succ a) (Ioc (succ a) b)) : Set α) = (↑(Ioc a b) : Set α)

Tactic:
simpa using Set.insert_Ioc_succ_left_eq_Ioc h

Premises used: Set.insert_Ioc_succ_left_eq_Ioc