awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
⊢ Function.RightInverse (α := k) (fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
fun x ↦ Subtype.ext ?_

Premises used: Function.LeftInverse, Function.RightInverse, Subtype.ext
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_3 :
  ∀ (x : (↑(Ioo (-1) 1) : Type u_1)),
    (↑(codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯
            ((fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|)) x)) :
        k) =
      (↑x : k)
⊢ Function.RightInverse (α := k) (fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
refine fun x ↦ Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : (↑(Ioo (-1) 1) : Type u_1)
⊢ 0 < 1 - |(↑x : k)|

Tactic:
have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : (↑(Ioo (-1) 1) : Type u_1)
this : 0 < 1 - |(↑x : k)|
⊢ (↑(codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯
          ((fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|)) x)) :
      k) =
    (↑x : k)

Tactic:
simp [field, abs_div, abs_of_pos this]

Premises used: abs_div, abs_of_pos
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
simp : b < (↑m : J) → ∃ (x : J) (_ : b < x), x < (↑m : J)
⊢ ¬b ⋖ (↑m : J)

Tactic:
simp only [CovBy, not_lt, not_and, not_forall, not_le]

Premises used: not_le, CovBy, not_lt, not_and, Classical.not_forall
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
pos : ∀ (hb' : j ≤ b), ∃ (x : J) (_ : b < x), x < (↑m : J)
neg : ∀ (hb' : ¬j ≤ b), ∃ (x : J) (_ : b < x), x < (↑m : J)
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)

Tactic:
by_cases hb' : j ≤ b
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
⊢ ¬Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' ⋖ m

Tactic:
have := hm.2 ⟨b, hb'⟩
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
this : ¬Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' ⋖ m
⊢ Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < m

Tactic:
hb
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
this : ¬Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' ⋖ m
⊢ Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < m

Tactic:
exact hb
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
this : ¬Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' ⋖ m
⊢ ∃ (c : (↑(Ici j) : Type u)), Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < c ∧ c < m

Tactic:
rw [not_covBy_iff (by exact hb)] at this

Premises used: not_covBy_iff
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
this : ∃ (c : (↑(Ici j) : Type u)), Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < c ∧ c < m
pos :
  ∀ (x : J) (h₁ : x ∈ Ici j)
    (h₂ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁)
    (h₃ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁ < m), ∃ (x : J) (_ : b < x), x < (↑m : J)
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)

Tactic:
obtain ⟨⟨x, h₁⟩, h₂, h₃⟩ := this
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
x : J
h₁ : x ∈ Ici j
h₂ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁
h₃ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁ < m
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)

Tactic:
⟨x, h₂, h₃⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
x : J
h₁ : x ∈ Ici j
h₂ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁
h₃ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁ < m
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)

Tactic:
refine ⟨x, h₂, h₃⟩
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : ¬j ≤ b
⊢ b < j

Tactic:
simp only [not_le] at hb'

Premises used: not_le
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)

Tactic:
⟨j, hb', ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
neg : j < (↑m : J)
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)

Tactic:
refine ⟨j, hb', ?_⟩
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
neg : ∀ (this : (↑m : J) ≤ j), False
⊢ j < (↑m : J)

Tactic:
by_contra!
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
this : (↑m : J) ≤ j
neg : IsMin m
⊢ False

Tactic:
apply hm.1

Premises used: And.left
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
this : (↑m : J) ≤ j
k : J
hk : k ∈ Ici j
h : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) k hk ≤ m
⊢ j ≤ (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) k hk) : J)

Tactic:
simpa using hk
-- Module: Mathlib.Order.Interval.Set.Limit
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
this : (↑m : J) ≤ j
k : J
hk : k ∈ Ici j
h : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) k hk ≤ m
⊢ m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) k hk

Tactic:
exact this.trans (by simpa using hk)

Premises used: LE.le.trans
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a c : α
⊢ ¬c ∈ Ici a ↔ c < a

Tactic:
not_le

Premises used: not_le, Set.Ici, Set.Mem, setOf
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a c : α
⊢ ¬c ∈ Ioi a ↔ c ≤ a

Tactic:
not_lt

Premises used: Set.Ioi, Set.Mem, setOf, not_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ (Iic a)ᶜ = Ioi a

Tactic:
ext fun _ => not_le

Premises used: not_le, Set.ext
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ (Iio a)ᶜ = Ici a

Tactic:
ext fun _ => not_lt

Premises used: Set.ext, not_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ici a ∩ (Ici b)ᶜ = Ico a b
rw₁ : Ici a ∩ Iio b = Ico a b
rw₂ rw₃ : Ico a b = Ico a b
⊢ Ici a \ Ici b = Ico a b

Tactic:
rw [diff_eq, compl_Ici, Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio, Set.diff_eq, Set.compl_Ici
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ici a ∩ (Ioi b)ᶜ = Icc a b
rw₁ : Ici a ∩ Iic b = Icc a b
rw₂ rw₃ : Icc a b = Icc a b
⊢ Ici a \ Ioi b = Icc a b

Tactic:
rw [diff_eq, compl_Ioi, Ici_inter_Iic]

Premises used: Set.diff_eq, Set.compl_Ioi, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ioi a ∩ (Ioi b)ᶜ = Ioc a b
rw₁ : Ioi a ∩ Iic b = Ioc a b
rw₂ rw₃ : Ioc a b = Ioc a b
⊢ Ioi a \ Ioi b = Ioc a b

Tactic:
rw [diff_eq, compl_Ioi, Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic, Set.diff_eq, Set.compl_Ioi
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ioi a ∩ (Ici b)ᶜ = Ioo a b
rw₁ : Ioi a ∩ Iio b = Ioo a b
rw₂ rw₃ : Ioo a b = Ioo a b
⊢ Ioi a \ Ici b = Ioo a b

Tactic:
rw [diff_eq, compl_Ici, Ioi_inter_Iio]

Premises used: Set.diff_eq, Set.Ioi_inter_Iio, Set.compl_Ici
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) Ioi

Tactic:
fun _ _ =>
  eq_of_forall_gt_iff ∘ Set.ext_iff.1

Premises used: eq_of_forall_gt_iff, Function.comp, Iff.mp, Set.ext_iff, Function.Injective
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a = Ioi b ↔ a = b

Tactic:
Ioi_injective.eq_iff

Premises used: Function.Injective.eq_iff, Set.Ioi_injective
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
⟨fun h =>
    have : a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_rfl, h₁⟩
    ⟨this.1, le_of_not_gt fun h' => lt_irrefl b₂ (h ⟨this.2.le, h'⟩).2⟩,
    fun ⟨h₁, h₂⟩ => Ico_subset_Ico h₁ h₂⟩

Premises used: lt_irrefl, le_rfl, le_of_not_gt, LT.lt.le, HasSubset.Subset, Set.Ico_subset_Ico, Set.Ico, And.right, And.left, And.intro, Iff.intro, _private.0.Set.Ico_subset_Ico_iff.match_1
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
⊢ Ico b₁ a₁ ⊆ Ico b₂ a₂ ↔ b₂ ≤ b₁ ∧ a₁ ≤ a₂

Tactic:
@Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁

Premises used: Set.Ico_subset_Ico_iff
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
h : Set α = Set αᵒᵈ → Ioc a₁ b₁ = Ico b₁ a₁
h₂ : Set α = Set αᵒᵈ → Ioc a₂ b₂ = Ico b₂ a₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁

Tactic:
convert! @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2

Premises used: Set.Ico_subset_Ico_iff
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1 : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁

Tactic:
(@Ico_toDual α _ _ _).symm

Premises used: Set.Ioc, Set.Mem, setOf, Set.Ico_toDual, Set.preimage, OrderDual, Eq.symm
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1 : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁

Tactic:
exact (@Ico_toDual α _ _ _).symm

Premises used: Set.Ico_toDual, Eq.symm
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1 : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂

Tactic:
(@Ico_toDual α _ _ _).symm

Premises used: Set.Ioc, Set.Mem, setOf, Set.Ico_toDual, Set.preimage, OrderDual, Eq.symm
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1 : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂

Tactic:
exact (@Ico_toDual α _ _ _).symm

Premises used: Set.Ico_toDual, Eq.symm
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h : a < b ∨ c < d
⊢ a = c ∧ b = d → Ico a b = Ico c d

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h : a < b ∨ c < d
refine : ∀ (h : Ico a b = Ico c d), a = c ∧ b = d
⊢ Ico a b = Ico c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun h ↦ ?_, by grind⟩
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
⊢ a < b

Tactic:
grind [Set.nonempty_Ico]

Premises used: Set.nonempty_Ico
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
⊢ c ≤ a ∧ b ≤ d

Tactic:
have : c ≤ a ∧ b ≤ d := (Ico_subset_Ico_iff (show a < b by grind [Set.nonempty_Ico])).1 h.subset
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
this : c ≤ a ∧ b ≤ d
⊢ c < d

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
this : c ≤ a ∧ b ≤ d
⊢ a ≤ c ∧ d ≤ b

Tactic:
have : a ≤ c ∧ d ≤ b := (Ico_subset_Ico_iff (show c < d by grind)).1 h.superset
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
this_1 : c ≤ a ∧ b ≤ d
this : a ≤ c ∧ d ≤ b
⊢ a = c ∧ b = d

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
⊢ a = c ∧ b = d → Ioc a b = Ioc c d

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
refine : ∀ (h : Ioc a b = Ioc c d), a = c ∧ b = d
⊢ Ioc a b = Ioc c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun h ↦ ?_, by grind⟩
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
⊢ a < b

Tactic:
grind [Set.nonempty_Ioc]

Premises used: Set.nonempty_Ioc
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
⊢ b ≤ d ∧ c ≤ a

Tactic:
have : b ≤ d ∧ c ≤ a := (Ioc_subset_Ioc_iff (show a < b by grind [Set.nonempty_Ioc])).1 h.subset
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this : b ≤ d ∧ c ≤ a
⊢ c < d

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this : b ≤ d ∧ c ≤ a
⊢ d ≤ b ∧ a ≤ c

Tactic:
have : d ≤ b ∧ a ≤ c := (Ioc_subset_Ioc_iff (show c < d by grind)).1 h.superset
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this_1 : b ≤ d ∧ c ≤ a
this : d ≤ b ∧ a ≤ c
⊢ a = c ∧ b = d

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
rcases : ∀ (x : α) (xa : a₁ < x) (xb : x < b₁), a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rcases exists_between h₁ with ⟨x, xa, xb⟩

Premises used: exists_between
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
left : a₂ ≤ a₁
right : b₁ ≤ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁

Tactic:
le_of_not_gt fun h' => ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
left : ∀ (h' : a₁ < a₂), False
⊢ a₂ ≤ a₁

Tactic:
refine le_of_not_gt fun h' => ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂

Tactic:
le_of_not_gt fun h' => ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
right : ∀ (h' : b₂ < b₁), False
⊢ b₁ ≤ b₂

Tactic:
refine le_of_not_gt fun h' => ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ a₂ < b₁

Tactic:
have ab := (h ⟨xa, xb⟩).1.trans xb
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False

Tactic:
lt_irrefl _ (h ⟨h', ab⟩).1

Premises used: lt_irrefl, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False

Tactic:
exact lt_irrefl _ (h ⟨h', ab⟩).1

Premises used: lt_irrefl, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ a₁ < b₂

Tactic:
have ab := xa.trans (h ⟨xa, xb⟩).2
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
ab : a₁ < b₂
⊢ False

Tactic:
lt_irrefl _ (h ⟨ab, h'⟩).2

Premises used: lt_irrefl, And.right, And.intro
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
ab : a₁ < b₂
⊢ False

Tactic:
exact lt_irrefl _ (h ⟨ab, h'⟩).2

Premises used: lt_irrefl, And.right, And.intro
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : IsTop x
h₁ : ∀ (y : α), y ∈ Ici x ↔ Membership.mem (γ := Set α) {x} y
⊢ Ici x = {x}

Tactic:
ext y
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : IsTop x
y : α
⊢ y ∈ Ici x ↔ Membership.mem (γ := Set α) {x} y

Tactic:
simp [(h y).ge_iff_eq]

Premises used: LE.le.ge_iff_eq
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
refine : ∀ (h : Ici x = {x}) (y : α), y ≤ x
⊢ Ici x = {x} ↔ IsTop x

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
by_contra! : ∀ (H : x < y), False
⊢ y ≤ x

Tactic:
by_contra! H
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
⊢ y ∈ Ici x

Tactic:
have : y ∈ Ici x := H.le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ Ici x
⊢ y = x

Tactic:
rw [h, mem_singleton_iff] at this

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False

Tactic:
lt_irrefl y (this.le.trans_lt H)

Premises used: lt_irrefl, Eq.le, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False

Tactic:
exact lt_irrefl y (this.le.trans_lt H)

Premises used: lt_irrefl, Eq.le, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b

Tactic:
⟨fun h => ?_, Ioi_subset_Ioi⟩

Premises used: Iff.intro, Set.Ioi_subset_Ioi
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
refine : ∀ (h : Ioi b ⊆ Ioi a), a ≤ b
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, Ioi_subset_Ioi⟩
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
by_contra : ∀ (ba : ¬a ≤ b), False
⊢ a ≤ b

Tactic:
by_contra ba
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False

Tactic:
lt_irrefl _ (h (not_le.mp ba))

Premises used: not_le, lt_irrefl, Iff.mp
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False

Tactic:
exact lt_irrefl _ (h (not_le.mp ba))

Premises used: not_le, lt_irrefl, Iff.mp
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi b ⊂ Ioi a ↔ a < b

Tactic:
⟨fun h => ?_, Ioi_ssubset_Ioi⟩

Premises used: Set.Ioi_ssubset_Ioi, Iff.intro
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
refine : ∀ (h : Ioi b ⊂ Ioi a), a < b
⊢ Ioi b ⊂ Ioi a ↔ a < b

Tactic:
refine ⟨fun h => ?_, Ioi_ssubset_Ioi⟩
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊂ Ioi a
obtain : Ioi b ⊆ Ioi a → ∀ (c : α) (ac : c ∈ Ioi a) (cb : ¬c ∈ Ioi b), a < b
⊢ a < b

Tactic:
obtain ⟨_, c, ac, cb⟩ := ssubset_iff_exists.mp h

Premises used: Set.ssubset_iff_exists, Iff.mp
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊂ Ioi a
left : Ioi b ⊆ Ioi a
c : α
ac : c ∈ Ioi a
cb : ¬c ∈ Ioi b
⊢ a < b

Tactic:
ac.trans_le (le_of_not_gt cb)

Premises used: le_of_not_gt, LT.lt.trans_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊂ Ioi a
left : Ioi b ⊆ Ioi a
c : α
ac : c ∈ Ioi a
cb : ¬c ∈ Ioi b
⊢ a < b

Tactic:
exact ac.trans_le (le_of_not_gt cb)

Premises used: le_of_not_gt, LT.lt.trans_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
⊢ Ioi b ⊆ Ici a ↔ a ≤ b

Tactic:
⟨fun h => ?_, Ioi_subset_Ici⟩

Premises used: Iff.intro, Set.Ioi_subset_Ici
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
refine : ∀ (h : Ioi b ⊆ Ici a), a ≤ b
⊢ Ioi b ⊆ Ici a ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, Ioi_subset_Ici⟩
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
by_contra : ∀ (ba : ¬a ≤ b), False
⊢ a ≤ b

Tactic:
by_contra ba
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ ∃ (c : α), b < c ∧ c < a

Tactic:
exists_between (not_le.mp ba)

Premises used: not_le, exists_between, Iff.mp
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
obtain : ∀ (c : α) (bc : b < c) (ca : c < a), False
⊢ False

Tactic:
obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)

Premises used: not_le, exists_between, Iff.mp
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False

Tactic:
lt_irrefl _ (ca.trans_le (h bc))

Premises used: lt_irrefl, LT.lt.trans_le