awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d x : M
h : x ∈ Ici (a + d)
obtain :
  ∀ (c : M) (h : a + d + c ∈ Ici (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) (a + d + c)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) x

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)

Premises used: ExistsAddOfLE.exists_add_of_le, Set.mem_Ici, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a ≤ a + c

Tactic:
rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h

Premises used: add_right_comm, add_le_add_iff_right, Set.mem_Ici
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
rw rw₁ : (fun (x : M) ↦ x + d) (a + c) = a + c + d
⊢ (fun (x : M) ↦ x + d) (a + c) = a + d + c

Tactic:
rw [add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) (a + d + c)

Tactic:
exact ⟨a + c, h, by rw [add_right_comm]⟩
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
⊢ MapsTo (fun (x : M) ↦ x + d) (Ioi a) (Ioi (a + d))

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
⊢ InjOn (β := M) (fun (x : M) ↦ x + d) (Ioi a)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
refine : ∀ (x : M) (h : x ∈ Ioi (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) x
⊢ BijOn (fun (x : M) ↦ x + d) (Ioi a) (Ioi (a + d))

Tactic:
refine ⟨by simp [MapsTo], by simp, fun _ h => ?_⟩
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d x : M
h : x ∈ Ioi (a + d)
obtain :
  ∀ (c : M) (h : a + d + c ∈ Ioi (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) (a + d + c)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) x

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le

Premises used: Set.mem_Ioi, LT.lt.le, ExistsAddOfLE.exists_add_of_le, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a < a + c

Tactic:
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h

Premises used: Set.mem_Ioi, add_right_comm, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a < a + c
rw rw₁ : (fun (x : M) ↦ x + d) (a + c) = a + c + d
⊢ (fun (x : M) ↦ x + d) (a + c) = a + d + c

Tactic:
rw [add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) (a + d + c)

Tactic:
exact ⟨a + c, h, by rw [add_right_comm]⟩
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
rw : BijOn (fun (x : M) ↦ x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))
⊢ BijOn (fun (x : M) ↦ x + d) (Icc a b) (Icc (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iic, ← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ MapsTo (fun (x : M) ↦ x + d) (Iic b) (Iic (b + d))

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))

Tactic:
exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => le_of_add_le_add_right hx.2

Premises used: le_of_add_le_add_right, Set.BijOn.inter_mapsTo, Set.Ici_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
rw : BijOn (fun (x : M) ↦ x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))
⊢ BijOn (fun (x : M) ↦ x + d) (Ioo a b) (Ioo (a + d) (b + d))

Tactic:
rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ MapsTo (fun (x : M) ↦ x + d) (Iio b) (Iio (b + d))

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))

Tactic:
exact (Ioi_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => lt_of_add_lt_add_right hx.2

Premises used: Set.Ioi_add_bij, lt_of_add_lt_add_right, Set.BijOn.inter_mapsTo
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
rw : BijOn (fun (x : M) ↦ x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
⊢ BijOn (fun (x : M) ↦ x + d) (Ioc a b) (Ioc (a + d) (b + d))

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))

Tactic:
exact (Ioi_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => le_of_add_le_add_right hx.2

Premises used: le_of_add_le_add_right, Set.Ioi_add_bij, Set.BijOn.inter_mapsTo
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
rw : BijOn (fun (x : M) ↦ x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
⊢ BijOn (fun (x : M) ↦ x + d) (Ico a b) (Ico (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))

Tactic:
exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => lt_of_add_lt_add_right hx.2

Premises used: lt_of_add_lt_add_right, Set.BijOn.inter_mapsTo, Set.Ici_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b : M
⊢ (fun (x : M) ↦ x + a) '' Ici b = Ici (b + a)

Tactic:
(Ici_add_bij _ _).image_eq

Premises used: Set.BijOn.image_eq, Set.Ici_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b : M
⊢ (fun (x : M) ↦ x + a) '' Ioi b = Ioi (b + a)

Tactic:
(Ioi_add_bij _ _).image_eq

Premises used: Set.BijOn.image_eq, Set.Ioi_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ x + a) '' Icc b c = Icc (b + a) (c + a)

Tactic:
(Icc_add_bij _ _ _).image_eq

Premises used: Set.BijOn.image_eq, Set.Icc_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ x + a) '' Ico b c = Ico (b + a) (c + a)

Tactic:
(Ico_add_bij _ _ _).image_eq

Premises used: Set.Ico_add_bij, Set.BijOn.image_eq
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ x + a) '' Ioc b c = Ioc (b + a) (c + a)

Tactic:
(Ioc_add_bij _ _ _).image_eq

Premises used: Set.BijOn.image_eq, Set.Ioc_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ x + a) '' Ioo b c = Ioo (b + a) (c + a)

Tactic:
(Ioo_add_bij _ _ _).image_eq

Premises used: Set.BijOn.image_eq, Set.Ioo_add_bij
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b : M
⊢ (fun (x : M) ↦ a + x) '' Ici b = Ici (a + b)

Tactic:
simp only [add_comm a, image_add_const_Ici]

Premises used: add_comm, Set.image_add_const_Ici
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b : M
⊢ (fun (x : M) ↦ a + x) '' Ioi b = Ioi (a + b)

Tactic:
simp only [add_comm a, image_add_const_Ioi]

Premises used: add_comm, Set.image_add_const_Ioi
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ a + x) '' Icc b c = Icc (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Icc]

Premises used: add_comm, Set.image_add_const_Icc
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ a + x) '' Ico b c = Ico (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ico]

Premises used: add_comm, Set.image_add_const_Ico
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ a + x) '' Ioc b c = Ioc (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ioc]

Premises used: add_comm, Set.image_add_const_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b c : M
⊢ (fun (x : M) ↦ a + x) '' Ioo b c = Ioo (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ioo]

Premises used: add_comm, Set.image_add_const_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.Ico_succ_left_eq_Ioo
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.Icc_succ_left_eq_Ioc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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: Order.succ_eq_add_one, Set.Ico_succ_right_eq_Icc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.Ioo_succ_right_eq_Ioc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.Ico_succ_succ_eq_Ioc_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.insert_Icc_succ_left_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.insert_Icc_right_eq_Icc_succ
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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: Set.insert_Ico_right_eq_Ico_succ_of_not_isMax, Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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: Order.succ_eq_add_one, Set.insert_Ico_succ_left_eq_Ico
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : 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, Set.insert_Ioc_succ_left_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
inst_4 : 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: Set.Icc_succ_left_eq_Ioc, Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
inst_4 : 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, Set.Ico_succ_right_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
inst_4 : 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, Set.Ioo_succ_right_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
inst_4 : 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, Set.Ico_succ_succ_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
a b : α
inst_4 : 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, Set.insert_Ico_right_eq_Ico_succ
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
a b : α
inst_4 : 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, Set.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Set.Ioc_pred_right_eq_Ioo, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Order.pred_eq_sub_one, Set.Icc_pred_right_eq_Ico_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Set.Ioc_pred_left_eq_Icc_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Set.Ioo_pred_left_eq_Ioc_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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, Set.Ioc_pred_pred_eq_Ico_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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, Set.insert_Icc_pred_right_eq_Icc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Set.insert_Icc_left_eq_Icc_pred, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Order.pred_eq_sub_one, Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Set.insert_Ioc_pred_right_eq_Ioc, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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: Set.insert_Ico_left_eq_Ico_pred_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : 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, Set.insert_Ico_pred_right_eq_Ico
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
inst_4 : 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: Set.Icc_pred_right_eq_Ico, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
inst_4 : 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: Set.Ioc_pred_left_eq_Icc, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
inst_4 : 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, Set.Ioo_pred_left_eq_Ioc
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
inst_4 : 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, Set.Ioc_pred_pred_eq_Ico
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
a b : α
inst_4 : 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, Set.insert_Ioc_left_eq_Ioc_pred
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
a b : α
inst_4 : 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, Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMin