awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
exact Ioi_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

Premises used: Set.Ioi_subset_Ici_self, HasSubset.Subset.trans
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
rw : Icc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Icc i j = Icc (i.addNat m) (j.addNat m)

Tactic:
rw [← preimage_addNat_Icc_addNat, image_preimage_eq_of_subset]

Premises used: Fin.preimage_addNat_Icc_addNat, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
Icc_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

Premises used: Fin.image_addNat_Ici, Eq.rec, HasSubset.Subset.trans, Set.image_subset_range, Set.Icc_subset_Ici_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
exact Icc_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

Premises used: HasSubset.Subset.trans, Set.Icc_subset_Ici_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
rw : Ico (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ico i j = Ico (i.addNat m) (j.addNat m)

Tactic:
rw [← preimage_addNat_Ico_addNat, image_preimage_eq_of_subset]

Premises used: Set.image_preimage_eq_of_subset, Fin.preimage_addNat_Ico_addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
Ico_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

Premises used: Fin.image_addNat_Ici, Eq.rec, HasSubset.Subset.trans, Set.image_subset_range, Set.Ico_subset_Ici_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ico (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
exact Ico_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

Premises used: HasSubset.Subset.trans, Set.Ico_subset_Ici_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
rw : Ioc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ioc i j = Ioc (i.addNat m) (j.addNat m)

Tactic:
rw [← preimage_addNat_Ioc_addNat, image_preimage_eq_of_subset]

Premises used: Set.image_preimage_eq_of_subset, Fin.preimage_addNat_Ioc_addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
Ioc_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

Premises used: Eq.rec, HasSubset.Subset.trans, Set.image_subset_range, Set.Ioc_subset_Ioi_self, Fin.image_addNat_Ioi
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ioc (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
exact Ioc_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

Premises used: HasSubset.Subset.trans, Set.Ioc_subset_Ioi_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
rw : Ioo (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ioo i j = Ioo (i.addNat m) (j.addNat m)

Tactic:
rw [← preimage_addNat_Ioo_addNat, image_preimage_eq_of_subset]

Premises used: Set.image_preimage_eq_of_subset, Fin.preimage_addNat_Ioo_addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
Ioo_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

Premises used: Eq.rec, HasSubset.Subset.trans, Set.image_subset_range, Fin.image_addNat_Ioi, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m

Tactic:
exact Ioo_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

Premises used: HasSubset.Subset.trans, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' uIcc i j = uIcc (i.addNat m) (j.addNat m)

Tactic:
simp [uIcc, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

Premises used: StrictMono.monotone, Monotone.map_max, Fin.strictMono_addNat, Monotone.map_min, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' uIoc i j = uIoc (i.addNat m) (j.addNat m)

Tactic:
simp [uIoc, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

Premises used: StrictMono.monotone, Set.uIoc, Monotone.map_max, Fin.strictMono_addNat, Monotone.map_min
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) '' uIoo i j = uIoo (i.addNat m) (j.addNat m)

Tactic:
simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

Premises used: StrictMono.monotone, Monotone.map_max, Fin.strictMono_addNat, Set.uIoo, Monotone.map_min
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ ⁻¹' Ici i.succ = Ici i

Tactic:
preimage_addNat_Ici_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Ici_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ ⁻¹' Ioi i.succ = Ioi i

Tactic:
preimage_addNat_Ioi_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Ioi_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ ⁻¹' Iic i.succ = Iic i

Tactic:
preimage_addNat_Iic_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Iic_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ ⁻¹' Iio i.succ = Iio i

Tactic:
preimage_addNat_Iio_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Iio_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' Icc i.succ j.succ = Icc i j

Tactic:
preimage_addNat_Icc_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Icc_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' Ico i.succ j.succ = Ico i j

Tactic:
preimage_addNat_Ico_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Ico_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' Ioc i.succ j.succ = Ioc i j

Tactic:
preimage_addNat_Ioc_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Ioc_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' Ioo i.succ j.succ = Ioo i j

Tactic:
preimage_addNat_Ioo_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_Ioo_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' uIcc i.succ j.succ = uIcc i j

Tactic:
preimage_addNat_uIcc_addNat ..

Premises used: Fin.preimage_addNat_uIcc_addNat, Fin.succ, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' uIoc i.succ j.succ = uIoc i j

Tactic:
preimage_addNat_uIoc_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_uIoc_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ ⁻¹' uIoo i.succ j.succ = uIoo i j

Tactic:
preimage_addNat_uIoo_addNat ..

Premises used: Fin.succ, Fin.preimage_addNat_uIoo_addNat, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ '' Ici i = Ici i.succ

Tactic:
image_addNat_Ici ..

Premises used: Fin.succ, Fin.image_addNat_Ici, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ '' Ioi i = Ioi i.succ

Tactic:
image_addNat_Ioi ..

Premises used: Fin.succ, Fin.image_addNat_Ioi, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ '' Iic i = Ioc 0 i.succ

Tactic:
Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_le_succ_iff.2 hj⟩) ?_

Premises used: Set.Subset.antisymm, Iff.mpr, Fin.succ_le_succ_iff, Fin.succ_pos, And.intro, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
refine : Ioc 0 i.succ ⊆ succ '' Iic i
⊢ succ '' Iic i = Ioc 0 i.succ

Tactic:
refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_le_succ_iff.2 hj⟩) ?_
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
j : Fin (n + 1)
hj₀ : 0 < j
hj : j ≤ i.succ
rcases : ∀ (j : Fin n) (hj₀ : 0 < j.succ) (hj : j.succ ≤ i.succ), j.succ ∈ succ '' Iic i
⊢ j ∈ succ '' Iic i

Tactic:
rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩

Premises used: Fin.exists_succ_eq_of_ne_zero, LT.lt.ne', rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ ≤ i.succ
⊢ j.succ ∈ succ '' Iic i

Tactic:
mem_image_of_mem _ <| succ_le_succ_iff.mp hj

Premises used: Fin.succ_le_succ_iff, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ ≤ i.succ
⊢ j.succ ∈ succ '' Iic i

Tactic:
exact mem_image_of_mem _ <| succ_le_succ_iff.mp hj

Premises used: Fin.succ_le_succ_iff, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ succ '' Iio i = Ioo 0 i.succ

Tactic:
Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_lt_succ_iff.2 hj⟩) ?_

Premises used: Set.Subset.antisymm, Iff.mpr, Fin.succ_lt_succ_iff, Fin.succ_pos, And.intro, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
refine : Ioo 0 i.succ ⊆ succ '' Iio i
⊢ succ '' Iio i = Ioo 0 i.succ

Tactic:
refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_lt_succ_iff.2 hj⟩) ?_
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
j : Fin (n + 1)
hj₀ : 0 < j
hj : j < i.succ
rcases : ∀ (j : Fin n) (hj₀ : 0 < j.succ) (hj : j.succ < i.succ), j.succ ∈ succ '' Iio i
⊢ j ∈ succ '' Iio i

Tactic:
rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩

Premises used: Fin.exists_succ_eq_of_ne_zero, LT.lt.ne', rfl
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ < i.succ
⊢ j.succ ∈ succ '' Iio i

Tactic:
mem_image_of_mem _ <| succ_lt_succ_iff.mp hj

Premises used: Fin.succ_lt_succ_iff, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ < i.succ
⊢ j.succ ∈ succ '' Iio i

Tactic:
exact mem_image_of_mem _ <| succ_lt_succ_iff.mp hj

Premises used: Fin.succ_lt_succ_iff, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' Icc i j = Icc i.succ j.succ

Tactic:
image_addNat_Icc ..

Premises used: Fin.succ, Fin.image_addNat_Icc, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' Ico i j = Ico i.succ j.succ

Tactic:
image_addNat_Ico ..

Premises used: Fin.succ, Fin.image_addNat_Ico, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' Ioc i j = Ioc i.succ j.succ

Tactic:
image_addNat_Ioc ..

Premises used: Fin.succ, Fin.image_addNat_Ioc, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' Ioo i j = Ioo i.succ j.succ

Tactic:
image_addNat_Ioo ..

Premises used: Fin.image_addNat_Ioo, Fin.succ, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' uIcc i j = uIcc i.succ j.succ

Tactic:
image_addNat_uIcc ..

Premises used: Fin.succ, Fin.image_addNat_uIcc, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' uIoc i j = uIoc i.succ j.succ

Tactic:
image_addNat_uIoc ..

Premises used: Fin.image_addNat_uIoc, Fin.succ, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ succ '' uIoo i j = uIoo i.succ j.succ

Tactic:
image_addNat_uIoo ..

Premises used: Fin.succ, Fin.image_addNat_uIoo, Fin.addNat
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
⊢ Eq (α := Set (Fin n)) (range rev) univ

Tactic:
rev_surjective.range_eq

Premises used: Function.Surjective.range_eq, Fin.rev_surjective
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
s : Set (Fin n)
⊢ rev '' s = rev ⁻¹' s

Tactic:
revPerm.image_eq_preimage_symm s

Premises used: Equiv.image_eq_preimage_symm, Fin.revPerm
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
⊢ Eq (α := (s : Set (Fin n)) → Set (Fin n)) (image rev) (preimage rev)

Tactic:
funext image_rev

Premises used: Fin.image_rev, funext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ici i ↔ x ∈ Iic i.rev
⊢ rev ⁻¹' Ici i = Iic i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i x : Fin n
⊢ x ∈ rev ⁻¹' Ici i ↔ x ∈ Iic i.rev

Tactic:
simp [le_rev_iff]

Premises used: Fin.le_rev_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ioi i ↔ x ∈ Iio i.rev
⊢ rev ⁻¹' Ioi i = Iio i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i x : Fin n
⊢ x ∈ rev ⁻¹' Ioi i ↔ x ∈ Iio i.rev

Tactic:
simp [lt_rev_iff]

Premises used: Fin.lt_rev_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Iic i ↔ x ∈ Ici i.rev
⊢ rev ⁻¹' Iic i = Ici i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i x : Fin n
⊢ x ∈ rev ⁻¹' Iic i ↔ x ∈ Ici i.rev

Tactic:
simp [rev_le_iff]

Premises used: Fin.rev_le_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Iio i ↔ x ∈ Ioi i.rev
⊢ rev ⁻¹' Iio i = Ioi i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i x : Fin n
⊢ x ∈ rev ⁻¹' Iio i ↔ x ∈ Ioi i.rev

Tactic:
simp [rev_lt_iff]

Premises used: Fin.rev_lt_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Icc i j ↔ x ∈ Icc j.rev i.rev
⊢ rev ⁻¹' Icc i j = Icc j.rev i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j x : Fin n
⊢ x ∈ rev ⁻¹' Icc i j ↔ x ∈ Icc j.rev i.rev

Tactic:
simp [le_rev_iff, rev_le_iff, and_comm]

Premises used: and_comm, Fin.rev_le_iff, Fin.le_rev_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ico i j ↔ x ∈ Ioc j.rev i.rev
⊢ rev ⁻¹' Ico i j = Ioc j.rev i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j x : Fin n
⊢ x ∈ rev ⁻¹' Ico i j ↔ x ∈ Ioc j.rev i.rev

Tactic:
simp [le_rev_iff, rev_lt_iff, and_comm]

Premises used: and_comm, Fin.rev_lt_iff, Fin.le_rev_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ioc i j ↔ x ∈ Ico j.rev i.rev
⊢ rev ⁻¹' Ioc i j = Ico j.rev i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j x : Fin n
⊢ x ∈ rev ⁻¹' Ioc i j ↔ x ∈ Ico j.rev i.rev

Tactic:
simp [lt_rev_iff, rev_le_iff, and_comm]

Premises used: and_comm, Fin.rev_le_iff, Fin.lt_rev_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ rev ⁻¹' Ioo i j ↔ x ∈ Ioo j.rev i.rev
⊢ rev ⁻¹' Ioo i j = Ioo j.rev i.rev

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j x : Fin n
⊢ x ∈ rev ⁻¹' Ioo i j ↔ x ∈ Ioo j.rev i.rev

Tactic:
simp [lt_rev_iff, rev_lt_iff, and_comm]

Premises used: and_comm, Fin.lt_rev_iff, Fin.rev_lt_iff
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ rev ⁻¹' uIcc i j = uIcc i.rev j.rev

Tactic:
simp [uIcc, ← rev_anti.map_min, ← rev_anti.map_max]

Premises used: Antitone.map_max, Antitone.map_min, Fin.rev_anti, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ rev ⁻¹' uIoo i j = uIoo i.rev j.rev

Tactic:
simp [uIoo, ← rev_anti.map_min, ← rev_anti.map_max]

Premises used: Antitone.map_max, Set.uIoo, Antitone.map_min, Fin.rev_anti
-- Module: Mathlib.Order.Interval.Set.Final
Goal:
J : Type u
inst : LinearOrder J
j : J
rw : ∀ (j₂ : J), ∃ (j₁ : { x : J // x ∈ Ici j }), j₂ ≤ (↑j₁ : J)
⊢ CategoryTheory.Functor.Final.{u, u, u, u} (C := { x : J // x ∈ Ici j }) (Monotone.functor ⋯)

Tactic:
rw [Monotone.final_functor_iff]

Premises used: Monotone.final_functor_iff
-- Module: Mathlib.Order.Interval.Set.Final
Goal:
J : Type u
inst : LinearOrder J
j k : J
⊢ ∃ (j₁ : { x : J // x ∈ Ici j }), k ≤ (↑j₁ : J)

Tactic:
⟨⟨max j k, le_max_left _ _⟩, le_max_right _ _⟩

Premises used: le_max_right, Subtype.mk, Max.max, Exists.intro, le_max_left
-- Module: Mathlib.Order.Interval.Set.Final
Goal:
J : Type u
inst : LinearOrder J
j k : J
⊢ ∃ (j₁ : { x : J // x ∈ Ici j }), k ≤ (↑j₁ : J)

Tactic:
exact ⟨⟨max j k, le_max_left _ _⟩, le_max_right _ _⟩
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : MonotoneOn f (Ici a)
x : α
h_1 : x ∈ Ici a
⊢ f x ∈ Ici (f a)

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : MonotoneOn f (Iic b)
x : α
h_1 : x ∈ Iic b
⊢ f x ∈ Iic (f b)

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : MonotoneOn f (Icc a b)
⊢ MapsTo f (Icc a b) (Icc (f a) (f b))

Tactic:
fun _c hc ↦
    ⟨h (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1, h hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, Set.Icc, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : AntitoneOn f (Ici a)
x : α
h_1 : x ∈ Ici a
⊢ f x ∈ Iic (f a)

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : AntitoneOn f (Iic b)
x : α
h_1 : x ∈ Iic b
⊢ f x ∈ Ici (f b)

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : AntitoneOn f (Icc a b)
⊢ MapsTo f (Icc a b) (Icc (f b) (f a))

Tactic:
fun _c hc ↦
    ⟨h hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2, h (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, Set.Icc, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictMonoOn f (Ici a)
⊢ MapsTo f (Ioi a) (Ioi (f a))

Tactic:
fun _c hc ↦ h le_rfl hc.le hc

Premises used: Set.Ioi, le_rfl, Set.Mem, setOf, LT.lt.le, Set.MapsTo
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictMonoOn f (Iic b)
⊢ MapsTo f (Iio b) (Iio (f b))

Tactic:
fun _c hc ↦ h hc.le le_rfl hc

Premises used: le_rfl, Set.Mem, setOf, LT.lt.le, Set.MapsTo, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictMonoOn f (Icc a b)
⊢ MapsTo f (Ioo a b) (Ioo (f a) (f b))

Tactic:
fun _c hc ↦
    ⟨h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1,
     h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Ioo_subset_Icc_self, Set.Mem, setOf, LT.lt.le, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, LT.lt.trans, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictAntiOn f (Ici a)
⊢ MapsTo f (Ioi a) (Iio (f a))

Tactic:
fun _c hc ↦ h le_rfl hc.le hc

Premises used: le_rfl, Set.Mem, setOf, LT.lt.le, Set.MapsTo, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictAntiOn f (Iic b)
⊢ MapsTo f (Iio b) (Ioi (f b))

Tactic:
fun _c hc ↦ h hc.le le_rfl hc

Premises used: Set.Ioi, le_rfl, Set.Mem, setOf, LT.lt.le, Set.MapsTo
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictAntiOn f (Icc a b)
⊢ MapsTo f (Ioo a b) (Ioo (f b) (f a))

Tactic:
fun _c hc ↦
    ⟨h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2,
     h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Ioo_subset_Icc_self, Set.Mem, setOf, LT.lt.le, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, LT.lt.trans, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : Monotone f
⊢ MapsTo f (Ici a) (Ici (f a))

Tactic:
(h.monotoneOn _).mapsTo_Ici

Premises used: MonotoneOn.mapsTo_Ici, Monotone.monotoneOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : Monotone f
⊢ MapsTo f (Iic b) (Iic (f b))

Tactic:
(h.monotoneOn _).mapsTo_Iic

Premises used: Monotone.monotoneOn, MonotoneOn.mapsTo_Iic
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : Monotone f
⊢ MapsTo f (Icc a b) (Icc (f a) (f b))

Tactic:
(h.monotoneOn _).mapsTo_Icc

Premises used: Monotone.monotoneOn, MonotoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : Antitone f
⊢ MapsTo f (Ici a) (Iic (f a))

Tactic:
(h.antitoneOn _).mapsTo_Ici

Premises used: Antitone.antitoneOn, AntitoneOn.mapsTo_Ici
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : Antitone f
⊢ MapsTo f (Iic b) (Ici (f b))

Tactic:
(h.antitoneOn _).mapsTo_Iic

Premises used: Antitone.antitoneOn, AntitoneOn.mapsTo_Iic
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : Antitone f
⊢ MapsTo f (Icc a b) (Icc (f b) (f a))

Tactic:
(h.antitoneOn _).mapsTo_Icc

Premises used: Antitone.antitoneOn, AntitoneOn.mapsTo_Icc
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictMono f
⊢ MapsTo f (Ioi a) (Ioi (f a))

Tactic:
(h.strictMonoOn _).mapsTo_Ioi

Premises used: StrictMonoOn.mapsTo_Ioi, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictMono f
⊢ MapsTo f (Iio b) (Iio (f b))

Tactic:
(h.strictMonoOn _).mapsTo_Iio

Premises used: StrictMono.strictMonoOn, StrictMonoOn.mapsTo_Iio
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictMono f
⊢ MapsTo f (Ioo a b) (Ioo (f a) (f b))

Tactic:
(h.strictMonoOn _).mapsTo_Ioo

Premises used: StrictMonoOn.mapsTo_Ioo, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictAnti f
⊢ MapsTo f (Ioi a) (Iio (f a))

Tactic:
(h.strictAntiOn _).mapsTo_Ioi

Premises used: StrictAnti.strictAntiOn, StrictAntiOn.mapsTo_Ioi
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictAnti f
⊢ MapsTo f (Iio b) (Ioi (f b))

Tactic:
(h.strictAntiOn _).mapsTo_Iio

Premises used: StrictAnti.strictAntiOn, StrictAntiOn.mapsTo_Iio
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictAnti f
⊢ MapsTo f (Ioo a b) (Ioo (f b) (f a))

Tactic:
(h.strictAntiOn _).mapsTo_Ioo

Premises used: StrictAnti.strictAntiOn, StrictAntiOn.mapsTo_Ioo