awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iio a) = Iio (castLE h a)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iic a) = Iic (castLE h a)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iio a) = Iio (castLE h a)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (castAdd m) (Icc i j) = Icc (castAdd m i) (castAdd m j)

Tactic:
finsetImage_castLE_Icc ..

Premises used: Fin.finsetImage_castLE_Icc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (castAdd m) (Ico i j) = Ico (castAdd m i) (castAdd m j)

Tactic:
finsetImage_castLE_Ico ..

Premises used: Fin.finsetImage_castLE_Ico
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (castAdd m) (Ioc i j) = Ioc (castAdd m i) (castAdd m j)

Tactic:
finsetImage_castLE_Ioc ..

Premises used: Fin.finsetImage_castLE_Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (castAdd m) (Ioo i j) = Ioo (castAdd m i) (castAdd m j)

Tactic:
finsetImage_castLE_Ioo ..

Premises used: Fin.finsetImage_castLE_Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (castAdd m) (uIcc i j) = uIcc (castAdd m i) (castAdd m j)

Tactic:
finsetImage_castLE_uIcc ..

Premises used: Fin.finsetImage_castLE_uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
inst : NeZero m
i : Fin n
⊢ image (castAdd m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
inst : NeZero m
i : Fin n
⊢ image (castAdd m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ image (castAdd m) (Iic i) = Iic (castAdd m i)

Tactic:
finsetImage_castLE_Iic i _

Premises used: Fin.finsetImage_castLE_Iic
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ image (castAdd m) (Iio i) = Iio (castAdd m i)

Tactic:
finsetImage_castLE_Iio ..

Premises used: Fin.finsetImage_castLE_Iio
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (castAddEmb m) (Icc i j) = Icc (castAdd m i) (castAdd m j)

Tactic:
map_castLEEmb_Icc ..

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_Icc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (castAddEmb m) (Ico i j) = Ico (castAdd m i) (castAdd m j)

Tactic:
map_castLEEmb_Ico ..

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_Ico
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (castAddEmb m) (Ioc i j) = Ioc (castAdd m i) (castAdd m j)

Tactic:
map_castLEEmb_Ioc ..

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (castAddEmb m) (Ioo i j) = Ioo (castAdd m i) (castAdd m j)

Tactic:
map_castLEEmb_Ioo ..

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (castAddEmb m) (uIcc i j) = uIcc (castAdd m i) (castAdd m j)

Tactic:
map_castLEEmb_uIcc ..

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
inst : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
simp [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
inst : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ map (castAddEmb m) (Iic i) = Iic (castAdd m i)

Tactic:
map_castLEEmb_Iic i _

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_Iic
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ map (castAddEmb m) (Iio i) = Iio (castAdd m i)

Tactic:
map_castLEEmb_Iio ..

Premises used: Fin.castAddEmb, Fin.map_castLEEmb_Iio
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Icc i j) = Icc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ico i j) = Ico (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ioc i j) = Ioc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ioo i j) = Ioo (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (uIcc i j) = uIcc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Ici i) = Ici (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Ioi i) = Ioi (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Iic i) = Iic (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Iio i) = Iio (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Icc i j) = Icc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ico i j) = Ico (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ioc i j) = Ioc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ioo i j) = Ioo (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (uIcc i j) = uIcc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Ici i) = Ici (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Ioi i) = Ioi (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iic i) = Iic (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iio i) = Iio (Fin.cast h i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image castSucc (Icc i j) = Icc i.castSucc j.castSucc

Tactic:
finsetImage_castAdd_Icc ..

Premises used: Fin.finsetImage_castAdd_Icc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image castSucc (Ico i j) = Ico i.castSucc j.castSucc

Tactic:
finsetImage_castAdd_Ico ..

Premises used: Fin.finsetImage_castAdd_Ico
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image castSucc (Ioc i j) = Ioc i.castSucc j.castSucc

Tactic:
finsetImage_castAdd_Ioc ..

Premises used: Fin.finsetImage_castAdd_Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image castSucc (Ioo i j) = Ioo i.castSucc j.castSucc

Tactic:
finsetImage_castAdd_Ioo ..

Premises used: Fin.finsetImage_castAdd_Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image castSucc (uIcc i j) = uIcc i.castSucc j.castSucc

Tactic:
finsetImage_castAdd_uIcc ..

Premises used: Fin.finsetImage_castAdd_uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image castSucc (Ici i) = Ico i.castSucc (last n)

Tactic:
finsetImage_castAdd_Ici ..

Premises used: Fin.finsetImage_castAdd_Ici
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image castSucc (Ioi i) = Ioo i.castSucc (last n)

Tactic:
finsetImage_castAdd_Ioi ..

Premises used: Fin.finsetImage_castAdd_Ioi
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image castSucc (Iic i) = Iic i.castSucc

Tactic:
finsetImage_castAdd_Iic ..

Premises used: Fin.finsetImage_castAdd_Iic
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image castSucc (Iio i) = Iio i.castSucc

Tactic:
finsetImage_castAdd_Iio ..

Premises used: Fin.finsetImage_castAdd_Iio
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map castSuccEmb (Icc i j) = Icc i.castSucc j.castSucc

Tactic:
map_castAddEmb_Icc ..

Premises used: Fin.castSuccEmb, Fin.map_castAddEmb_Icc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map castSuccEmb (Ico i j) = Ico i.castSucc j.castSucc

Tactic:
map_castAddEmb_Ico ..

Premises used: Fin.map_castAddEmb_Ico, Fin.castSuccEmb
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map castSuccEmb (Ioc i j) = Ioc i.castSucc j.castSucc

Tactic:
map_castAddEmb_Ioc ..

Premises used: Fin.map_castAddEmb_Ioc, Fin.castSuccEmb
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map castSuccEmb (Ioo i j) = Ioo i.castSucc j.castSucc

Tactic:
map_castAddEmb_Ioo ..

Premises used: Fin.castSuccEmb, Fin.map_castAddEmb_Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map castSuccEmb (uIcc i j) = uIcc i.castSucc j.castSucc

Tactic:
map_castAddEmb_uIcc ..

Premises used: Fin.map_castAddEmb_uIcc, Fin.castSuccEmb
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map castSuccEmb (Ici i) = Ico i.castSucc (last n)

Tactic:
map_castAddEmb_Ici ..

Premises used: Fin.map_castAddEmb_Ici, Fin.castSuccEmb
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map castSuccEmb (Ioi i) = Ioo i.castSucc (last n)

Tactic:
map_castAddEmb_Ioi ..

Premises used: Fin.castSuccEmb, Fin.map_castAddEmb_Ioi
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map castSuccEmb (Iic i) = Iic i.castSucc

Tactic:
map_castAddEmb_Iic ..

Premises used: Fin.castSuccEmb, Fin.map_castAddEmb_Iic
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map castSuccEmb (Iio i) = Iio i.castSucc

Tactic:
map_castAddEmb_Iio ..

Premises used: Fin.map_castAddEmb_Iio, Fin.castSuccEmb
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ico i j) = Ico (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ioc i j) = Ioc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (natAdd m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ici i) = Ici (natAdd m i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ioi i) = Ioi (natAdd m i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ico i j) = Ico (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioc i j) = Ioc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ici i) = Ici (natAdd m i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ioi i) = Ioi (natAdd m i)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (Ici i) = Ici (i.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ image (fun (x : Fin n) ↦ x.addNat m) (Ioi i) = Ioi (i.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ici i) = Ici (i.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ioi i) = Ioi (i.addNat m)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image succ (Icc i j) = Icc i.succ j.succ

Tactic:
finsetImage_addNat_Icc ..

Premises used: Fin.succ, Fin.finsetImage_addNat_Icc, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image succ (Ico i j) = Ico i.succ j.succ

Tactic:
finsetImage_addNat_Ico ..

Premises used: Fin.succ, Fin.finsetImage_addNat_Ico, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image succ (Ioc i j) = Ioc i.succ j.succ

Tactic:
finsetImage_addNat_Ioc ..

Premises used: Fin.succ, Fin.finsetImage_addNat_Ioc, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image succ (Ioo i j) = Ioo i.succ j.succ

Tactic:
finsetImage_addNat_Ioo ..

Premises used: Fin.succ, Fin.finsetImage_addNat_Ioo, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image succ (uIcc i j) = uIcc i.succ j.succ

Tactic:
finsetImage_addNat_uIcc ..

Premises used: Fin.succ, Fin.finsetImage_addNat_uIcc, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image succ (Ici i) = Ici i.succ

Tactic:
finsetImage_addNat_Ici ..

Premises used: Fin.finsetImage_addNat_Ici, Fin.succ, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image succ (Ioi i) = Ioi i.succ

Tactic:
finsetImage_addNat_Ioi ..

Premises used: Fin.finsetImage_addNat_Ioi, Fin.succ, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image succ (Iic i) = Ioc 0 i.succ

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image succ (Iio i) = Ioo 0 i.succ

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (succEmb n) (Icc i j) = Icc i.succ j.succ

Tactic:
map_addNatEmb_Icc ..

Premises used: Fin.succ, Fin.succEmb, Fin.map_addNatEmb_Icc, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (succEmb n) (Ico i j) = Ico i.succ j.succ

Tactic:
map_addNatEmb_Ico ..

Premises used: Fin.succ, Fin.map_addNatEmb_Ico, Fin.succEmb, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (succEmb n) (Ioc i j) = Ioc i.succ j.succ

Tactic:
map_addNatEmb_Ioc ..

Premises used: Fin.succ, Fin.succEmb, Fin.map_addNatEmb_Ioc, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (succEmb n) (Ioo i j) = Ioo i.succ j.succ

Tactic:
map_addNatEmb_Ioo ..

Premises used: Fin.succ, Fin.succEmb, Fin.map_addNatEmb_Ioo, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (succEmb n) (uIcc i j) = uIcc i.succ j.succ

Tactic:
map_addNatEmb_uIcc ..

Premises used: Fin.succ, Fin.succEmb, Fin.map_addNatEmb_uIcc, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (succEmb n) (Ici i) = Ici i.succ

Tactic:
map_addNatEmb_Ici ..

Premises used: Fin.map_addNatEmb_Ici, Fin.succ, Fin.succEmb, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (succEmb n) (Ioi i) = Ioi i.succ

Tactic:
map_addNatEmb_Ioi ..

Premises used: Fin.succ, Fin.map_addNatEmb_Ioi, Fin.succEmb, Fin.addNat
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (succEmb n) (Iic i) = Ioc 0 i.succ

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (succEmb n) (Iio i) = Ioo 0 i.succ

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image rev (Icc i j) = Icc j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image rev (Ico i j) = Ioc j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image rev (Ioc i j) = Ico j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image rev (Ioo i j) = Ioo j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ image rev (uIcc i j) = uIcc i.rev j.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image rev (Ici i) = Iic i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image rev (Ioi i) = Iio i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image rev (Iic i) = Ici i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ image rev (Iio i) = Ioi i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Icc i j) = Icc j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ico i j) = Ioc j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioc i j) = Ico j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioo i j) = Ioo j.rev i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (uIcc i j) = uIcc i.rev j.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ici i) = Iic i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioi i) = Iio i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj