awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioc a b) = map (addRightEmbedding c) (Ioc a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioc a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b))
    (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ioc a b))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioc a b)) (image (fun (h : α) ↦ h + c) (Ioc a b))
⊢ image (fun (x : α) ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Premises used: Finset.map_eq_image, Finset.map_add_right_Ioc, Function.Embedding.coeFn_mk, addRightEmbedding
-- Module: Mathlib.Algebra.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
inst_5 : DecidableEq α
a b c : α
rw : image (fun (x : α) ↦ x + c) (Ioo a b) = map (addRightEmbedding c) (Ioo a b)
rw₁ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b)) (image (⇑(addRightEmbedding c) : (a : α) → α) (Ioo a b))
rw₂ :
  Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b))
    (image (⇑{ toFun := fun (h : α) ↦ h + c, inj' := ⋯ : α ↪ α } : (a : α) → α) (Ioo a b))
rw₃ rw₄ : Eq (α := Finset α) (image (fun (x : α) ↦ x + c) (Ioo a b)) (image (fun (h : α) ↦ h + c) (Ioo a b))
⊢ image (fun (x : α) ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Premises used: Finset.map_eq_image, Finset.map_add_right_Ioo, Function.Embedding.coeFn_mk, addRightEmbedding
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_left_eq_Ioo a b

Premises used: Order.succ_eq_add_one, Finset.Ico_succ_left_eq_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc_of_not_isMax ha b

Premises used: Order.succ_eq_add_one, Finset.Icc_succ_left_eq_Ioc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc_of_not_isMax hb a

Premises used: Finset.Ico_succ_right_eq_Icc_of_not_isMax, Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc_of_not_isMax hb a

Premises used: Order.succ_eq_add_one, Finset.Ioo_succ_right_eq_Ioc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a

Premises used: Order.succ_eq_add_one, Finset.Ico_succ_succ_eq_Ioc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b

Tactic:
simpa [succ_eq_add_one] using insert_Icc_succ_left_eq_Icc h

Premises used: Order.succ_eq_add_one, Finset.insert_Icc_succ_left_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
h : a ≤ b + 1
⊢ insert (b + 1) (Icc a b) = Icc a (b + 1)

Tactic:
simpa [← succ_eq_add_one] using insert_Icc_right_eq_Icc_succ (succ_eq_add_one b ▸ h)

Premises used: Order.succ_eq_add_one, Finset.insert_Icc_right_eq_Icc_succ
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ_of_not_isMax h hb

Premises used: Order.succ_eq_add_one, Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
h : a < b
⊢ insert a (Ico (a + 1) b) = Ico a b

Tactic:
simpa [succ_eq_add_one] using insert_Ico_succ_left_eq_Ico h

Premises used: Finset.insert_Ico_succ_left_eq_Ico, Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ioc_right_eq_Ioc_succ_of_not_isMax h hb

Premises used: Order.succ_eq_add_one, Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
h : a < b
⊢ insert (a + 1) (Ioc (a + 1) b) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using insert_Ioc_succ_left_eq_Ioc h

Premises used: Order.succ_eq_add_one, Finset.insert_Ioc_succ_left_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b

Premises used: Order.succ_eq_add_one, Finset.Icc_succ_left_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc a b

Premises used: Order.succ_eq_add_one, Finset.Ico_succ_right_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

Premises used: Order.succ_eq_add_one, Finset.Ioo_succ_right_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b

Premises used: Order.succ_eq_add_one, Finset.Ico_succ_succ_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
inst_5 : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ h

Premises used: Order.succ_eq_add_one, Finset.insert_Ico_right_eq_Ico_succ
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : SuccAddOrder α
a b : α
inst_5 : NoMaxOrder α
h : a ≤ b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Tactic:
insert_Ioc_right_eq_Ioc_add_one_of_not_isMax h (not_isMax _)

Premises used: not_isMax, Finset.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
⊢ Ioc a (b - 1) = Ioo a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_right_eq_Ioo a b

Premises used: Order.pred_eq_sub_one, Finset.Ioc_pred_right_eq_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico_of_not_isMin hb a

Premises used: Finset.Icc_pred_right_eq_Ico_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc_of_not_isMin ha b

Premises used: Order.pred_eq_sub_one, Finset.Ioc_pred_left_eq_Icc_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc_of_not_isMin ha b

Premises used: Order.pred_eq_sub_one, Finset.Ioo_pred_left_eq_Ioc_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico_of_not_isMin ha b

Premises used: Order.pred_eq_sub_one, Finset.Ioc_pred_pred_eq_Ico_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b

Tactic:
simpa [pred_eq_sub_one] using insert_Icc_pred_right_eq_Icc h

Premises used: Order.pred_eq_sub_one, Finset.insert_Icc_pred_right_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
h : a - 1 ≤ b
⊢ insert (a - 1) (Icc a b) = Icc (a - 1) b

Tactic:
simpa [← pred_eq_sub_one] using insert_Icc_left_eq_Icc_pred (pred_eq_sub_one a ▸ h)

Premises used: Order.pred_eq_sub_one, Finset.insert_Icc_left_eq_Icc_pred
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred_of_not_isMin h ha

Premises used: Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (b - 1)) = Ioc a b

Tactic:
simpa [pred_eq_sub_one] using insert_Ioc_pred_right_eq_Ioc h

Premises used: Finset.insert_Ioc_pred_right_eq_Ioc, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

Premises used: Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
h : a < b
⊢ insert (b - 1) (Ico a (b - 1)) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using insert_Ico_pred_right_eq_Ico h

Premises used: Order.pred_eq_sub_one, Finset.insert_Ico_pred_right_eq_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
inst_5 : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico a b

Premises used: Order.pred_eq_sub_one, Finset.Icc_pred_right_eq_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
inst_5 : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b

Premises used: Order.pred_eq_sub_one, Finset.Ioc_pred_left_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
inst_5 : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc a b

Premises used: Order.pred_eq_sub_one, Finset.Ioo_pred_left_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
inst_5 : NoMinOrder α
a b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico a b

Premises used: Order.pred_eq_sub_one, Finset.Ioc_pred_pred_eq_Ico
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
inst_5 : NoMinOrder α
h : a ≤ b
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred h

Premises used: Order.pred_eq_sub_one, Finset.insert_Ioc_left_eq_Ioc_pred
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Sub α
inst_4 : PredSubOrder α
a b : α
inst_5 : NoMinOrder α
h : a ≤ b
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
insert_Ico_left_eq_Ico_sub_one_of_not_isMin h (not_isMin _)

Premises used: not_isMin, Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrder α
inst_3 : Add α
inst_4 : Sub α
inst_5 : SuccAddOrder α
inst_6 : PredSubOrder α
inst_7 : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b

Premises used: Order.succ_eq_add_one, Finset.Icc_succ_pred_eq_Ioo, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderBot α
inst_3 : Add α
inst_4 : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

Premises used: Order.succ_eq_add_one, Finset.Iio_succ_eq_Iic_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderBot α
inst_3 : Add α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

Premises used: Order.succ_eq_add_one, Finset.Iio_succ_eq_Iic
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderBot α
inst_3 : Sub α
inst_4 : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb

Premises used: Order.pred_eq_sub_one, Finset.Iic_pred_eq_Iio_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderBot α
inst_3 : Sub α
inst_4 : PredSubOrder α
inst_5 : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

Premises used: Finset.Iic_pred_eq_Iio, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderTop α
inst_3 : Add α
inst_4 : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi_of_not_isMax ha

Premises used: Finset.Ici_succ_eq_Ioi_of_not_isMax, Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderTop α
inst_3 : Add α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

Premises used: Order.succ_eq_add_one, Finset.Ici_succ_eq_Ioi
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderTop α
inst_3 : Sub α
inst_4 : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici_of_not_isMin ha

Premises used: Finset.Ioi_pred_eq_Ici_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : LocallyFiniteOrderTop α
inst_3 : Sub α
inst_4 : PredSubOrder α
inst_5 : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

Premises used: Order.pred_eq_sub_one, Finset.Ioi_pred_eq_Ici
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = Icc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
rw₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val))
rw₄ rw₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

Premises used: Multiset.Nodup.map, Multiset.Icc, add_right_injective, Finset.nodup, Multiset.Nodup.dedup, Finset.image_add_left_Icc, Finset.image_val
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = Icc (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Icc a b).val = (Finset.Icc (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Icc a b)))
classical₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val))
classical₄ classical₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Icc a b).val)
⊢ map (fun (x : α) ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

Premises used: Multiset.Icc, Finset.image_add_left_Icc, Finset.image_val
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
rw₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val))
rw₄ rw₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

Premises used: Multiset.Nodup.map, add_right_injective, Finset.nodup, Multiset.Ico, Multiset.Nodup.dedup, Finset.image_val, Finset.image_add_left_Ico
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
classical : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = Ico (c + a) (c + b)
classical₁ : map (fun (x : α) ↦ c + x) (Finset.Ico a b).val = (Finset.Ico (c + a) (c + b)).val
classical₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ico a b)))
classical₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val))
classical₄ classical₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ico a b).val)
⊢ map (fun (x : α) ↦ c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
classical rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

Premises used: Multiset.Ico, Finset.image_val, Finset.image_add_left_Ico
-- Module: Mathlib.Algebra.Order.Interval.Multiset
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : ExistsAddOfLE α
inst_4 : LocallyFiniteOrder α
a b c : α
rw : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = Ioc (c + a) (c + b)
rw₁ : map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val
rw₂ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (Finset.val (Finset.image (fun (x : α) ↦ c + x) (Finset.Ioc a b)))
rw₃ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
    (dedup (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val))
rw₄ rw₅ :
  Eq (α := Multiset α) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val) (map (fun (x : α) ↦ c + x) (Finset.Ioc a b).val)
⊢ map (fun (x : α) ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

Premises used: Multiset.Nodup.map, add_right_injective, Finset.nodup, Multiset.Nodup.dedup, Multiset.Ioc, Finset.image_val, Finset.image_add_left_Ioc