awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
h : m = n
i j : Fin n
⊢ Fin.cast h ⁻¹' uIoo i j = uIoo (Fin.cast ⋯ i) (Fin.cast ⋯ 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
⊢ castSucc ⁻¹' Ici i.castSucc = 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
⊢ castSucc ⁻¹' Ioi i.castSucc = 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
⊢ castSucc ⁻¹' Iic i.castSucc = 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
⊢ castSucc ⁻¹' Iio i.castSucc = 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
⊢ castSucc ⁻¹' Icc i.castSucc j.castSucc = 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
⊢ castSucc ⁻¹' Ico i.castSucc j.castSucc = 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
⊢ castSucc ⁻¹' Ioc i.castSucc j.castSucc = 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
⊢ castSucc ⁻¹' Ioo i.castSucc j.castSucc = 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
⊢ castSucc ⁻¹' uIcc i.castSucc j.castSucc = 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
⊢ castSucc ⁻¹' uIoc i.castSucc j.castSucc = 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
⊢ castSucc ⁻¹' uIoo i.castSucc j.castSucc = 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
⊢ castSucc '' Ici i = Ico i.castSucc (last n)

Tactic:
image_castAdd_Ici ..

Premises used: Fin.image_castAdd_Ici
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ castSucc '' Ioi i = Ioo i.castSucc (last n)

Tactic:
image_castAdd_Ioi ..

Premises used: Fin.image_castAdd_Ioi
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ castSucc '' Iic i = Iic i.castSucc

Tactic:
image_castAdd_Iic ..

Premises used: Fin.image_castAdd_Iic
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i : Fin n
⊢ castSucc '' Iio i = Iio i.castSucc

Tactic:
image_castAdd_Iio ..

Premises used: Fin.image_castAdd_Iio
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' Icc i j = Icc i.castSucc j.castSucc

Tactic:
image_castAdd_Icc ..

Premises used: Fin.image_castAdd_Icc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' Ico i j = Ico i.castSucc j.castSucc

Tactic:
image_castAdd_Ico ..

Premises used: Fin.image_castAdd_Ico
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' Ioc i j = Ioc i.castSucc j.castSucc

Tactic:
image_castAdd_Ioc ..

Premises used: Fin.image_castAdd_Ioc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' Ioo i j = Ioo i.castSucc j.castSucc

Tactic:
image_castAdd_Ioo ..

Premises used: Fin.image_castAdd_Ioo
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' uIcc i j = uIcc i.castSucc j.castSucc

Tactic:
image_castAdd_uIcc ..

Premises used: Fin.image_castAdd_uIcc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' uIoc i j = uIoc i.castSucc j.castSucc

Tactic:
image_castAdd_uIoc ..

Premises used: Fin.image_castAdd_uIoc
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n : ℕ
i j : Fin n
⊢ castSucc '' uIoo i j = uIoo i.castSucc j.castSucc

Tactic:
image_castAdd_uIoo ..

Premises used: Fin.image_castAdd_uIoo
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
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
⊢ Eq (α := Set (Fin (m + n))) (range (natAdd m)) {i : Fin (m + n) | m ≤ (↑i : ℕ)}

Tactic:
ext i
-- Module: Mathlib.Order.Interval.Set.Fin
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
h₁ :
  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))) (range (natAdd m)) i ↔
    Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin n
⊢ Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} (natAdd m i)

Tactic:
apply le_coe_natAdd

Premises used: Fin.le_coe_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin (m + n)
hi : m ≤ (↑i : ℕ)
⊢ (↑i : ℕ) - m < n

Tactic:
lia
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin (m + n)
h : ∀ (hi : m ≤ (↑i : ℕ)), natAdd m (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n) = i
⊢ Membership.mem (γ := Set (Fin (m + n))) {i : Fin (m + n) | m ≤ (↑i : ℕ)} i →
    Membership.mem (γ := Set (Fin (m + n))) (range (natAdd m)) i

Tactic:
refine fun (hi : m ≤ i) ↦ ⟨⟨i - m, by lia⟩, ?_⟩
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin (m + n)
hi : m ≤ (↑i : ℕ)
h : (↑(natAdd m (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n)) : ℕ) = (↑i : ℕ)
⊢ natAdd m (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n) = i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
i : Fin (m + n)
hi : m ≤ (↑i : ℕ)
⊢ (↑(natAdd m (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n)) : ℕ) = (↑i : ℕ)

Tactic:
simp [hi]
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
inst : NeZero n
⊢ Eq (α := Set (Fin (m + n))) (range (natAdd m)) (Ici (natAdd m 0))

Tactic:
range_natAdd m n

Premises used: Set.Ici, setOf, Fin.range_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
inst : NeZero m
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))
⊢ range (natAdd m) = Ioi (castAdd n ⊤)

Tactic:
ext ⟨_, _⟩
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
m n : ℕ
inst : NeZero m
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:
simp [range_natAdd, lt_def, ← Nat.succ_le_iff, Nat.one_le_iff_ne_zero.mpr (NeZero.ne m)]

Premises used: Iff.mpr, Fin.range_natAdd, Fin.lt_def, Nat.one_le_iff_ne_zero, Nat.succ_le_iff, NeZero.ne
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ici (natAdd m i) ↔ x ∈ Ici i
⊢ natAdd m ⁻¹' Ici (natAdd m i) = Ici i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ x ∈ natAdd m ⁻¹' Ici (natAdd m i) ↔ x ∈ Ici i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ioi (natAdd m i) ↔ x ∈ Ioi i
⊢ natAdd m ⁻¹' Ioi (natAdd m i) = Ioi i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ x ∈ natAdd m ⁻¹' Ioi (natAdd m i) ↔ x ∈ Ioi i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Iic (natAdd m i) ↔ x ∈ Iic i
⊢ natAdd m ⁻¹' Iic (natAdd m i) = Iic i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ x ∈ natAdd m ⁻¹' Iic (natAdd m i) ↔ x ∈ Iic i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Iio (natAdd m i) ↔ x ∈ Iio i
⊢ natAdd m ⁻¹' Iio (natAdd m i) = Iio i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ x ∈ natAdd m ⁻¹' Iio (natAdd m i) ↔ x ∈ Iio i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) ↔ x ∈ Icc i j
⊢ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) = Icc i j

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

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) ↔ x ∈ Ico i j
⊢ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) = Ico i j

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

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) ↔ x ∈ Ioc i j
⊢ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) = Ioc i j

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

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
h : ∀ (x : Fin n), x ∈ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) ↔ x ∈ Ioo i j
⊢ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) = Ioo i j

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

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' uIcc (natAdd m i) (natAdd m j) = uIcc i j

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

Premises used: StrictMono.monotone, Monotone.map_max, Monotone.map_min, Set.uIcc, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' uIoc (natAdd m i) (natAdd m j) = uIoc i j

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

Premises used: StrictMono.monotone, Set.uIoc, Monotone.map_max, Monotone.map_min, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' uIoo (natAdd m i) (natAdd m j) = uIoo i j

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

Premises used: StrictMono.monotone, Monotone.map_max, Set.uIoo, Monotone.map_min, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
rw : Ici (natAdd m i) ⊆ range (natAdd m)
⊢ natAdd m '' Ici i = Ici (natAdd m i)

Tactic:
rw [← preimage_natAdd_Ici_natAdd, image_preimage_eq_of_subset]

Premises used: Set.image_preimage_eq_of_subset, Fin.preimage_natAdd_Ici_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
rw : Ici (natAdd m i) ⊆ {i : Fin (m + n) | m ≤ (↑i : ℕ)}
⊢ Ici (natAdd m i) ⊆ range (natAdd m)

Tactic:
rw [range_natAdd]

Premises used: Fin.range_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ {i : Fin (m + n) | m ≤ (↑i : ℕ)}

Tactic:
fun j hj ↦ Nat.le_trans (le_coe_natAdd ..) hj

Premises used: Set.Mem, setOf, Fin.le_coe_natAdd, Set.Subset, Nat.le_trans
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ {i : Fin (m + n) | m ≤ (↑i : ℕ)}

Tactic:
exact fun j hj ↦ Nat.le_trans (le_coe_natAdd ..) hj

Premises used: Fin.le_coe_natAdd, Nat.le_trans
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
rw : Ioi (natAdd m i) ⊆ range (natAdd m)
⊢ natAdd m '' Ioi i = Ioi (natAdd m i)

Tactic:
rw [← preimage_natAdd_Ioi_natAdd, image_preimage_eq_of_subset]

Premises used: Fin.preimage_natAdd_Ioi_natAdd, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) ⊆ range (natAdd m)

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

Premises used: Fin.image_natAdd_Ici, Set.Ioi_subset_Ici_self, Eq.rec, HasSubset.Subset.trans, Set.image_subset_range
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) ⊆ range (natAdd m)

Tactic:
exact Ioi_subset_Ici_self.trans <| image_natAdd_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 (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
⊢ natAdd m '' Icc i j = Icc (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Icc_natAdd, image_preimage_eq_of_subset]

Premises used: Fin.preimage_natAdd_Icc_natAdd, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Icc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

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

Premises used: Fin.image_natAdd_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 (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
exact Icc_subset_Ici_self.trans <| image_natAdd_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 (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
⊢ natAdd m '' Ico i j = Ico (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Ico_natAdd, image_preimage_eq_of_subset]

Premises used: Fin.preimage_natAdd_Ico_natAdd, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ico (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

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

Premises used: Fin.image_natAdd_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 (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

Tactic:
exact Ico_subset_Ici_self.trans <| image_natAdd_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 (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
⊢ natAdd m '' Ioc i j = Ioc (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Ioc_natAdd, image_preimage_eq_of_subset]

Premises used: Fin.preimage_natAdd_Ioc_natAdd, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ioc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

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

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

Tactic:
exact Ioc_subset_Ioi_self.trans <| image_natAdd_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 (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
⊢ natAdd m '' Ioo i j = Ioo (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Ioo_natAdd, image_preimage_eq_of_subset]

Premises used: Fin.preimage_natAdd_Ioo_natAdd, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)

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

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

Tactic:
exact Ioo_subset_Ioi_self.trans <| image_natAdd_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
⊢ natAdd m '' uIcc i j = uIcc (natAdd m i) (natAdd m j)

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

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

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

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

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

Premises used: StrictMono.monotone, Monotone.map_max, Set.uIoo, Monotone.map_min, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ici (i.addNat m)) x ↔ x ∈ Ici i
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ici (i.addNat m) = Ici i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ici (i.addNat m)) x ↔ x ∈ Ici i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioi (i.addNat m)) x ↔ x ∈ Ioi i
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) = Ioi i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioi (i.addNat m)) x ↔ x ∈ Ioi i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iic (i.addNat m)) x ↔ x ∈ Iic i
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iic (i.addNat m) = Iic i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iic (i.addNat m)) x ↔ x ∈ Iic i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
h : ∀ (x : Fin n), Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iio (i.addNat m)) x ↔ x ∈ Iio i
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iio (i.addNat m) = Iio i

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i x : Fin n
⊢ Membership.mem (γ := Set (Fin n)) ((fun (x : Fin n) ↦ x.addNat m) ⁻¹' Iio (i.addNat m)) x ↔ x ∈ Iio i

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
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
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m) = Icc i j

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j 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:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
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
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ico (i.addNat m) (j.addNat m) = Ico i j

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j 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:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
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
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioc (i.addNat m) (j.addNat m) = Ioc i j

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j 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:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
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
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' Ioo (i.addNat m) (j.addNat m) = Ioo i j

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j 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:
simp
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ (fun (x : Fin n) ↦ x.addNat m) ⁻¹' uIcc (i.addNat m) (j.addNat m) = uIcc i j

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.addNat m) (j.addNat m) = uIoc i j

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.addNat m) (j.addNat m) = uIoo i j

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 m : ℕ
i : Fin n
rw : Ici (i.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ici i = Ici (i.addNat m)

Tactic:
rw [← preimage_addNat_Ici_addNat, image_preimage_eq_of_subset]

Premises used: Fin.preimage_addNat_Ici_addNat, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
⊢ (↑i : ℕ) + m ≤ (↑j : ℕ)

Tactic:
have : (i : ℕ) + m ≤ j := hj
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : (↑i : ℕ) + m ≤ (↑j : ℕ)
⊢ (↑j : ℕ) - m < n

Tactic:
lia
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : (↑i : ℕ) + m ≤ (↑j : ℕ)
refine : (fun (x : Fin n) ↦ x.addNat m) ⟨(↑j : ℕ) - m, ⋯⟩ = j
⊢ Membership.mem (γ := Set (Fin (n + m))) (range fun (x : Fin n) ↦ x.addNat m) j

Tactic:
refine ⟨⟨j - m, by lia⟩, ?_⟩
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : (↑i : ℕ) + m ≤ (↑j : ℕ)
⊢ (fun (x : Fin n) ↦ x.addNat m) ⟨(↑j : ℕ) - m, ⋯⟩ = j

Tactic:
simp (disch := lia)
-- Module: Mathlib.Order.Interval.Set.Fin
Goal:
n m : ℕ
i : Fin n
rw : Ioi (i.addNat m) ⊆ range fun (x : Fin n) ↦ x.addNat m
⊢ (fun (x : Fin n) ↦ x.addNat m) '' Ioi i = Ioi (i.addNat m)

Tactic:
rw [← preimage_addNat_Ioi_addNat, image_preimage_eq_of_subset]

Premises used: Fin.preimage_addNat_Ioi_addNat, Set.image_preimage_eq_of_subset
-- 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:
Ioi_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

Premises used: Fin.image_addNat_Ici, Set.Ioi_subset_Ici_self, Eq.rec, HasSubset.Subset.trans, Set.image_subset_range