awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ k < succ k

Tactic:
exact lt_succ_of_not_isMax hk

Premises used: Order.lt_succ_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
h : m ≤ k
⊢ m ≤ φ m

Tactic:
ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) _ h

Premises used: StrictMonoOn.mono, Order.le_succ, le_trans
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
h : m ≤ k
⊢ m ≤ φ m

Tactic:
exact ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) _ h

Premises used: StrictMonoOn.mono, Order.le_succ, le_trans
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderTop α
n : α
φ : α → α
hφ : StrictMonoOn φ (Ici n)
⊢ ∀ (m : α), n ≤ m → φ m ≤ m

Tactic:
StrictMonoOn.Iic_id_le (α := αᵒᵈ) fun _ hi _ hj hij => hφ hj hi hij

Premises used: StrictMonoOn.Iic_id_le, OrderDual
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
a b : ℕ
⊢ (Icc a b).ncard = b + 1 - a

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Icc a b

Premises used: Nat.card_Icc, Set.ncard_coe_finset
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
a b : ℕ
⊢ (Ico a b).ncard = b - a

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Ico a b

Premises used: Nat.card_Ico, Set.ncard_coe_finset
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
a b : ℕ
⊢ (Ioc a b).ncard = b - a

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Ioc a b

Premises used: Nat.card_Ioc, Set.ncard_coe_finset
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
a b : ℕ
⊢ (Ioo a b).ncard = b - a - 1

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Ioo a b

Premises used: Nat.card_Ioo, Set.ncard_coe_finset
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
a b : ℕ
⊢ (uIcc a b).ncard = (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_uIcc a b

Premises used: Set.ncard_coe_finset, Nat.card_uIcc
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
b : ℕ
⊢ (Iic b).ncard = b + 1

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Iic b

Premises used: Nat.card_Iic, Set.ncard_coe_finset
-- Module: Mathlib.Order.Interval.Set.Nat
Goal:
b : ℕ
⊢ (Iio b).ncard = b

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Iio b

Premises used: Nat.card_Iio, Set.ncard_coe_finset
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : s.OrdConnected
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Icc x y ⊆ s

Tactic:
h.1

Premises used: Set.OrdConnected.out'
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Icc x y ⊆ s

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Set.OrdConnected.mk, Set.OrdConnected.out', Iff.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s.OrdConnected ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
ordConnected_def.trans
    ⟨fun hs _ hx _ hy _ => hs hx hy, fun H x hx y hy _ hz => H x hx y hy (le_trans hz.1 hz.2) hz⟩

Premises used: Set.ordConnected_def, And.right, And.left, Iff.intro, Iff.trans, le_trans
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
rw : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s
⊢ s.OrdConnected

Tactic:
rw [ordConnected_iff]

Premises used: Set.ordConnected_iff
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
inl : ∀ (hy : x ∈ s) (hxy : x ≤ x), Icc x x ⊆ s
inr : ∀ (hxy' : x < y), Icc x y ⊆ s
⊢ Icc x y ⊆ s

Tactic:
rcases eq_or_lt_of_le hxy with (rfl | hxy')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

Tactic:
simpa
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
inr : insert x (insert y (Ioo x y)) ⊆ s
⊢ Icc x y ⊆ s

Tactic:
rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']

Premises used: Set.Ioc_insert_left, Set.Ioo_insert_right
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s

Tactic:
insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

Premises used: Iff.mpr, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s

Tactic:
exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

Premises used: Iff.mpr, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : β → α
hs : s.OrdConnected
hf : Monotone f
⊢ (f ⁻¹' s).OrdConnected

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

Premises used: Set.OrdConnected.out, Set.OrdConnected.mk, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : β → α
hs : s.OrdConnected
hf : Antitone f
⊢ (f ⁻¹' s).OrdConnected

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

Premises used: Set.OrdConnected.out, Set.OrdConnected.mk, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : s.OrdConnected
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ Icc x y ⊆ s

Tactic:
hs.out hx hy

Premises used: Set.OrdConnected.out
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Icc x y : Set β)
    (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)

Tactic:
rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]

Premises used: Set.inter_eq_left, Iff.mpr, OrderEmbedding.preimage_Icc, Set.OrdConnected.out, Set.image_preimage_eq_inter_range, Exists.intro, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ico x y : Set β)
    (Ico ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)

Tactic:
rw [← e.preimage_Ico, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Premises used: Set.inter_eq_left, Iff.mpr, Set.Ico_subset_Icc_self, HasSubset.Subset.trans, Set.OrdConnected.out, Set.image_preimage_eq_inter_range, OrderEmbedding.preimage_Ico, Exists.intro, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioc x y : Set β)
    (Ioc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)

Tactic:
rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Premises used: Set.inter_eq_left, Iff.mpr, OrderEmbedding.preimage_Ioc, Set.Ioc_subset_Icc_self, HasSubset.Subset.trans, Set.OrdConnected.out, Set.image_preimage_eq_inter_range, Exists.intro, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
x y : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β)
          (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)) :
      Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Set β) (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioo x y : Set β)
    (Ioo ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)

Tactic:
rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Premises used: Set.inter_eq_left, Iff.mpr, Set.Ioo_subset_Icc_self, HasSubset.Subset.trans, Set.OrdConnected.out, Set.image_preimage_eq_inter_range, Exists.intro, OrderEmbedding.preimage_Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : s.OrdConnected
x y : (↑s : Type u_1)
⊢ OrdConnected.{u_1} (α := α)
    (range (ι := { x : α // x ∈ s }) (⇑(OrderEmbedding.subtype fun (x : α) ↦ x ∈ s) : (a : { x : α // x ∈ s }) → α))

Tactic:
simpa
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : s.OrdConnected
ht : t.OrdConnected
⊢ (s ∩ t).OrdConnected

Tactic:
⟨fun _ hx _ hy => subset_inter (hs.out hx.1 hy.1) (ht.out hx.2 hy.2)⟩

Premises used: Set.OrdConnected.out, Set.subset_inter, Set.OrdConnected.mk, And.right, And.left
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
inst_2 : s.OrdConnected
inst_3 : t.OrdConnected
⊢ (s ∩ t).OrdConnected

Tactic:
OrdConnected.inter ‹_› ‹_›

Premises used: Set.OrdConnected.inter
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : s.OrdConnected
⊢ OrdConnected (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)

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

Premises used: Set.OrdConnected.out, Set.OrdConnected.mk, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : s.OrdConnected
⊢ OrdConnected (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)

Tactic:
.dual ‹OrdConnected s›

Premises used: Set.OrdConnected.dual
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : OrdConnected (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
⊢ s.OrdConnected

Tactic:
simpa only [ordConnected_def] using h.dual

Premises used: Set.ordConnected_def, Set.OrdConnected.dual
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
S : Set (Set α)
hS : ∀ s ∈ S, s.OrdConnected
⊢ (⋂₀ S).OrdConnected

Tactic:
⟨fun _x hx _y hy _z hz s hs => (hS s hs).out (hx s hs) (hy s hs) hz⟩

Premises used: Set.OrdConnected.out, Set.OrdConnected.mk
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_3
s : ι → Set α
hs : ∀ (i : ι), (s i).OrdConnected
⊢ OrdConnected.{u_1} (α := α) (⋂ (i : ι), s i)

Tactic:
ordConnected_sInter <| forall_mem_range.2 hs

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, Set.ordConnected_sInter
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
ι : Sort u_3
s : ι → Set α
inst_2 : ∀ (i : ι), (s i).OrdConnected
⊢ OrdConnected.{u_1} (α := α) (⋂ (i : ι), s i)

Tactic:
ordConnected_iInter ‹_›

Premises used: Set.ordConnected_iInter
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_3
p : ι → Prop
s : (i : ι) → p i → Set α
hs : ∀ (i : ι) (hi : p i), (s i hi).OrdConnected
⊢ OrdConnected.{u_1} (α := α) (⋂ (i : ι), ⋂ (hi : p i), s i hi)

Tactic:
ordConnected_iInter fun i => ordConnected_iInter <| hs i

Premises used: Set.ordConnected_iInter
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
s : Set ι
t : (i : ι) → Set (α i)
h : ∀ i ∈ s, (t i).OrdConnected
⊢ (s.pi (α := α) t).OrdConnected

Tactic:
⟨fun _ hx _ hy _ hz i hi => (h i hi).out (hx i hi) (hy i hi) ⟨hz.1 i, hz.2 i⟩⟩

Premises used: Set.OrdConnected.out, Set.OrdConnected.mk, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α_1 : Type u_1
β : Type u_2
inst : Preorder α_1
inst_1 : Preorder β
ι : Type u_3
α : ι → Type u_4
inst_2 : (i : ι) → Preorder (α i)
s : Set ι
t : (i : ι) → Set (α i)
h : ∀ (i : ι), (t i).OrdConnected
⊢ (s.pi (α := α) t).OrdConnected

Tactic:
ordConnected_pi fun i _ => h i

Premises used: Set.ordConnected_pi
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
⊢ (Ici a).OrdConnected

Tactic:
⟨fun _ hx _ _ _ hz => le_trans hx hz.1⟩

Premises used: Set.OrdConnected.mk, And.left, le_trans
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
⊢ (Ioi a).OrdConnected

Tactic:
⟨fun _ hx _ _ _ hz => lt_of_lt_of_le hx hz.1⟩

Premises used: Set.OrdConnected.mk, And.left, lt_of_lt_of_le
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
⊢ (Icc a b).OrdConnected

Tactic:
ordConnected_Ici.inter ordConnected_Iic

Premises used: Set.Ici, Set.ordConnected_Iic, Set.Mem, Set.ordConnected_Ici, setOf, Set.inter, Set.Icc, Set.OrdConnected.inter
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
⊢ (Ico a b).OrdConnected

Tactic:
ordConnected_Ici.inter ordConnected_Iio

Premises used: Set.Ici, Set.Mem, Set.ordConnected_Ici, setOf, Set.inter, Set.Ico, Set.OrdConnected.inter, Set.ordConnected_Iio
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
⊢ (Ioo a b).OrdConnected

Tactic:
ordConnected_Ioi.inter ordConnected_Iio

Premises used: Set.Ioi, Set.ordConnected_Ioi, Set.Mem, setOf, Set.inter, Set.OrdConnected.inter, Set.ordConnected_Iio, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
a : α
rw : (Icc a a).OrdConnected
⊢ OrdConnected (α := α) {a}

Tactic:
rw [← Icc_self]

Premises used: Set.Icc_self
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected

Tactic:
ordConnected_Icc

Premises used: Set.ordConnected_Icc
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_3
inst : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected

Tactic:
exact ordConnected_Icc

Premises used: Set.ordConnected_Icc
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
⊢ OrdConnected.{u_1} (α := α) ∅

Tactic:
⟨fun _ => False.elim⟩

Premises used: False.elim, Set.OrdConnected.mk
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
inst : Preorder α
⊢ OrdConnected.{u_1} (α := α) univ

Tactic:
⟨fun _ _ _ _ => subset_univ _⟩

Premises used: Set.subset_univ, Set.Icc, Set.OrdConnected.mk
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
s : Set α
hs : s.OrdConnected
⊢ DenselyOrdered.{u_1} (↑s : Type u_1)

Tactic:
⟨fun a b (h : (a : α) < b) =>
    let ⟨x, H⟩ := exists_between h
    ⟨⟨x, (hs.out a.2 b.2) (Ioo_subset_Icc_self H)⟩, H⟩⟩

Premises used: Set.Ioo_subset_Icc_self, Exists, Set.OrdConnected.out, exists_between, DenselyOrdered.mk, Subtype.mk, And, LT.lt, Exists.intro, _private.0.Set.instDenselyOrdered.match_1, Subtype.property
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
F : Type u_3
inst_2 : FunLike F α β
inst_3 : OrderHomClass F α β
f : F
s : Set β
hs : s.OrdConnected
⊢ OrdConnected.{u_1} (α := α) ((⇑f : (a : α) → β) ⁻¹' s)

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

Premises used: Set.OrdConnected.out, OrderHomClass.mono, Set.OrdConnected.mk, And.right, And.left, And.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
erw : OrdConnected.{u_2} (α := β) ((⇑(OrderIso.symm (↑e : α ≃o β)) : (a : β) → α) ⁻¹' s)
⊢ OrdConnected.{u_2} (α := β) ((⇑e : (a : α) → β) '' s)

Tactic:
erw [(e : α ≃o β).image_eq_preimage_symm]

Premises used: OrderIsoClass.toOrderIso, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ OrdConnected.{u_2} (α := β) ((⇑(OrderIso.symm (↑e : α ≃o β)) : (a : β) → α) ⁻¹' s)

Tactic:
apply ordConnected_preimage (e : α ≃o β).symm

Premises used: Set.ordConnected_preimage, OrderIso.symm, OrderIsoClass.toOrderIso
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
simp_rw : OrdConnected.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ)
⊢ OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))

Tactic:
simp_rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
⊢ OrdConnected.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ)

Tactic:
ordConnected_image (e : α ≃o β)

Premises used: Set.ordConnected_image, OrderIsoClass.toOrderIso
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
⊢ OrdConnected.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ)

Tactic:
exact ordConnected_image (e : α ≃o β)

Premises used: Set.ordConnected_image, OrderIsoClass.toOrderIso
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
⊢ ∃ (u : Set β), u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u

Tactic:
⟨u, ⟨?_⟩, Subset.antisymm ?_ ?_⟩

Premises used: Set.Subset.antisymm, Set.OrdConnected.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
refine_1 : ∀ ⦃x : β⦄ (hx : x ∈ u) ⦃y : β⦄ (hy : y ∈ u), Icc x y ⊆ u
refine_2 : t ∩ f ⁻¹' s ⊆ t ∩ u
refine_3 : t ∩ u ⊆ t ∩ f ⁻¹' s
⊢ ∃ (u : Set β), u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u

Tactic:
refine ⟨u, ⟨?_⟩, Subset.antisymm ?_ ?_⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
x' z : β
zt : z ∈ t
x'z : x' ≤ z
zs : f z ∈ s
a : β
ha : a ∈ Icc x x'
⊢ a ∈ u

Tactic:
⟨⟨y, yt, yx.trans ha.1, ys⟩, ⟨z, zt, ha.2.trans x'z, zs⟩⟩

Premises used: Set.Mem, setOf, And.right, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
x' z : β
zt : z ∈ t
x'z : x' ≤ z
zs : f z ∈ s
a : β
ha : a ∈ Icc x x'
⊢ a ∈ u

Tactic:
exact ⟨⟨y, yt, yx.trans ha.1, ys⟩, ⟨z, zt, ha.2.trans x'z, zs⟩⟩
-- Module: Mathlib.Order.Interval.Set.OrdConnected
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x : β | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
xs : x ∈ f ⁻¹' s
⊢ x ∈ t ∩ u

Tactic:
⟨xt, ⟨x, xt, le_rfl, xs⟩, ⟨x, xt, le_rfl, xs⟩⟩

Premises used: le_rfl, Set.Mem, setOf, Set.inter, And.intro, Exists.intro