awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
R : Type u_1
inst : CompleteLinearOrder R
f : ι → R
no_least_elem : ⨅ (i : ι), f i ∉ range f
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (i : ι), Ici (f i)) (Ioi (⨅ (i : ι), f i))

Tactic:
simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

Premises used: Set.mem_range, Set.iUnion_exists, isGLB_iInf, IsGLB.biUnion_Ici_eq_Ioi, Set.iUnion_iUnion_eq'
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
R : Type u_1
inst : CompleteLinearOrder R
f : ι → R
no_greatest_elem : ⨆ (i : ι), f i ∉ range f
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (i : ι), Iic (f i)) (Iio (⨆ (i : ι), f i))

Tactic:
@iUnion_Ici_eq_Ioi_iInf ι (OrderDual R) _ f no_greatest_elem

Premises used: iSup, setOf, iUnion_Ici_eq_Ioi_iInf, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
R : Type u_1
inst : CompleteLinearOrder R
f : ι → R
has_least_elem : ⨅ (i : ι), f i ∈ range f
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (i : ι), Ici (f i)) (Ici (⨅ (i : ι), f i))

Tactic:
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

Premises used: Set.mem_range, IsGLB.biUnion_Ici_eq_Ici, Set.iUnion_exists, isGLB_iInf, Set.iUnion_iUnion_eq'
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
R : Type u_1
inst : CompleteLinearOrder R
f : ι → R
has_greatest_elem : ⨆ (i : ι), f i ∈ range f
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ (i : ι), Iic (f i)) (Iic (⨆ (i : ι), f i))

Tactic:
@iUnion_Ici_eq_Ici_iInf ι (OrderDual R) _ f has_greatest_elem

Premises used: iSup, setOf, Set.Iic, OrderDual, iUnion_Ici_eq_Ici_iInf
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
⊢ Eq.{v + 1} (α := Set α) (⋃ (i : ι), Iio (f i)) univ ↔ ¬BddAbove (range f)

Tactic:
simp [not_bddAbove_iff, Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, not_bddAbove_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ Eq.{v + 1} (α := Set α) (⋃ (i : ι), Iic (f i)) univ

Tactic:
Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)

Premises used: Iff.mpr, Set.eq_univ_of_subset, iUnion_Iio_eq_univ_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
refine : Subset.{v} (α := Set α) (⋃ (i : ι), Iio (f i)) (⋃ (i : ι), Iic (f i))
⊢ Eq.{v + 1} (α := Set α) (⋃ (i : ι), Iic (f i)) univ

Tactic:
refine Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)

Premises used: Iff.mpr, Set.eq_univ_of_subset, iUnion_Iio_eq_univ_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
h : ∀ (i : ι), Iio (f i) ⊆ Iic (f i)
⊢ Subset.{v} (α := Set α) (⋃ (i : ι), Iio (f i)) (⋃ (i : ι), Iic (f i))

Tactic:
gcongr
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
i : ι
⊢ Iio (f i) ⊆ Iic (f i)

Tactic:
Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
i : ι
⊢ Iio (f i) ⊆ Iic (f i)

Tactic:
exact Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
⊢ Eq.{v + 1} (α := Set α) (⋂ (i : ι), Iic (f i)) ∅ ↔ ¬BddBelow (range f)

Tactic:
simp [not_bddBelow_iff, Set.eq_empty_iff_forall_notMem]

Premises used: not_bddBelow_iff, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ Eq.{v + 1} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅

Tactic:
eq_empty_of_subset_empty ?_

Premises used: Set.eq_empty_of_subset_empty
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
refine : Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅
⊢ Eq.{v + 1} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅

Tactic:
refine eq_empty_of_subset_empty ?_

Premises used: Set.eq_empty_of_subset_empty
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
rw : Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) (⋂ (i : ι), Iic (f i))
⊢ Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) ∅

Tactic:
rw [← iInter_Iic_eq_empty_iff.mpr hf]

Premises used: Iff.mpr, iInter_Iic_eq_empty_iff
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
h : ∀ (i : ι), Iio (f i) ⊆ Iic (f i)
⊢ Subset.{v} (α := Set α) (⋂ (i : ι), Iio (f i)) (⋂ (i : ι), Iic (f i))

Tactic:
gcongr
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
i : ι
⊢ Iio (f i) ⊆ Iic (f i)

Tactic:
Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Interval.Set.Disjoint
Goal:
ι : Sort u
α : Type v
inst : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
i : ι
⊢ Iio (f i) ⊆ Iic (f i)

Tactic:
exact Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
h : ∀ (x : ℕ), x ∈ range (ι := Fin n) val ↔ x ∈ Iio n
⊢ range (ι := Fin n) val = Iio n

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n x : ℕ
⊢ x ∈ range (ι := Fin n) val ↔ x ∈ Iio n

Tactic:
simp [Fin.exists_iff]

Premises used: Fin.exists_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ val ⁻¹' Ici (↑i : ℕ) = Ici i

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ val ⁻¹' Ioi (↑i : ℕ) = Ioi i

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ val ⁻¹' Iic (↑i : ℕ) = Iic i

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ val ⁻¹' Iio (↑i : ℕ) = Iio i

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' Icc (↑i : ℕ) (↑j : ℕ) = Icc i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' Ico (↑i : ℕ) (↑j : ℕ) = Ico i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Ico, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' Ioc (↑i : ℕ) (↑j : ℕ) = Ioc i j

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' Ioo (↑i : ℕ) (↑j : ℕ) = Ioo i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' uIcc (↑i : ℕ) (↑j : ℕ) = uIcc i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, Set.uIcc, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' uIoc (↑i : ℕ) (↑j : ℕ) = uIoc i j

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, Set.uIoc, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val ⁻¹' uIoo (↑i : ℕ) (↑j : ℕ) = uIoo i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.uIoo, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
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
rw₃ rw₄ : Ico (↑i : ℕ) n = Ico (↑i : ℕ) n
⊢ val '' Ici i = Ico (↑i : ℕ) n

Tactic:
rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]

Premises used: Fin.preimage_val_Ici_val, Set.Ici_inter_Iio, Set.image_preimage_eq_inter_range, Fin.range_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
rw : Iic (↑i : ℕ) ⊆ range (ι := Fin n) val
⊢ val '' Iic i = Iic (↑i : ℕ)

Tactic:
rw [← preimage_val_Iic_val, image_preimage_eq_of_subset]

Premises used: Fin.preimage_val_Iic_val, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ Iic (↑i : ℕ) ⊆ range (ι := Fin n) val

Tactic:
simp [range_val]

Premises used: Fin.range_val
-- Module: Mathlib.Order.Interval.Set.Fin
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
rw₃ rw₄ : Ioo (↑i : ℕ) n = Ioo (↑i : ℕ) n
⊢ val '' Ioi i = Ioo (↑i : ℕ) n

Tactic:
rw [← preimage_val_Ioi_val, image_preimage_eq_inter_range, range_val, Ioi_inter_Iio]

Premises used: Fin.preimage_val_Ioi_val, Set.image_preimage_eq_inter_range, Set.Ioi_inter_Iio, Fin.range_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
rw : Iio (↑i : ℕ) ⊆ Iio n
⊢ val '' Iio i = Iio (↑i : ℕ)

Tactic:
rw [← preimage_val_Iio_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_eq_inter_range, Fin.range_val, Fin.preimage_val_Iio_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ Iio (↑i : ℕ) ⊆ Iio n

Tactic:
Iio_subset_Iio i.is_lt.le

Premises used: Fin.is_lt, LT.lt.le, Set.Iio_subset_Iio
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ Iio (↑i : ℕ) ⊆ Iio n

Tactic:
exact Iio_subset_Iio i.is_lt.le

Premises used: Fin.is_lt, LT.lt.le, Set.Iio_subset_Iio
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
rw : Icc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
⊢ val '' Icc i j = Icc (↑i : ℕ) (↑j : ℕ)

Tactic:
rw [← preimage_val_Icc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_eq_inter_range, Fin.preimage_val_Icc_val, Fin.range_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Icc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
fun k hk ↦ hk.2.trans_lt j.is_lt

Premises used: Set.Mem, setOf, Fin.is_lt, Set.Subset, And.right, Set.Iio, LE.le.trans_lt, Nat.lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Icc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans_lt j.is_lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
rw : Ico (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
⊢ val '' Ico i j = Ico (↑i : ℕ) (↑j : ℕ)

Tactic:
rw [← preimage_val_Ico_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Premises used: Set.inter_eq_left, Fin.preimage_val_Ico_val, Set.image_preimage_eq_inter_range, Fin.range_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Ico (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
fun k hk ↦ hk.2.trans j.is_lt

Premises used: Set.Mem, setOf, Fin.is_lt, Set.Subset, And.right, LT.lt.trans, Set.Iio, Nat.lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Ico (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans j.is_lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
rw : Ioc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
⊢ val '' Ioc i j = Ioc (↑i : ℕ) (↑j : ℕ)

Tactic:
rw [← preimage_val_Ioc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Premises used: Set.inter_eq_left, Fin.preimage_val_Ioc_val, Set.image_preimage_eq_inter_range, Fin.range_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Ioc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
fun k hk ↦ hk.2.trans_lt j.is_lt

Premises used: Set.Mem, setOf, Fin.is_lt, Set.Subset, And.right, Set.Iio, LE.le.trans_lt, Nat.lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Ioc (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans_lt j.is_lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
rw : Ioo (↑i : ℕ) (↑j : ℕ) ⊆ Iio n
⊢ val '' Ioo i j = Ioo (↑i : ℕ) (↑j : ℕ)

Tactic:
rw [← preimage_val_Ioo_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_eq_inter_range, Fin.range_val, Fin.preimage_val_Ioo_val
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Ioo (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
fun k hk ↦ hk.2.trans j.is_lt

Premises used: Set.Mem, setOf, Fin.is_lt, Set.Subset, And.right, LT.lt.trans, Set.Iio, Nat.lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ Ioo (↑i : ℕ) (↑j : ℕ) ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans j.is_lt
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val '' uIcc i j = uIcc (↑i : ℕ) (↑j : ℕ)

Tactic:
simp [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val '' uIoc i j = uIoc (↑i : ℕ) (↑j : ℕ)

Tactic:
simp [uIoc]

Premises used: Set.uIoc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ val '' uIoo i j = uIoo (↑i : ℕ) (↑j : ℕ)

Tactic:
simp [uIoo]

Premises used: Set.uIoo
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Ici (castLE h i) = Ici i

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Ioi (castLE h i) = Ioi i

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Iic (castLE h i) = Iic i

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Iio (castLE h i) = Iio i

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Icc (castLE h i) (castLE h j) = Icc i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Ico (castLE h i) (castLE h j) = Ico i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Ico, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Ioc (castLE h i) (castLE h j) = Ioc i j

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' Ioo (castLE h i) (castLE h j) = Ioo i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' uIcc (castLE h i) (castLE h j) = uIcc i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, Set.uIcc, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' uIoc (castLE h i) (castLE h j) = uIoc i j

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, Set.uIoc, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ castLE h ⁻¹' uIoo (castLE h i) (castLE h j) = uIoo i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.uIoo, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin m
h : m ≤ n
⊢ val '' castLE h '' Iic i = val '' Iic (castLE h i)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin m
h : m ≤ n
⊢ val '' castLE h '' Iio i = val '' Iio (castLE h i)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Icc i j = val '' Icc (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ico i j = val '' Ico (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ioc i j = val '' Ioc (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' Ioo i j = val '' Ioo (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIcc i j = val '' uIcc (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIoc i j = val '' uIoc (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i j : Fin m
h : m ≤ n
⊢ val '' castLE h '' uIoo i j = val '' uIoo (castLE h i) (castLE h j)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
inst : NeZero m
⊢ image (α := Fin (n + m)) val (range (castAdd m)) = image (α := Fin (n + m)) val (Iio (natAdd n 0))

Tactic:
simp [← range_comp, comp_def]

Premises used: Set.range_comp, Function.comp_def
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ castAdd m ⁻¹' Ici (castAdd m i) = Ici i

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ castAdd m ⁻¹' Ioi (castAdd m i) = Ioi i

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ castAdd m ⁻¹' Iic (castAdd m i) = Iic i

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ castAdd m ⁻¹' Iio (castAdd m i) = Iio i

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' Icc (castAdd m i) (castAdd m j) = Icc i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' Ico (castAdd m i) (castAdd m j) = Ico i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Ico, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' Ioc (castAdd m i) (castAdd m j) = Ioc i j

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' Ioo (castAdd m i) (castAdd m j) = Ioo i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' uIcc (castAdd m i) (castAdd m j) = uIcc i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, Set.uIcc, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' uIoc (castAdd m i) (castAdd m j) = uIoc i j

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, Set.uIoc, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m ⁻¹' uIoo (castAdd m i) (castAdd m j) = uIoo i j

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.uIoo, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
inst : NeZero m
i : Fin n
⊢ val '' castAdd m '' Ici i = val '' Ico (castAdd m i) (natAdd n 0)

Tactic:
simp [← image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
inst : NeZero m
i : Fin n
⊢ val '' castAdd m '' Ioi i = val '' Ioo (castAdd m i) (natAdd n 0)

Tactic:
simp [← image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ castAdd m '' Iic i = Iic (castAdd m i)

Tactic:
image_castLE_Iic i _

Premises used: Fin.image_castLE_Iic
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ castAdd m '' Iio i = Iio (castAdd m i)

Tactic:
image_castLE_Iio ..

Premises used: Fin.image_castLE_Iio
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' Icc i j = Icc (castAdd m i) (castAdd m j)

Tactic:
image_castLE_Icc ..

Premises used: Fin.image_castLE_Icc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' Ico i j = Ico (castAdd m i) (castAdd m j)

Tactic:
image_castLE_Ico ..

Premises used: Fin.image_castLE_Ico
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' Ioc i j = Ioc (castAdd m i) (castAdd m j)

Tactic:
image_castLE_Ioc ..

Premises used: Fin.image_castLE_Ioc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' Ioo i j = Ioo (castAdd m i) (castAdd m j)

Tactic:
image_castLE_Ioo ..

Premises used: Fin.image_castLE_Ioo
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' uIcc i j = uIcc (castAdd m i) (castAdd m j)

Tactic:
image_castLE_uIcc ..

Premises used: Fin.image_castLE_uIcc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' uIoc i j = uIoc (castAdd m i) (castAdd m j)

Tactic:
image_castLE_uIoc ..

Premises used: Fin.image_castLE_uIoc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ castAdd m '' uIoo i j = uIoo (castAdd m i) (castAdd m j)

Tactic:
image_castLE_uIoo ..

Premises used: Fin.image_castLE_uIoo
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
s : Set (Fin m)
⊢ Fin.cast h '' s = Fin.cast ⋯ ⁻¹' s

Tactic:
(finCongr h).image_eq_preimage_symm _

Premises used: finCongr, Equiv.image_eq_preimage_symm
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
⊢ image (Fin.cast h) = preimage (Fin.cast ⋯)

Tactic:
funext <| image_cast h

Premises used: funext, Fin.image_cast
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i : Fin n
⊢ Fin.cast h ⁻¹' Ici i = Ici (Fin.cast ⋯ i)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i : Fin n
⊢ Fin.cast h ⁻¹' Ioi i = Ioi (Fin.cast ⋯ i)

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i : Fin n
⊢ Fin.cast h ⁻¹' Iic i = Iic (Fin.cast ⋯ i)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i : Fin n
⊢ Fin.cast h ⁻¹' Iio i = Iio (Fin.cast ⋯ i)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' Icc i j = Icc (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' Ico i j = Ico (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Ico, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' Ioc i j = Ioc (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' Ioo i j = Ioo (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' uIcc i j = uIcc (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, Set.uIcc, rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' uIoc i j = uIoc (Fin.cast ⋯ i) (Fin.cast ⋯ j)

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, Set.uIoc, setOf, Set.preimage, rfl