awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : MonotoneOn f (Ici a)
⊢ f '' Ici a ⊆ Ici (f a)

Tactic:
h.mapsTo_Ici.image_subset

Premises used: MonotoneOn.mapsTo_Ici, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : MonotoneOn f (Iic b)
⊢ f '' Iic b ⊆ Iic (f b)

Tactic:
h.mapsTo_Iic.image_subset

Premises used: Set.MapsTo.image_subset, MonotoneOn.mapsTo_Iic
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : MonotoneOn f (Icc a b)
⊢ f '' Icc a b ⊆ Icc (f a) (f b)

Tactic:
h.mapsTo_Icc.image_subset

Premises used: MonotoneOn.mapsTo_Icc, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : AntitoneOn f (Ici a)
⊢ f '' Ici a ⊆ Iic (f a)

Tactic:
h.mapsTo_Ici.image_subset

Premises used: AntitoneOn.mapsTo_Ici, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : AntitoneOn f (Iic b)
⊢ f '' Iic b ⊆ Ici (f b)

Tactic:
h.mapsTo_Iic.image_subset

Premises used: AntitoneOn.mapsTo_Iic, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : AntitoneOn f (Icc a b)
⊢ f '' Icc a b ⊆ Icc (f b) (f a)

Tactic:
h.mapsTo_Icc.image_subset

Premises used: AntitoneOn.mapsTo_Icc, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictMonoOn f (Ici a)
⊢ f '' Ioi a ⊆ Ioi (f a)

Tactic:
h.mapsTo_Ioi.image_subset

Premises used: StrictMonoOn.mapsTo_Ioi, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictMonoOn f (Iic b)
⊢ f '' Iio b ⊆ Iio (f b)

Tactic:
h.mapsTo_Iio.image_subset

Premises used: StrictMonoOn.mapsTo_Iio, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictMonoOn f (Icc a b)
⊢ f '' Ioo a b ⊆ Ioo (f a) (f b)

Tactic:
h.mapsTo_Ioo.image_subset

Premises used: StrictMonoOn.mapsTo_Ioo, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictAntiOn f (Ici a)
⊢ f '' Ioi a ⊆ Iio (f a)

Tactic:
h.mapsTo_Ioi.image_subset

Premises used: StrictAntiOn.mapsTo_Ioi, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictAntiOn f (Iic b)
⊢ f '' Iio b ⊆ Ioi (f b)

Tactic:
h.mapsTo_Iio.image_subset

Premises used: StrictAntiOn.mapsTo_Iio, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictAntiOn f (Icc a b)
⊢ f '' Ioo a b ⊆ Ioo (f b) (f a)

Tactic:
h.mapsTo_Ioo.image_subset

Premises used: StrictAntiOn.mapsTo_Ioo, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : Monotone f
⊢ f '' Ici a ⊆ Ici (f a)

Tactic:
(h.monotoneOn _).image_Ici_subset

Premises used: Monotone.monotoneOn, MonotoneOn.image_Ici_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : Monotone f
⊢ f '' Iic b ⊆ Iic (f b)

Tactic:
(h.monotoneOn _).image_Iic_subset

Premises used: MonotoneOn.image_Iic_subset, Monotone.monotoneOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : Monotone f
⊢ f '' Icc a b ⊆ Icc (f a) (f b)

Tactic:
(h.monotoneOn _).image_Icc_subset

Premises used: MonotoneOn.image_Icc_subset, Monotone.monotoneOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : Antitone f
⊢ f '' Ici a ⊆ Iic (f a)

Tactic:
(h.antitoneOn _).image_Ici_subset

Premises used: Antitone.antitoneOn, AntitoneOn.image_Ici_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : Antitone f
⊢ f '' Iic b ⊆ Ici (f b)

Tactic:
(h.antitoneOn _).image_Iic_subset

Premises used: AntitoneOn.image_Iic_subset, Antitone.antitoneOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : Antitone f
⊢ f '' Icc a b ⊆ Icc (f b) (f a)

Tactic:
(h.antitoneOn _).image_Icc_subset

Premises used: Antitone.antitoneOn, AntitoneOn.image_Icc_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictMono f
⊢ f '' Ioi a ⊆ Ioi (f a)

Tactic:
(h.strictMonoOn _).image_Ioi_subset

Premises used: StrictMonoOn.image_Ioi_subset, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictMono f
⊢ f '' Iio b ⊆ Iio (f b)

Tactic:
(h.strictMonoOn _).image_Iio_subset

Premises used: StrictMonoOn.image_Iio_subset, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictMono f
⊢ f '' Ioo a b ⊆ Ioo (f a) (f b)

Tactic:
(h.strictMonoOn _).image_Ioo_subset

Premises used: StrictMonoOn.image_Ioo_subset, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a : α
h : StrictAnti f
⊢ f '' Ioi a ⊆ Iio (f a)

Tactic:
(h.strictAntiOn _).image_Ioi_subset

Premises used: StrictAntiOn.image_Ioi_subset, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
b : α
h : StrictAnti f
⊢ f '' Iio b ⊆ Ioi (f b)

Tactic:
(h.strictAntiOn _).image_Iio_subset

Premises used: StrictAntiOn.image_Iio_subset, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
a b : α
h : StrictAnti f
⊢ f '' Ioo a b ⊆ Ioo (f b) (f a)

Tactic:
(h.strictAntiOn _).image_Ioo_subset

Premises used: StrictAntiOn.image_Ioo_subset, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMonoOn f (Icc a b)
⊢ MapsTo f (Ico a b) (Ico (f a) (f b))

Tactic:
fun _c hc ↦ ⟨h.monotoneOn (left_mem_Icc.2 <| hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1,
    h (Ico_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.trans hc.2.le) hc.2⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Ico_subset_Icc_self, Set.Mem, setOf, LT.lt.le, Set.Ico, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, StrictMonoOn.monotoneOn, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMonoOn f (Icc a b)
⊢ MapsTo f (Ioc a b) (Ioc (f a) (f b))

Tactic:
fun _c hc ↦ ⟨h (left_mem_Icc.2 <| hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1,
    h.monotoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.le.trans hc.2) hc.2⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Ioc, Set.Mem, setOf, Set.Ioc_subset_Icc_self, LT.lt.le, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, StrictMonoOn.monotoneOn, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAntiOn f (Icc a b)
⊢ MapsTo f (Ico a b) (Ioc (f b) (f a))

Tactic:
fun _c hc ↦ ⟨h (Ico_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.trans hc.2.le) hc.2,
    h.antitoneOn (left_mem_Icc.2 <| hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Ioc, Set.Ico_subset_Icc_self, Set.Mem, setOf, LT.lt.le, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, StrictAntiOn.antitoneOn, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAntiOn f (Icc a b)
⊢ MapsTo f (Ioc a b) (Ico (f b) (f a))

Tactic:
fun _c hc ↦ ⟨h.antitoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.le.trans hc.2) hc.2,
    h (left_mem_Icc.2 <| hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, Set.Ioc_subset_Icc_self, LT.lt.le, Set.Ico, And.right, And.left, Set.left_mem_Icc, Set.MapsTo, And.intro, StrictAntiOn.antitoneOn, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMono f
⊢ MapsTo f (Ico a b) (Ico (f a) (f b))

Tactic:
(h.strictMonoOn _).mapsTo_Ico

Premises used: StrictMonoOn.mapsTo_Ico, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMono f
⊢ MapsTo f (Ioc a b) (Ioc (f a) (f b))

Tactic:
(h.strictMonoOn _).mapsTo_Ioc

Premises used: StrictMonoOn.mapsTo_Ioc, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAnti f
⊢ MapsTo f (Ico a b) (Ioc (f b) (f a))

Tactic:
(h.strictAntiOn _).mapsTo_Ico

Premises used: StrictAnti.strictAntiOn, StrictAntiOn.mapsTo_Ico
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAnti f
⊢ MapsTo f (Ioc a b) (Ico (f b) (f a))

Tactic:
(h.strictAntiOn _).mapsTo_Ioc

Premises used: StrictAnti.strictAntiOn, StrictAntiOn.mapsTo_Ioc
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMonoOn f (Icc a b)
⊢ f '' Ico a b ⊆ Ico (f a) (f b)

Tactic:
h.mapsTo_Ico.image_subset

Premises used: StrictMonoOn.mapsTo_Ico, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMonoOn f (Icc a b)
⊢ f '' Ioc a b ⊆ Ioc (f a) (f b)

Tactic:
h.mapsTo_Ioc.image_subset

Premises used: StrictMonoOn.mapsTo_Ioc, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAntiOn f (Icc a b)
⊢ f '' Ico a b ⊆ Ioc (f b) (f a)

Tactic:
h.mapsTo_Ico.image_subset

Premises used: StrictAntiOn.mapsTo_Ico, Set.MapsTo.image_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAntiOn f (Icc a b)
⊢ f '' Ioc a b ⊆ Ico (f b) (f a)

Tactic:
h.mapsTo_Ioc.image_subset

Premises used: Set.MapsTo.image_subset, StrictAntiOn.mapsTo_Ioc
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMono f
⊢ f '' Ico a b ⊆ Ico (f a) (f b)

Tactic:
(h.strictMonoOn _).image_Ico_subset

Premises used: StrictMono.strictMonoOn, StrictMonoOn.image_Ico_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictMono f
⊢ f '' Ioc a b ⊆ Ioc (f a) (f b)

Tactic:
(h.strictMonoOn _).image_Ioc_subset

Premises used: StrictMonoOn.image_Ioc_subset, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAnti f
⊢ f '' Ico a b ⊆ Ioc (f b) (f a)

Tactic:
(h.strictAntiOn _).image_Ico_subset

Premises used: StrictAnti.strictAntiOn, StrictAntiOn.image_Ico_subset
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : PartialOrder α
inst_1 : Preorder β
a b : α
h : StrictAnti f
⊢ f '' Ioc a b ⊆ Ico (f b) (f a)

Tactic:
(h.strictAntiOn _).image_Ioc_subset

Premises used: StrictAntiOn.image_Ioc_subset, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x : α // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c : α) x → p a x
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r (↑c : α) y}) x ↔
      Membership.mem (γ := Set α) {y : α | r (↑c : α) y ∧ q y b} x
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r (↑c : α) y}) {y : α | r (↑c : α) y ∧ q y b}

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x : α // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c : α) x → p a x
x : α
⊢ Membership.mem (γ := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r (↑c : α) y}) x ↔
    Membership.mem (γ := Set α) {y : α | r (↑c : α) y ∧ q y b} x

Tactic:
simp +contextual [@and_comm (r _ _), h]

Premises used: and_comm
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x : α // p a x ∧ q x b }
h : ∀ {x : α}, r x (↑c : α) → q x b
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r y (↑c : α)}) x ↔
      Membership.mem (γ := Set α) {y : α | p a y ∧ r y (↑c : α)} x
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r y (↑c : α)}) {y : α | p a y ∧ r y (↑c : α)}

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x : α // p a x ∧ q x b }
h : ∀ {x : α}, r x (↑c : α) → q x b
x : α
⊢ Membership.mem (γ := Set α) ({x : α | p a x ∧ q x b} ∩ {y : α | r y (↑c : α)}) x ↔
    Membership.mem (γ := Set α) {y : α | p a y ∧ r y (↑c : α)} x

Tactic:
simp +contextual [h]
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Ici (↑a : α) = Ici a

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Iic (↑a : α) = Iic a

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iic, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Ioi (↑a : α) = Ioi a

Tactic:
rfl

Premises used: Set.Ioi, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Iio (↑a : α) = Iio a

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Icc (↑a : α) (↑b : α) = Icc a b

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Icc, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Ico (↑a : α) (↑b : α) = Ico a b

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Ico, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Ioc (↑a : α) (↑b : α) = Ioc a b

Tactic:
rfl

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) ⁻¹' Ioo (↑a : α) (↑b : α) = Ioo a b

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Ioo, rfl
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Icc a b ⊆ Icc (↑a : α) (↑b : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Ico a b ⊆ Ico (↑a : α) (↑b : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Ioc a b ⊆ Ioc (↑a : α) (↑b : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a b : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Ioo a b ⊆ Ioo (↑a : α) (↑b : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Iic a ⊆ Iic (↑a : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Iio a ⊆ Iio (↑a : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Ici a ⊆ Ici (↑a : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
a : { x : α // p x }
⊢ Subtype.val (p := fun (x : α) ↦ p x) '' Ioi a ⊆ Ioi (↑a : α)

Tactic:
image_subset_iff.mpr fun _ m => m

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ici a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) '' Iic b = Icc a (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ici a) (Iic b.1)).trans Ici_inter_Iic

Premises used: Set.Ici, Set.Mem, setOf, Set.preimage, Subtype.image_preimage_val, Set.Iic, Subtype.val, Eq.trans, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ici a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) '' Iio b = Ico a (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ici a) (Iio b.1)).trans Ici_inter_Iio

Premises used: Set.Ici, Set.Ici_inter_Iio, Set.Mem, setOf, Set.preimage, Subtype.image_preimage_val, Subtype.val, Set.Iio, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ici a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) '' Ici b = Ici (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ici a) (Ici b.1)).trans <| inter_eq_right.2 <| Ici_subset_Ici.2 b.2

Premises used: Iff.mpr, Set.Ici, Set.Mem, setOf, Set.inter_eq_right, Set.Ici_subset_Ici, Set.preimage, Subtype.image_preimage_val, Subtype.val, Eq.trans, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ici a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) '' Ioi b = Ioi (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ici a) (Ioi b.1)).trans <| inter_eq_right.2 <| Ioi_subset_Ici b.2

Premises used: Iff.mpr, Set.Ioi, Set.Ici, Set.Mem, setOf, Set.inter_eq_right, Set.preimage, Subtype.image_preimage_val, Subtype.val, Set.Ioi_subset_Ici, Eq.trans, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iic a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' Ici b = Icc (↑b : α) a

Tactic:
(Subtype.image_preimage_val (Iic a) (Ici b)).trans <| inter_comm _ _

Premises used: Set.Ici, Set.Mem, setOf, Set.inter_comm, Set.preimage, Subtype.image_preimage_val, Set.Iic, Subtype.val, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iic a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' Ioi b = Ioc (↑b : α) a

Tactic:
(Subtype.image_preimage_val (Iic a) (Ioi b)).trans <| inter_comm _ _

Premises used: Set.Ioi, Set.Mem, setOf, Set.inter_comm, Set.preimage, Subtype.image_preimage_val, Set.Iic, Subtype.val, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iic a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' Iic b = Iic (↑b : α)

Tactic:
image_subtype_val_Ici_Ici (α := αᵒᵈ) _

Premises used: Set.image_subtype_val_Ici_Ici, Set.Mem, setOf, Set.Iic, OrderDual
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iic a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' Iio b = Iio (↑b : α)

Tactic:
image_subtype_val_Ici_Ioi (α := αᵒᵈ) _

Premises used: Set.Mem, setOf, Set.Iic, OrderDual, Set.Iio, Set.image_subtype_val_Ici_Ioi
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ioi a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) '' Ici b = Ici (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ioi a) (Ici b.1)).trans <| inter_eq_right.2 <| Ici_subset_Ioi.2 b.2

Premises used: Iff.mpr, Set.Ioi, Set.Ici, Set.Mem, setOf, Set.inter_eq_right, Set.preimage, Subtype.image_preimage_val, Subtype.val, Set.Ici_subset_Ioi, Eq.trans, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ioi a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) '' Iic b = Ioc a (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ioi a) (Iic b.1)).trans Ioi_inter_Iic

Premises used: Set.Ioi_inter_Iic, Set.Ioi, Set.Mem, setOf, Set.preimage, Subtype.image_preimage_val, Set.Iic, Subtype.val, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ioi a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) '' Ioi b = Ioi (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ioi a) (Ioi b.1)).trans <| inter_eq_right.2 <| Ioi_subset_Ioi b.2.le

Premises used: Iff.mpr, Set.Ioi, Set.Mem, setOf, LT.lt.le, Set.inter_eq_right, Set.preimage, Subtype.image_preimage_val, Set.Ioi_subset_Ioi, Subtype.val, Eq.trans, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Ioi a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) '' Iio b = Ioo a (↑b : α)

Tactic:
(Subtype.image_preimage_val (Ioi a) (Iio b.1)).trans Ioi_inter_Iio

Premises used: Set.Ioi, Set.Mem, setOf, Set.Ioi_inter_Iio, Set.preimage, Subtype.image_preimage_val, Subtype.val, Set.Iio, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iio a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iio a) '' Ici b = Ico (↑b : α) a

Tactic:
(Subtype.image_preimage_val (Iio a) (Ici b)).trans <| inter_comm _ _

Premises used: Set.Ici, Set.Mem, setOf, Set.inter_comm, Set.preimage, Subtype.image_preimage_val, Subtype.val, Set.Iio, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iio a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iio a) '' Iic b = Iic (↑b : α)

Tactic:
image_subtype_val_Ioi_Ici (α := αᵒᵈ) _

Premises used: Set.Mem, setOf, Set.image_subtype_val_Ioi_Ici, Set.Iic, OrderDual, Set.Iio