awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
⊢ ⋃ x ∈ s, Ioi x = Ioi a
have refine_1 : ∀ (x : α) (hx : x ∈ s), Ioi x ⊆ Ioi a
Tactic: refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
refine_1 : ∀ (x : α) (hx : x ∈ s), Ioi x ⊆ Ioi a
⊢ ⋃ x ∈ s, Ioi x = Ioi a
have refine_2 : ∀ (x : α) (hx : x ∈ Ioi a), Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x
Tactic: refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x
have refine_2 : ∀ (y : α) (hys : y ∈ s), a ≤ y → ∀ (hyx : y < x), Membership.mem (γ := Set α) (⋃ i ∈ s, Ioi i) x
Tactic: rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
⊢ ⋃ x ∈ s, Ici x = Ioi a
have refine_1 : ∀ (x : α) (hx : x ∈ s), Ici x ⊆ Ioi a
Tactic: refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
refine_1 : ∀ (x : α) (hx : x ∈ s), Ici x ⊆ Ioi a
⊢ ⋃ x ∈ s, Ici x = Ioi a
have refine_2 : ∀ (x : α) (hx : x ∈ Ioi a), Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
Tactic: refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
have refine_2 : ∀ (y : α) (hys : y ∈ s), a ≤ y → ∀ (hyx : y < x), Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
Tactic: rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left : a ≤ y
hyx : y < x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
have refine_2 : ∃ (i : α) (_ : i ∈ s), x ∈ Ici i
Tactic: rw [mem_iUnion₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
⊢ ⋃ x ∈ s, Ici x = Ici a
have refine_1 : ∀ (x : α) (hx : x ∈ s), Ici x ⊆ Ici a
Tactic: refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
refine_1 : ∀ (x : α) (hx : x ∈ s), Ici x ⊆ Ici a
⊢ ⋃ x ∈ s, Ici x = Ici a
have refine_2 : ∀ (x : α) (hx : x ∈ Ici a), Membership.mem (γ := Set α) (⋃ i ∈ s, Ici i) x
Tactic: refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ Eq.{v + 1} (α := Set α) (⋃ (i : ι), Iic (f i)) univ
have refine : Subset.{v} (α := Set α) (⋃ (i : ι), Iio (f i)) (⋃ (i : ι), Iic (f i))
Tactic: refine Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ Subset.{v} (α := Set α) (⋃ (i : ι), Iio (f i)) (⋃ (i : ι), Iic (f i))
have h : ∀ (i : ι), Iio (f i) ⊆ Iic (f i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ Eq.{v + 1} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅
have refine : Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅
Tactic: refine eq_empty_of_subset_empty ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅
have rw : Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) (⋂ (i : ι), Iic (f i))
Tactic: rw [← iInter_Iic_eq_empty_iff.mpr hf]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) (⋂ (i : ι), Iic (f i))
have h : ∀ (i : ι), Iio (f i) ⊆ Iic (f i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
⊢ range (ι := Fin n) val = Iio n
have h : ∀ (x : ℕ), x ∈ range (ι := Fin n) val ↔ x ∈ Iio n
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ val '' Ici i = Ico (↑i : ℕ) n
have rw : image (α := Fin n) val (val ⁻¹' Ici (↑i : ℕ)) = Ico (↑i : ℕ) n
Tactic: rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : image (α := Fin n) val (val ⁻¹' Ici (↑i : ℕ)) = Ico (↑i : ℕ) n
⊢ val '' Ici i = Ico (↑i : ℕ) n
have rw₁ : Ici (↑i : ℕ) ∩ range (ι := Fin n) val = Ico (↑i : ℕ) n
Tactic: rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : image (α := Fin n) val (val ⁻¹' Ici (↑i : ℕ)) = Ico (↑i : ℕ) n
rw₁ : Ici (↑i : ℕ) ∩ range (ι := Fin n) val = Ico (↑i : ℕ) n
⊢ val '' Ici i = Ico (↑i : ℕ) n
have rw₂ : Ici (↑i : ℕ) ∩ Iio n = Ico (↑i : ℕ) n
Tactic: rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : image (α := Fin n) val (val ⁻¹' Ici (↑i : ℕ)) = Ico (↑i : ℕ) n
rw₁ : Ici (↑i : ℕ) ∩ range (ι := Fin n) val = Ico (↑i : ℕ) n
rw₂ : Ici (↑i : ℕ) ∩ Iio n = Ico (↑i : ℕ) n
⊢ val '' Ici i = Ico (↑i : ℕ) n
have rw₃ : Ico (↑i : ℕ) n = Ico (↑i : ℕ) n
Tactic: rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ val '' Iic i = Iic (↑i : ℕ)
have rw : Iic (↑i : ℕ) ⊆ range (ι := Fin n) val
Tactic: rw [← preimage_val_Iic_val, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ val '' Ioi i = Ioo (↑i : ℕ) n
have rw : image (α := Fin n) val (val ⁻¹' Ioi (↑i : ℕ)) = Ioo (↑i : ℕ) n
Tactic: rw [← preimage_val_Ioi_val, image_preimage_eq_inter_range, range_val, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : image (α := Fin n) val (val ⁻¹' Ioi (↑i : ℕ)) = Ioo (↑i : ℕ) n
⊢ val '' Ioi i = Ioo (↑i : ℕ) n
have rw₁ : Ioi (↑i : ℕ) ∩ range (ι := Fin n) val = Ioo (↑i : ℕ) n
Tactic: rw [← preimage_val_Ioi_val, image_preimage_eq_inter_range, range_val, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : image (α := Fin n) val (val ⁻¹' Ioi (↑i : ℕ)) = Ioo (↑i : ℕ) n
rw₁ : Ioi (↑i : ℕ) ∩ range (ι := Fin n) val = Ioo (↑i : ℕ) n
⊢ val '' Ioi i = Ioo (↑i : ℕ) n
have rw₂ : Ioi (↑i : ℕ) ∩ Iio n = Ioo (↑i : ℕ) n
Tactic: rw [← preimage_val_Ioi_val, image_preimage_eq_inter_range, range_val, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : image (α := Fin n) val (val ⁻¹' Ioi (↑i : ℕ)) = Ioo (↑i : ℕ) n
rw₁ : Ioi (↑i : ℕ) ∩ range (ι := Fin n) val = Ioo (↑i : ℕ) n
rw₂ : Ioi (↑i : ℕ) ∩ Iio n = Ioo (↑i : ℕ) n
⊢ val '' Ioi i = Ioo (↑i : ℕ) n
have rw₃ : Ioo (↑i : ℕ) n = Ioo (↑i : ℕ) n
Tactic: rw [← preimage_val_Ioi_val, image_preimage_eq_inter_range, range_val, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ val '' Iio i = Iio (↑i : ℕ)
have rw : Iio (↑i : ℕ) ⊆ Iio n
Tactic: rw [← preimage_val_Iio_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ val '' Icc i j = Icc (↑i : ℕ) (↑j : ℕ)
have rw : Icc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
Tactic: rw [← preimage_val_Icc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ val '' Ico i j = Ico (↑i : ℕ) (↑j : ℕ)
have rw : Ico (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
Tactic: rw [← preimage_val_Ico_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ val '' Ioc i j = Ioc (↑i : ℕ) (↑j : ℕ)
have rw : Ioc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
Tactic: rw [← preimage_val_Ioc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ val '' Ioo i j = Ioo (↑i : ℕ) (↑j : ℕ)
have rw : Ioo (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
Tactic: rw [← preimage_val_Ioo_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
m n : ℕ
⊢ Eq (α := Set (Fin (m + n))) (range (natAdd m)) {i : Fin (m + n) | m ≤ (↑i : ℕ)}
have h : ∀ (i : Fin (m + n)),
  Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i ↔
    Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
m n : ℕ
i : Fin (m + n)
⊢ Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i ↔
    Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i
have h : Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i →
  Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
m n : ℕ
i : Fin (m + n)
h :
  Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i →
    Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i
⊢ Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i ↔
    Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i
have h₁ : Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i →
  Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
m n : ℕ
i : Fin (m + n)
⊢ Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i →
    Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i
have h : ∀ (hi : m ≤ (↑i : ℕ)), natAdd m (⟨(↑i : ℕ) - m, sorry⟩ : Fin n) = i
Tactic: refine fun (hi : m ≤ i) ↦ ⟨⟨i - m, by lia⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
m n : ℕ
i : Fin (m + n)
hi : m ≤ (↑i : ℕ)
⊢ natAdd m (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n) = i
have h : (↑(natAdd m (⟨(↑i : ℕ) - m, sorry⟩ : Fin n)) : ℕ) = (↑i : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
m n : ℕ
inst : NeZero m
⊢ range (natAdd m) = Ioi (castAdd n ⊤)
have h : ∀ (val : ℕ) (isLt : val < m + n),
  Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) (⟨val, isLt⟩ : Fin (m + n)) ↔
    Membership.mem (γ := Set (Fin (m + n))) (Ioi (castAdd n ⊤)) (⟨val, isLt⟩ : Fin (m + n))
Tactic: ext ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ici (natAdd m i) = Ici i
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ici (natAdd m i) ↔ x ∈ Ici i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ioi (natAdd m i) = Ioi i
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ioi (natAdd m i) ↔ x ∈ Ioi i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Iic (natAdd m i) = Iic i
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Iic (natAdd m i) ↔ x ∈ Iic i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Iio (natAdd m i) = Iio i
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Iio (natAdd m i) ↔ x ∈ Iio i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) = Icc i j
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) ↔ x ∈ Icc i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) = Ico i j
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) ↔ x ∈ Ico i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) = Ioc i j
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) ↔ x ∈ Ioc i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) = Ioo i j
have h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) ↔ x ∈ Ioo i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ natAdd m '' Ici i = Ici (natAdd m i)
have rw : Ici (natAdd m i) ⊆ range (natAdd m)
Tactic: rw [← preimage_natAdd_Ici_natAdd, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ range (natAdd m)
have rw : Ici (natAdd m i) ⊆ {i : Fin (m + n) | m ≤ (↑i : ℕ)}
Tactic: rw [range_natAdd]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ natAdd m '' Ioi i = Ioi (natAdd m i)
have rw : Ioi (natAdd m i) ⊆ range (natAdd m)
Tactic: rw [← preimage_natAdd_Ioi_natAdd, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m '' Icc i j = Icc (natAdd m i) (natAdd m j)
have rw : Icc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Tactic: rw [← preimage_natAdd_Icc_natAdd, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m '' Ico i j = Ico (natAdd m i) (natAdd m j)
have rw : Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Tactic: rw [← preimage_natAdd_Ico_natAdd, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioc i j = Ioc (natAdd m i) (natAdd m j)
have rw : Ioc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Tactic: rw [← preimage_natAdd_Ioc_natAdd, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioo i j = Ioo (natAdd m i) (natAdd m j)
have rw : Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Tactic: rw [← preimage_natAdd_Ioo_natAdd, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ici (i.addNat m) = Ici i
have h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ici (i.addNat m)) x ↔ x ∈ Ici i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) = Ioi i
have h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioi (i.addNat m)) x ↔ x ∈ Ioi i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iic (i.addNat m) = Iic i
have h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iic (i.addNat m)) x ↔ x ∈ Iic i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iio (i.addNat m) = Iio i
have h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iio (i.addNat m)) x ↔ x ∈ Iio i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m) = Icc i j
have h : ∀ (x : Fin n),
  Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m)) x ↔ x ∈ Icc i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ico (i.addNat m) (j.addNat m) = Ico i j
have h : ∀ (x : Fin n),
  Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ico (i.addNat m) (j.addNat m)) x ↔ x ∈ Ico i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioc (i.addNat m) (j.addNat m) = Ioc i j
have h : ∀ (x : Fin n),
  Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioc (i.addNat m) (j.addNat m)) x ↔ x ∈ Ioc i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioo (i.addNat m) (j.addNat m) = Ioo i j
have h : ∀ (x : Fin n),
  Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioo (i.addNat m) (j.addNat m)) x ↔ x ∈ Ioo i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ici i = Ici (i.addNat m)
have rw : Ici (i.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
Tactic: rw [← preimage_addNat_Ici_addNat, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (hypothesis)
Goal:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
⊢ Membership.mem (γ := Set (Fin (n + m))) (range fun (x : Fin n) ↦ x.addNat m) j
have this : (↑i : ℕ) + m ≤ (↑j : ℕ)
Tactic: have : (i : ℕ) + m ≤ j := hj
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : (↑i : ℕ) + m ≤ (↑j : ℕ)
⊢ Membership.mem (γ := Set (Fin (n + m))) (range fun (x : Fin n) ↦ x.addNat m) j
have refine : (fun (x : Fin n) ↦ x.addNat m) ⟨(↑j : ℕ) - m, sorry⟩ = j
Tactic: refine ⟨⟨j - m, by lia⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ioi i = Ioi (i.addNat m)
have rw : Ioi (i.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
Tactic: rw [← preimage_addNat_Ioi_addNat, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Icc i j = Icc (i.addNat m) (j.addNat m)
have rw : Icc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
Tactic: rw [← preimage_addNat_Icc_addNat, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ico i j = Ico (i.addNat m) (j.addNat m)
have rw : Ico (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
Tactic: rw [← preimage_addNat_Ico_addNat, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ioc i j = Ioc (i.addNat m) (j.addNat m)
have rw : Ioc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
Tactic: rw [← preimage_addNat_Ioc_addNat, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ioo i j = Ioo (i.addNat m) (j.addNat m)
have rw : Ioo (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
Tactic: rw [← preimage_addNat_Ioo_addNat, image_preimage_eq_of_subset]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ succ '' Iic i = Ioc 0 i.succ
have refine : Ioc 0 i.succ ⊆ succ '' Iic i
Tactic: refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_le_succ_iff.2 hj⟩) ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 1)
hj₀ : 0 < j
hj : j ≤ i.succ
⊢ j ∈ succ '' Iic i
have rcases : ∀ (j : Fin n) (hj₀ : 0 < j.succ) (hj : j.succ ≤ i.succ), j.succ ∈ succ '' Iic i
Tactic: rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩
Cleared hypotheses: j, hj₀, hj
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ succ '' Iio i = Ioo 0 i.succ
have refine : Ioo 0 i.succ ⊆ succ '' Iio i
Tactic: refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_lt_succ_iff.2 hj⟩) ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 1)
hj₀ : 0 < j
hj : j < i.succ
⊢ j ∈ succ '' Iio i
have rcases : ∀ (j : Fin n) (hj₀ : 0 < j.succ) (hj : j.succ < i.succ), j.succ ∈ succ '' Iio i
Tactic: rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩
Cleared hypotheses: j, hj₀, hj
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ rev ⁻¹' Ici i = Iic i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ici i ↔ x ∈ Iic i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ rev ⁻¹' Ioi i = Iio i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ioi i ↔ x ∈ Iio i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ rev ⁻¹' Iic i = Ici i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Iic i ↔ x ∈ Ici i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ rev ⁻¹' Iio i = Ioi i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Iio i ↔ x ∈ Ioi i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ rev ⁻¹' Icc i j = Icc j.rev i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Icc i j ↔ x ∈ Icc j.rev i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ico i j = Ioc j.rev i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ico i j ↔ x ∈ Ioc j.rev i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ioc i j = Ico j.rev i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ioc i j ↔ x ∈ Ico j.rev i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Fin (goal)
Goal:
n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ioo i j = Ioo j.rev i.rev
have h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ioo i j ↔ x ∈ Ioo j.rev i.rev
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Final (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
⊢ CategoryTheory.Functor.Final.{u, u, u, u} (C := { x : J // x ∈ Ici j }) (Monotone.functor ⋯)
have rw : ∀ (j₂ : J), ∃ (j₁ : { x : J // x ∈ Ici j }), j₂ ≤ (↑j₁ : J)
Tactic: rw [Monotone.final_functor_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Image (goal)
Goal:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x : α // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c : α) x → p a x
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r (↑c : α) y}) {y : α | r (↑c : α) y ∧ q y b}
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r (↑c : α) y}) x ↔
    Membership.mem (γ := Set α) {y : α | r (↑c : α) y ∧ q y b} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Image (goal)
Goal:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x : α // p a x ∧ q x b }
h : ∀ {x : α}, r x (↑c : α) → q x b
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r y (↑c : α)}) {y : α | p a y ∧ r y (↑c : α)}
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r y (↑c : α)}) x ↔
    Membership.mem (γ := Set α) {y : α | p a y ∧ r y (↑c : α)} x
Tactic: ext