awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a x : α
f : (↑(Ici a) : Type u_1) → β
hx : x ∈ Ici a
⊢ IciExtend f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) x hx)

Tactic:
congr_arg f <| projIci_of_mem hx

Premises used: Set.IciExtend, congr_arg, Set.projIci_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
b x : α
f : (↑(Iic b) : Type u_1) → β
hx : x ∈ Iic b
⊢ IicExtend f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) x hx)

Tactic:
congr_arg f <| projIic_of_mem hx

Premises used: congr_arg, Set.IicExtend, Set.projIic_of_mem
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
x : α
f : (↑(Icc a b) : Type u_1) → β
hx : x ∈ Icc a b
⊢ IccExtend h f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) x hx)

Tactic:
congr_arg f <| projIcc_of_mem h hx

Premises used: Set.projIcc_of_mem, congr_arg, Set.IccExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a : α
f : (↑(Ici a) : Type u_1) → β
x : (↑(Ici a) : Type u_1)
⊢ IciExtend f (↑x : α) = f x

Tactic:
congr_arg f <| projIci_coe x

Premises used: Set.IciExtend, congr_arg, Set.projIci_coe
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
b : α
f : (↑(Iic b) : Type u_1) → β
x : (↑(Iic b) : Type u_1)
⊢ IicExtend f (↑x : α) = f x

Tactic:
congr_arg f <| projIic_coe x

Premises used: Set.projIic_coe, congr_arg, Set.IicExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
x : (↑(Icc a b) : Type u_1)
⊢ IccExtend h f (↑x : α) = f x

Tactic:
congr_arg f <| projIcc_val h x

Premises used: congr_arg, Set.projIcc_val, Set.IccExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
h₁ : ∀ (x : α), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) = f

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
h₁ : ∀ (hxa : x < a), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
h₂ : ∀ (hax : a ≤ x), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x

Tactic:
rcases lt_or_ge x a with hxa | hax

Premises used: lt_or_ge
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hxa : x < a
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x

Tactic:
simp [IccExtend_of_le_left _ _ hxa.le, ha x hxa]

Premises used: LT.lt.le, Set.IccExtend_of_le_left
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
h₁ : ∀ (hxb : x ≤ b), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
h₂ : ∀ (hbx : b < x), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x

Tactic:
rcases le_or_gt x b with hxb | hbx

Premises used: le_or_gt
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ Icc a b

Tactic:
⟨hax, hxb⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
h₁ :
  ∀ (x : { x : α // x ∈ Icc a b }) (hax : a ≤ (↑x : α)) (hxb : (↑x : α) ≤ b),
    IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) (↑x : α) = f (↑x : α)
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x

Tactic:
lift x to Icc a b using ⟨hax, hxb⟩

Premises used: Set.Icc
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x : α // x ∈ Icc a b }
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
h₁ : (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f (↑x : α)
h₂ h₃ : f (↑x : α) = f (↑x : α)
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) (↑x : α) = f (↑x : α)

Tactic:
rw [IccExtend_val, comp_apply]

Premises used: Set.IccExtend_val, Function.comp_apply
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x

Tactic:
simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]

Premises used: LT.lt.le, Set.IccExtend_of_right_le
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : (↑(Ici a) : Type u_1) → β
hf : Monotone f
⊢ Monotone (IciExtend f)

Tactic:
hf.comp monotone_projIci

Premises used: Monotone.comp, Set.IciExtend, Set.monotone_projIci
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : (↑(Iic b) : Type u_1) → β
hf : Monotone f
⊢ Monotone (IicExtend f)

Tactic:
hf.comp monotone_projIic

Premises used: Set.monotone_projIic, Monotone.comp, Set.IicExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
hf : Monotone f
⊢ Monotone (IccExtend h f)

Tactic:
hf.comp <| monotone_projIcc h

Premises used: Monotone.comp, Set.monotone_projIcc, Set.IccExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a : α
f : (↑(Ici a) : Type u_1) → β
hf : StrictMono f
⊢ StrictMonoOn (IciExtend f) (Ici a)

Tactic:
hf.comp_strictMonoOn strictMonoOn_projIci

Premises used: Set.IciExtend, Set.strictMonoOn_projIci, StrictMono.comp_strictMonoOn
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : (↑(Iic b) : Type u_1) → β
hf : StrictMono f
⊢ StrictMonoOn (IicExtend f) (Iic b)

Tactic:
hf.comp_strictMonoOn strictMonoOn_projIic

Premises used: Set.strictMonoOn_projIic, StrictMono.comp_strictMonoOn, Set.IicExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
a b : α
h : a ≤ b
f : (↑(Icc a b) : Type u_1) → β
hf : StrictMono f
⊢ StrictMonoOn (IccExtend h f) (Icc a b)

Tactic:
hf.comp_strictMonoOn (strictMonoOn_projIcc h)

Premises used: Set.strictMonoOn_projIcc, StrictMono.comp_strictMonoOn, Set.IccExtend
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a : α
s : Set (↑(Ici a) : Type u_1)
hs : s.OrdConnected
⊢ OrdConnected.{u_1} (α := α) {x : α | IciExtend (a := a) (fun (x : (↑(Ici a) : Type u_1)) ↦ x ∈ s) x}

Tactic:
⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨max_le_max le_rfl hz.1, max_le_max le_rfl hz.2⟩⟩

Premises used: le_rfl, Set.OrdConnected.out, Set.OrdConnected.mk, And.right, And.left, max_le_max, And.intro
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
b : α
s : Set (↑(Iic b) : Type u_1)
hs : s.OrdConnected
⊢ OrdConnected.{u_1} (α := α) {x : α | IicExtend (b := b) (fun (x : (↑(Iic b) : Type u_1)) ↦ x ∈ s) x}

Tactic:
⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨min_le_min le_rfl hz.1, min_le_min le_rfl hz.2⟩⟩

Premises used: le_rfl, Set.OrdConnected.out, Set.OrdConnected.mk, And.right, And.left, And.intro, min_le_min
-- Module: Mathlib.Order.Interval.Set.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
hs : s.OrdConnected
⊢ OrdConnected.{u_1} (α := (↑t : Type u_1))
    {x : (↑t : Type u_1) | t.restrict (π := fun (x : α) ↦ Prop) (fun (x : α) ↦ x ∈ s) x}

Tactic:
⟨fun _ hx _ hy _ hz => hs.out hx hy hz⟩

Premises used: Set.OrdConnected.out, Set.OrdConnected.mk
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
rw : Order.succ (↑i : J) ∈ Iic j
⊢ (↑(Order.succ i) : J) = Order.succ (↑i : J)

Tactic:
rw [coe_succ_of_mem]

Premises used: coe_succ_of_mem
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
a : (↑i : J) < j
⊢ Order.succ (↑i : J) ∈ Iic j

Tactic:
apply Order.succ_le_of_lt

Premises used: Order.succ_le_of_lt
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ i ≠ ⊤

Tactic:
simpa using hi
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ (↑i : J) < j

Tactic:
exact lt_of_le_of_ne (α := Set.Iic j) le_top (by simpa using hi)

Premises used: le_top, lt_of_le_of_ne
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
rw : (↑(Order.succ i) : J) ∈ Iic j
⊢ Order.succ (↑i : J) ∈ Iic j

Tactic:
rw [← coe_succ_of_not_isMax hi]

Premises used: Set.Iic.coe_succ_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ (↑(Order.succ i) : J) ∈ Iic j

Tactic:
apply Subtype.coe_prop

Premises used: Subtype.coe_prop
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
a : (↑(Order.succ i) : J) = (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Iic j) (Order.succ (↑i : J)) ⋯) : J)
⊢ Order.succ i = Subtype.mk (p := fun (x : J) ↦ x ∈ Iic j) (Order.succ (↑i : J)) ⋯

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ (↑(Order.succ i) : J) = (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Iic j) (Order.succ (↑i : J)) ⋯) : J)

Tactic:
simp only [coe_succ_of_not_isMax hi]

Premises used: Set.Iic.coe_succ_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
rw : Order.pred (↑i : J) ∈ Ici j
⊢ (↑(Order.pred i) : J) = Order.pred (↑i : J)

Tactic:
rw [coe_pred_of_mem]

Premises used: coe_pred_of_mem
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
a : j < (↑i : J)
⊢ Order.pred (↑i : J) ∈ Ici j

Tactic:
apply Order.le_pred_of_lt

Premises used: Order.le_pred_of_lt
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ i ≠ ⊥

Tactic:
simpa using hi
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ j < (↑i : J)

Tactic:
exact lt_of_le_of_ne (α := Set.Ici j) bot_le (Ne.symm (by simpa using hi))

Premises used: Ne.symm, bot_le, lt_of_le_of_ne
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
rw : (↑(Order.pred i) : J) ∈ Ici j
⊢ Order.pred (↑i : J) ∈ Ici j

Tactic:
rw [← coe_pred_of_not_isMin hi]

Premises used: Set.Ici.coe_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ (↑(Order.pred i) : J) ∈ Ici j

Tactic:
apply Subtype.coe_prop

Premises used: Subtype.coe_prop
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
a : (↑(Order.pred i) : J) = (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) (Order.pred (↑i : J)) ⋯) : J)
⊢ Order.pred i = Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) (Order.pred (↑i : J)) ⋯

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.SuccOrder
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ (↑(Order.pred i) : J) = (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) (Order.pred (↑i : J)) ⋯) : J)

Tactic:
simp only [coe_pred_of_not_isMin hi]

Premises used: Set.Ici.coe_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
pos : ∀ (ha : IsMax a), Ico (succ a) b = Ioo a b
neg : ∀ (ha : ¬IsMax a), Ico (succ a) b = Ioo a b
⊢ Ico (succ a) b = Ioo a b

Tactic:
by_cases ha : IsMax a

Premises used: IsMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : IsMax a
pos : ∅ = Ioo a b
pos₁ pos₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Ico (succ a) b = Ioo a b

Tactic:
rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]

Premises used: Set.Ico_eq_empty, Order.le_succ, IsMax.mono, Set.Ioo_eq_empty, IsMax.not_lt
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
neg : ∀ (x : α), x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
⊢ Ico (succ a) b = Ioo a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
neg : succ a ≤ x ∧ x < b ↔ x ∈ Ioo a b
neg₁ : succ a ≤ x ∧ x < b ↔ a < x ∧ x < b
neg₂ neg₃ : a < x ∧ x < b ↔ a < x ∧ x < b
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b

Tactic:
rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

Premises used: Set.mem_Ioo, Set.mem_Ico, Order.succ_le_iff_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
b : α
h : ∀ (x : α), x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
⊢ Icc (succ a) b = Ioc a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
h : succ a ≤ x ∧ x ≤ b ↔ x ∈ Ioc a b
h₁ : succ a ≤ x ∧ x ≤ b ↔ a < x ∧ x ≤ b
h₂ h₃ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b

Tactic:
rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]

Premises used: Order.succ_le_iff_of_not_isMax, Set.mem_Icc, Set.mem_Ioc
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
h : ∀ (x : α), x ∈ Ico a (succ b) ↔ x ∈ Icc a b
⊢ Ico a (succ b) = Icc a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
h : a ≤ x ∧ x < succ b ↔ x ∈ Icc a b
h₁ : a ≤ x ∧ x < succ b ↔ a ≤ x ∧ x ≤ b
h₂ h₃ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b

Tactic:
rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]

Premises used: Set.mem_Ico, Set.mem_Icc, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
h : ∀ (x : α), x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
⊢ Ioo a (succ b) = Ioc a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
h : a < x ∧ x < succ b ↔ x ∈ Ioc a b
h₁ : a < x ∧ x < succ b ↔ a < x ∧ x ≤ b
h₂ h₃ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b

Tactic:
rw [mem_Ioo, mem_Ioc, lt_succ_iff_of_not_isMax hb]

Premises used: Set.mem_Ioo, Order.lt_succ_iff_of_not_isMax, Set.mem_Ioc
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
rw : Ioo a (succ b) = Ioc a b
rw₁ rw₂ : Ioc a b = Ioc a b
⊢ Ico (succ a) (succ b) = Ioc a b

Tactic:
rw [Ico_succ_left_eq_Ioo, Ioo_succ_right_eq_Ioc_of_not_isMax hb]

Premises used: Set.Ioo_succ_right_eq_Ioc_of_not_isMax, Set.Ico_succ_left_eq_Ioo
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
h₁ : ∀ (x : α), x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b
⊢ insert a (Icc (succ a) b) = Icc a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
x : α
h₁ : a ≤ x → a = x → x ≤ b
⊢ x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b

Tactic:
simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]

Premises used: Order.le_iff_eq_or_succ_le, eq_comm, or_and_left
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ a ≤ x → a = x → x ≤ b

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ succ b
h₁ : ∀ (x : α), x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)
⊢ insert (succ b) (Icc a b) = Icc a (succ b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ succ b
x : α
h₁ : x = succ b ∨ x ≤ b → x = succ b → a ≤ x
⊢ x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)

Tactic:
simp [or_and_left, le_succ_iff_eq_or_le]

Premises used: or_and_left, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x = succ b ∨ x ≤ b → x = succ b → a ≤ x

Tactic:
simp_all
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
rw : insert b (Ico a b) = Icc a b
rw₁ rw₂ : insert b (Ico a b) = insert b (Ico a b)
⊢ insert b (Ico a b) = Ico a (succ b)

Tactic:
rw [Ico_succ_right_of_not_isMax hb, ← Ico_insert_right h]

Premises used: Order.Ico_succ_right_of_not_isMax, Set.Ico_insert_right
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < b
rw : insert a (Ioo a b) = Ico a b
rw₁ rw₂ : insert a (Ioo a b) = insert a (Ioo a b)
⊢ insert a (Ico (succ a) b) = Ico a b

Tactic:
rw [Ico_succ_left_of_not_isMax h.not_isMax, ← Ioo_insert_left h]

Premises used: Order.Ico_succ_left_of_not_isMax, Set.Ioo_insert_left, LT.lt.not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
h₁ : ∀ (x : α), x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ b)
⊢ insert (succ b) (Ioc a b) = Ioc a (succ b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
x : α
⊢ x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ b)

Tactic:
simp +contextual [or_and_left, le_succ_iff_eq_or_le, lt_succ_of_le_of_not_isMax h hb]

Premises used: or_and_left, Order.lt_succ_of_le_of_not_isMax, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < b
rw : Icc (succ a) b = Ioc a b
rw₁ rw₂ : Ioc a b = Ioc a b
⊢ insert (succ a) (Ioc (succ a) b) = Ioc a b

Tactic:
rw [Ioc_insert_left (succ_le_of_lt h), Icc_succ_left_of_not_isMax h.not_isMax]

Premises used: Order.Icc_succ_left_of_not_isMax, Set.Ioc_insert_left, Order.succ_le_of_lt, LT.lt.not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Icc (succ a) b = Ioc a b

Tactic:
Icc_succ_left_eq_Ioc_of_not_isMax (not_isMax _) _

Premises used: not_isMax, Set.Icc_succ_left_eq_Ioc_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ico a (succ b) = Icc a b

Tactic:
Ico_succ_right_eq_Icc_of_not_isMax (not_isMax _) _

Premises used: Set.Ico_succ_right_eq_Icc_of_not_isMax, not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ioo a (succ b) = Ioc a b

Tactic:
Ioo_succ_right_eq_Ioc_of_not_isMax (not_isMax _) _

Premises used: Set.Ioo_succ_right_eq_Ioc_of_not_isMax, not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a b : α
⊢ Ico (succ a) (succ b) = Ioc a b

Tactic:
Ico_succ_succ_eq_Ioc_of_not_isMax (not_isMax _) _

Premises used: not_isMax, Set.Ico_succ_succ_eq_Ioc_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (succ b)

Tactic:
insert_Ico_right_eq_Ico_succ_of_not_isMax h (not_isMax _)

Premises used: Set.insert_Ico_right_eq_Ico_succ_of_not_isMax, not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : a ≤ b
⊢ insert (succ b) (Ioc a b) = Ioc a (succ b)

Tactic:
insert_Ioc_right_eq_Ioc_succ_of_not_isMax h (not_isMax _)

Premises used: not_isMax, Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
pos : ∀ (hb : IsMin b), Ioc a (pred b) = Ioo a b
neg : ∀ (hb : ¬IsMin b), Ioc a (pred b) = Ioo a b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
by_cases hb : IsMin b

Premises used: IsMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : IsMin b
pos : ∅ = Ioo a b
pos₁ pos₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Ioc a (pred b) = Ioo a b

Tactic:
rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]

Premises used: IsMin.not_lt, IsMin.mono, Set.Ioc_eq_empty, Order.pred_le, Set.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : ¬IsMin b
neg : ∀ (x : α), x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : ¬IsMin b
x : α
neg : a < x ∧ x ≤ pred b ↔ x ∈ Ioo a b
neg₁ : a < x ∧ x ≤ pred b ↔ a < x ∧ x < b
neg₂ neg₃ : a < x ∧ x < b ↔ a < x ∧ x < b
⊢ x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b

Tactic:
rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]

Premises used: Set.mem_Ioo, Order.le_pred_iff_of_not_isMin, Set.mem_Ioc
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
a : α
h : ∀ (x : α), x ∈ Icc a (pred b) ↔ x ∈ Ico a b
⊢ Icc a (pred b) = Ico a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
a x : α
h : a ≤ x ∧ x ≤ pred b ↔ x ∈ Ico a b
h₁ : a ≤ x ∧ x ≤ pred b ↔ a ≤ x ∧ x < b
h₂ h₃ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b

Tactic:
rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]

Premises used: Set.mem_Ico, Order.le_pred_iff_of_not_isMin, Set.mem_Icc
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
h : ∀ (x : α), x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
⊢ Ioc (pred a) b = Icc a b

Tactic:
ext x