awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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))))
have h : ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y
Tactic: refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
⊢ (range' a b).toFinset = Ico a (a + b)
have h : ∀ (x : ℕ), x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b x : ℕ
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)
have h : x ∈ range' a b ↔ x ∈ Ico a (a + b)
Tactic: rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b x : ℕ
h : x ∈ range' a b ↔ x ∈ Ico a (a + b)
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)
have h₁ : a ≤ x ∧ x < a + b ↔ x ∈ Ico a (a + b)
Tactic: rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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)
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)
have h₂ : a ≤ x ∧ x < a + b ↔ a ≤ x ∧ x < a + b
Tactic: rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
⊢ (range' 1 a).toFinset = Icc 1 a
have h : ∀ (x : ℕ), x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a x : ℕ
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
have h : x ∈ range' 1 a ↔ x ∈ Icc 1 a
Tactic: rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a x : ℕ
h : x ∈ range' 1 a ↔ x ∈ Icc 1 a
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
have h₁ : 1 ≤ x ∧ x < 1 + a ↔ x ∈ Icc 1 a
Tactic: rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a x : ℕ
h : x ∈ range' 1 a ↔ x ∈ Icc 1 a
h₁ : 1 ≤ x ∧ x < 1 + a ↔ x ∈ Icc 1 a
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
have h₂ : 1 ≤ x ∧ x < a + 1 ↔ x ∈ Icc 1 a
Tactic: rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
have h₃ : 1 ≤ x ∧ x ≤ a ↔ x ∈ Icc 1 a
Tactic: rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
have h₄ : 1 ≤ x ∧ x ≤ a ↔ 1 ≤ x ∧ x ≤ a
Tactic: rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
⊢ (range a).toFinset = Finset.range a
have h : ∀ (x : ℕ), x ∈ (range a).toFinset ↔ x ∈ Finset.range a
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a x : ℕ
⊢ x ∈ (range a).toFinset ↔ x ∈ Finset.range a
have h : x ∈ range a ↔ x ∈ Finset.range a
Tactic: rw [List.mem_toFinset, List.mem_range, Finset.mem_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a x : ℕ
h : x ∈ range a ↔ x ∈ Finset.range a
⊢ x ∈ (range a).toFinset ↔ x ∈ Finset.range a
have h₁ : x < a ↔ x ∈ Finset.range a
Tactic: rw [List.mem_toFinset, List.mem_range, Finset.mem_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a x : ℕ
h : x ∈ range a ↔ x ∈ Finset.range a
h₁ : x < a ↔ x ∈ Finset.range a
⊢ x ∈ (range a).toFinset ↔ x ∈ Finset.range a
have h₂ : x < a ↔ x < a
Tactic: rw [List.mem_toFinset, List.mem_range, Finset.mem_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
⊢ image (fun (j : ℕ) ↦ n - 1 - j) (range n) = range n
have zero : image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) (range 0) = range 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
zero : image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) (range 0) = range 0
⊢ image (fun (j : ℕ) ↦ n - 1 - j) (range n) = range n
have succ : ∀ (n : ℕ), image (fun (j : ℕ) ↦ n + 1 - 1 - j) (range (n + 1)) = range (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
⊢ image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) (range 0) = range 0
have zero : Eq (α := Finset ℕ) (image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) ∅) ∅
Tactic: rw [range_zero, image_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
zero : Eq (α := Finset ℕ) (image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) ∅) ∅
⊢ image (fun (j : ℕ) ↦ HSub.hSub (α := ℕ) 0 1 - j) (range 0) = range 0
have zero₁ : Eq (α := Finset ℕ) ∅ ∅
Tactic: rw [range_zero, image_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
⊢ image (fun (j : ℕ) ↦ n + 1 - 1 - j) (range (n + 1)) = range (n + 1)
have succ : Ico (n + 1 - 1 + 1 - (n + 1)) (n + 1 - 1 + 1 - 0) = Ico 0 (n + 1)
Tactic: rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
⊢ Ico (n + 1 - 1 + 1 - (n + 1)) (n + 1 - 1 + 1 - 0) = Ico 0 (n + 1)
have succ : Ico (n - 0 - n) (n - 0 + 1 - 0) = Ico 0 (n + 1)
Tactic: simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
succ : Ico (n - 0 - n) (n - 0 + 1 - 0) = Ico 0 (n + 1)
⊢ Ico (n + 1 - 1 + 1 - (n + 1)) (n + 1 - 1 + 1 - 0) = Ico 0 (n + 1)
have succ₁ : Ico (n - n) (n + 1) = Ico 0 (n + 1)
Tactic: simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
have simp_rw : Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)
Tactic: simp_rw [Finset.range_eq_Ico, map_eq_image]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)
have h : image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b) = Ico a (a + b)
Tactic: convert! (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
⊢ image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b) = Ico a (a + b)
have h : ∀ (x : ℕ), Membership.mem (γ := Finset ℕ) (image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)) x ↔ x ∈ Ico a (a + b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b x : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 b)) x ↔ x ∈ Ico a (a + b)
have h : (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b
Tactic: simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b
have h : (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b x : ℕ
h : (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b
have h₁ : a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
P : ℕ → Prop
base : ∃ (n : ℕ), ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ P n
have apply : ∀ (n : ℕ), (fun (n : ℕ) ↦ ∀ m ≥ n, P m) (n + 1) → (fun (n : ℕ) ↦ ∀ m ≥ n, P m) n
Tactic: apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ P n
have apply₁ : ¬BddAbove (α := ℕ) {x : ℕ | (fun (n : ℕ) ↦ ∀ m ≥ n, P m) x}
Tactic: apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ P m
have inl : ∀ (hm : n ≥ n), P n
Tactic: rcases hm.eq_or_lt with rfl | hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ P m
have inr : ∀ (hm : n < m), P m
Tactic: rcases hm.eq_or_lt with rfl | hm
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ False
have rcases : ∀ (n : ℕ) (hn : ∀ m > n, P m), False
Tactic: rcases base with ⟨n, hn⟩
Cleared hypotheses: base
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ False
have specialize : ∀ (m : ℕ) (hm : m ≥ n + b + 1), m > n
Tactic: specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ False
have specialize₁ : ∀ (hb : n + b + 1 ≤ b), False
Tactic: specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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 : ℕ
⊢ P n
have apply : ∀ (hf : Set.Finite (α := ℕ) {x : ℕ | P x}), False
Tactic: apply Nat.decreasing_induction_of_infinite h fun hf => _
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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}
⊢ False
have 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
Tactic: obtain ⟨m, hP, hm⟩ := hf.exists_maximal ⟨seed, hs⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ False
have obtain : ∀ (y : ℕ) (hl : m < y) (hy : P y), False
Tactic: obtain ⟨y, hl, hy⟩ := hi m (le_of_not_gt <| not_lt_iff_le_imp_ge.2 <| hm hs) hP
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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 : ℕ
⊢ P n
have apply : ∀ (x : ℕ) (hl : seed.succ ≤ x) (hP : P x), x < (fun (x : ℕ) ↦ k * x) x
Tactic: apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ x < (fun (x : ℕ) ↦ k * x) x
have h₁ : x = 1 * x
Tactic: convert! (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ x = 1 * x
have h₁ : x = x
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
have rw : x ∈ (Finset.Icc a b).val ↔ a ≤ x ∧ x ≤ b
Tactic: rw [Icc, ← Finset.mem_def, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Icc a b).val ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
have rw₁ : x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [Icc, ← Finset.mem_def, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Icc a b).val ↔ a ≤ x ∧ x ≤ b
rw₁ : x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
have rw₂ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [Icc, ← Finset.mem_def, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b
have rw : x ∈ (Finset.Ico a b).val ↔ a ≤ x ∧ x < b
Tactic: rw [Ico, ← Finset.mem_def, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ico a b).val ↔ a ≤ x ∧ x < b
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b
have rw₁ : x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b
Tactic: rw [Ico, ← Finset.mem_def, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ico a b).val ↔ a ≤ x ∧ x < b
rw₁ : x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b
have rw₂ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
Tactic: rw [Ico, ← Finset.mem_def, Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b
have rw : x ∈ (Finset.Ioc a b).val ↔ a < x ∧ x ≤ b
Tactic: rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ioc a b).val ↔ a < x ∧ x ≤ b
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b
have rw₁ : x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b
Tactic: rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ioc a b).val ↔ a < x ∧ x ≤ b
rw₁ : x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b
have rw₂ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b
have rw : x ∈ (Finset.Ioo a b).val ↔ a < x ∧ x < b
Tactic: rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ioo a b).val ↔ a < x ∧ x < b
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b
have rw₁ : x ∈ Finset.Ioo a b ↔ a < x ∧ x < b
Tactic: rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b x : α
rw : x ∈ (Finset.Ioo a b).val ↔ a < x ∧ x < b
rw₁ : x ∈ Finset.Ioo a b ↔ a < x ∧ x < b
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b
have rw₂ : a < x ∧ x < b ↔ a < x ∧ x < b
Tactic: rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x
have rw : x ∈ (Finset.Ici a).val ↔ a ≤ x
Tactic: rw [Ici, ← Finset.mem_def, Finset.mem_Ici]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
rw : x ∈ (Finset.Ici a).val ↔ a ≤ x
⊢ x ∈ Ici a ↔ a ≤ x
have rw₁ : x ∈ Finset.Ici a ↔ a ≤ x
Tactic: rw [Ici, ← Finset.mem_def, Finset.mem_Ici]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
rw : x ∈ (Finset.Ici a).val ↔ a ≤ x
rw₁ : x ∈ Finset.Ici a ↔ a ≤ x
⊢ x ∈ Ici a ↔ a ≤ x
have rw₂ : a ≤ x ↔ a ≤ x
Tactic: rw [Ici, ← Finset.mem_def, Finset.mem_Ici]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x
have rw : x ∈ (Finset.Ioi a).val ↔ a < x
Tactic: rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
rw : x ∈ (Finset.Ioi a).val ↔ a < x
⊢ x ∈ Ioi a ↔ a < x
have rw₁ : x ∈ Finset.Ioi a ↔ a < x
Tactic: rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a x : α
rw : x ∈ (Finset.Ioi a).val ↔ a < x
rw₁ : x ∈ Finset.Ioi a ↔ a < x
⊢ x ∈ Ioi a ↔ a < x
have rw₂ : a < x ↔ a < x
Tactic: rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b
have rw : x ∈ (Finset.Iic b).val ↔ x ≤ b
Tactic: rw [Iic, ← Finset.mem_def, Finset.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
rw : x ∈ (Finset.Iic b).val ↔ x ≤ b
⊢ x ∈ Iic b ↔ x ≤ b
have rw₁ : x ∈ Finset.Iic b ↔ x ≤ b
Tactic: rw [Iic, ← Finset.mem_def, Finset.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
rw : x ∈ (Finset.Iic b).val ↔ x ≤ b
rw₁ : x ∈ Finset.Iic b ↔ x ≤ b
⊢ x ∈ Iic b ↔ x ≤ b
have rw₂ : x ≤ b ↔ x ≤ b
Tactic: rw [Iic, ← Finset.mem_def, Finset.mem_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iio b ↔ x < b
have rw : x ∈ (Finset.Iio b).val ↔ x < b
Tactic: rw [Iio, ← Finset.mem_def, Finset.mem_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
rw : x ∈ (Finset.Iio b).val ↔ x < b
⊢ x ∈ Iio b ↔ x < b
have rw₁ : x ∈ Finset.Iio b ↔ x < b
Tactic: rw [Iio, ← Finset.mem_def, Finset.mem_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
b x : α
rw : x ∈ (Finset.Iio b).val ↔ x < b
rw₁ : x ∈ Finset.Iio b ↔ x < b
⊢ x ∈ Iio b ↔ x < b
have rw₂ : x < b ↔ x < b
Tactic: rw [Iio, ← Finset.mem_def, Finset.mem_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Icc a b = 0 ↔ ¬a ≤ b
have rw : (Finset.Icc a b).val = 0 ↔ ¬a ≤ b
Tactic: rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Icc a b).val = 0 ↔ ¬a ≤ b
⊢ Icc a b = 0 ↔ ¬a ≤ b
have rw₁ : Finset.Icc a b = ∅ ↔ ¬a ≤ b
Tactic: rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Icc a b).val = 0 ↔ ¬a ≤ b
rw₁ : Finset.Icc a b = ∅ ↔ ¬a ≤ b
⊢ Icc a b = 0 ↔ ¬a ≤ b
have rw₂ : ¬a ≤ b ↔ ¬a ≤ b
Tactic: rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Ico a b = 0 ↔ ¬a < b
have rw : (Finset.Ico a b).val = 0 ↔ ¬a < b
Tactic: rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Ico a b).val = 0 ↔ ¬a < b
⊢ Ico a b = 0 ↔ ¬a < b
have rw₁ : Finset.Ico a b = ∅ ↔ ¬a < b
Tactic: rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Ico a b).val = 0 ↔ ¬a < b
rw₁ : Finset.Ico a b = ∅ ↔ ¬a < b
⊢ Ico a b = 0 ↔ ¬a < b
have rw₂ : ¬a < b ↔ ¬a < b
Tactic: rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Ioc a b = 0 ↔ ¬a < b
have rw : (Finset.Ioc a b).val = 0 ↔ ¬a < b
Tactic: rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Ioc a b).val = 0 ↔ ¬a < b
⊢ Ioc a b = 0 ↔ ¬a < b
have rw₁ : Finset.Ioc a b = ∅ ↔ ¬a < b
Tactic: rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
rw : (Finset.Ioc a b).val = 0 ↔ ¬a < b
rw₁ : Finset.Ioc a b = ∅ ↔ ¬a < b
⊢ Ioc a b = 0 ↔ ¬a < b
have rw₂ : ¬a < b ↔ ¬a < b
Tactic: rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DenselyOrdered α
⊢ Ioo a b = 0 ↔ ¬a < b
have rw : (Finset.Ioo a b).val = 0 ↔ ¬a < b
Tactic: rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DenselyOrdered α
rw : (Finset.Ioo a b).val = 0 ↔ ¬a < b
⊢ Ioo a b = 0 ↔ ¬a < b
have rw₁ : Finset.Ioo a b = ∅ ↔ ¬a < b
Tactic: rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DenselyOrdered α
rw : (Finset.Ioo a b).val = 0 ↔ ¬a < b
rw₁ : Finset.Ioo a b = ∅ ↔ ¬a < b
⊢ Ioo a b = 0 ↔ ¬a < b
have rw₂ : ¬a < b ↔ ¬a < b
Tactic: rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
⊢ Ico a a = 0
have rw : (Finset.Ico a a).val = 0
Tactic: rw [Ico, Finset.Ico_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ico a a).val = 0
⊢ Ico a a = 0
have rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
Tactic: rw [Ico, Finset.Ico_self, Finset.empty_val]