awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
hb : b < (f : (a : α) → β) a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b

Tactic:
f.mem_range_of_rel hb

Premises used: InitialSeg.mem_range_of_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) a : β)

Tactic:
exacts [⟨a, rfl⟩, f.mem_range_of_rel hb]
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
b : β
a : α
h : b ≤ (f : (a : α) → β) a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b

Tactic:
mem_range_of_le f h

Premises used: InitialSeg.mem_range_of_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
b : β
a : α
h : b ≤ (f : (a : α) → β) a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b

Tactic:
exact mem_range_of_le f h

Premises used: InitialSeg.mem_range_of_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a a' : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a' : β) ↔ a ≤ a'

Tactic:
f.toOrderEmbedding.le_iff_le

Premises used: InitialSeg.toOrderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a a' : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a' : β) ↔ a < a'

Tactic:
f.toOrderEmbedding.lt_iff_lt

Premises used: InitialSeg.toOrderEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.toOrderEmbedding.monotone

Premises used: OrderEmbedding.monotone, InitialSeg.toOrderEmbedding
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ StrictMono.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.toOrderEmbedding.strictMono

Premises used: OrderEmbedding.strictMono, InitialSeg.toOrderEmbedding
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ IsMin.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsMin a

Tactic:
⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩

Premises used: StrictMono.isMin_of_apply, InitialSeg.strictMono, Iff.intro
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
refine : ∀ (h : IsMin a) (b : β) (hb : b ≤ (f : (a : α) → β) a), (f : (a : α) → β) a ≤ b
⊢ IsMin.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsMin a

Tactic:
refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsMin a
b : β
hb : b ≤ (f : (a : α) → β) a
obtain :
  ∀ (x : α) (hb : LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β)),
    LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β)
⊢ (f : (a : α) → β) a ≤ b

Tactic:
obtain ⟨x, rfl⟩ := f.mem_range_of_le hb

Premises used: InitialSeg.mem_range_of_le, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsMin a
x : α
hb : LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β)
rw : ∀ (hb : x ≤ a), a ≤ x
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) x : β)

Tactic:
rw [f.le_iff_le] at hb ⊢

Premises used: InitialSeg.le_iff_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x

Tactic:
h hb
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x

Tactic:
exact h hb
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : OrderBot β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
(map_isMin f isMin_bot).eq_bot

Premises used: InitialSeg.map_isMin, IsMin.eq_bot, isMin_bot
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
a : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' Set.Iio a : Set β) (Set.Iio ((f : (a : α) → β) a) : Set β)

Tactic:
f.toOrderEmbedding.image_Iio f.isLowerSet_range a

Premises used: OrderEmbedding.image_Iio, InitialSeg.toOrderEmbedding, InitialSeg.isLowerSet_range
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
mp : b ≤ (f : (a : α) → β) a → ∃ c ≤ a, (f : (a : α) → β) c = b
mpr : (∃ c ≤ a, (f : (a : α) → β) c = b) → b ≤ (f : (a : α) → β) a
⊢ b ≤ (f : (a : α) → β) a ↔ ∃ c ≤ a, (f : (a : α) → β) c = b

Tactic:
constructor
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
mp : ∀ (c : α) (hc : (f : (a : α) → β) c = b), ∃ c ≤ a, (f : (a : α) → β) c = b
⊢ ∃ c ≤ a, (f : (a : α) → β) c = b

Tactic:
obtain ⟨c, hc⟩ := f.mem_range_of_le h

Premises used: InitialSeg.mem_range_of_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
⊢ ∃ c ≤ a, (f : (a : α) → β) c = b

Tactic:
⟨c, ?_, hc⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
mp : c ≤ a
⊢ ∃ c ≤ a, (f : (a : α) → β) c = b

Tactic:
refine ⟨c, ?_, hc⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
mp :
  ∀ (h : LE.le.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)) (hc : (f : (a : α) → β) c = b), c ≤ a
mp₁ mp₂ mp₃ mp₄ : ∀ (h : c ≤ a) (hc : (f : (a : α) → β) c = b), c ≤ a
⊢ c ≤ a

Tactic:
rwa [← hc, f.le_iff_le] at h

Premises used: InitialSeg.le_iff_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
c : α
hc : c ≤ a
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)

Tactic:
f.monotone hc

Premises used: InitialSeg.monotone
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
c : α
hc : c ≤ a
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)

Tactic:
exact f.monotone hc

Premises used: InitialSeg.monotone
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
mp : b < (f : (a : α) → β) a → ∃ a' < a, (f : (a : α) → β) a' = b
mpr : (∃ a' < a, (f : (a : α) → β) a' = b) → b < (f : (a : α) → β) a
⊢ b < (f : (a : α) → β) a ↔ ∃ a' < a, (f : (a : α) → β) a' = b

Tactic:
constructor
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
mp : ∀ (c : α) (hc : (f : (a : α) → β) c = b), ∃ a' < a, (f : (a : α) → β) a' = b
⊢ ∃ a' < a, (f : (a : α) → β) a' = b

Tactic:
obtain ⟨c, hc⟩ := f.mem_range_of_rel h

Premises used: InitialSeg.mem_range_of_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
⊢ ∃ a' < a, (f : (a : α) → β) a' = b

Tactic:
⟨c, ?_, hc⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
mp : c < a
⊢ ∃ a' < a, (f : (a : α) → β) a' = b

Tactic:
refine ⟨c, ?_, hc⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : b < (f : (a : α) → β) a
c : α
hc : (f : (a : α) → β) c = b
mp :
  ∀ (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)) (hc : (f : (a : α) → β) c = b), c < a
mp₁ mp₂ mp₃ mp₄ : ∀ (h : c < a) (hc : (f : (a : α) → β) c = b), c < a
⊢ c < a

Tactic:
rwa [← hc, f.lt_iff_lt] at h

Premises used: InitialSeg.lt_iff_lt
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
c : α
hc : c < a
⊢ LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)

Tactic:
f.strictMono hc

Premises used: InitialSeg.strictMono
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
c : α
hc : c < a
⊢ LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)

Tactic:
exact f.strictMono hc

Premises used: InitialSeg.strictMono
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
h : b ≤ (f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a
⊢ Membership.mem (γ := Set β)
    (Set.range.{u_2, u_1 + 1} (ι := α)
      (⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β))
    b

Tactic:
(f : α ≤i β).mem_range_of_le h

Premises used: InitialSeg.mem_range_of_le, Set.Mem, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ Set.range.{u_2, u_1 + 1} (ι := α)
      (⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β) =
    Set.Iio (f.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2))

Tactic:
f.range_eq

Premises used: Set.Iio, PrincipalSeg.range_eq
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : LT α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ IsLowerSet.{u_2} (α := β)
    (Set.range.{u_2, u_1 + 1} (ι := α)
      (⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β))

Tactic:
(f : α ≤i β).isLowerSet_range

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk, InitialSeg.isLowerSet_range
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a a' : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ LE.le.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a' : β) ↔
    a ≤ a'

Tactic:
(f : α ≤i β).le_iff_le

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk, InitialSeg.le_iff_le
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a a' : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ LT.lt.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a' : β) ↔
    a < a'

Tactic:
(f : α ≤i β).lt_iff_lt

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.lt_iff_lt, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ Monotone.{u_1, u_2} (α := α) (β := β)
    (⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β)

Tactic:
(f : α ≤i β).monotone

Premises used: InitialSeg.monotone, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ StrictMono.{u_1, u_2} (α := α) (β := β)
    (⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β)

Tactic:
(f : α ≤i β).strictMono

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.strictMono, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ IsMin.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β) ↔
    IsMin a

Tactic:
(f : α ≤i β).isMin_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk, InitialSeg.isMin_apply_iff
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : OrderBot β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ Eq.{u_2 + 1} (α := β)
    ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
(f : α ≤i β).map_bot

Premises used: InitialSeg.map_bot, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
a : α
⊢ Eq.{u_2 + 1} (α := Set β)
    ((⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β) ''
        Set.Iio a :
      Set β)
    (Set.Iio ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a) :
      Set β)

Tactic:
(f : α ≤i β).image_Iio a

Premises used: PrincipalSeg.toRelEmbedding, InitialSeg.image_Iio, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ b ≤ (f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a ↔
    ∃ c ≤ a, (f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) c = b

Tactic:
(f : α ≤i β).le_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.le_apply_iff, InitialSeg.mk
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
a : α
b : β
inst_1 : PartialOrder α
f : (fun (x1 x2 : α) ↦ x1 < x2) ≺i fun (x1 x2 : β) ↦ x1 < x2
⊢ b < (f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a ↔
    ∃ a' < a, (f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a' = b

Tactic:
(f : α ≤i β).lt_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.lt_apply_iff, InitialSeg.mk
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
s t : NonemptyInterval α
h : s.toProd = t.toProd
mk :
  ∀ (toProd : α × α) (fst_le_snd : toProd.1 ≤ toProd.2)
    (h : { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd = t.toProd),
    { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
t : NonemptyInterval α
toProd : α × α
fst_le_snd : toProd.1 ≤ toProd.2
h : { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd = t.toProd
mk :
  ∀ (toProd_1 : α × α) (fst_le_snd_1 : toProd_1.1 ≤ toProd_1.2)
    (h :
      { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd =
        { toProd := toProd_1, fst_le_snd := fst_le_snd_1 : NonemptyInterval α }.toProd),
    { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } =
      { toProd := toProd_1, fst_le_snd := fst_le_snd_1 }
⊢ { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } = t

Tactic:
cases t
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
toProd : α × α
fst_le_snd : toProd.1 ≤ toProd.2
toProd_1 : α × α
fst_le_snd_1 : toProd_1.1 ≤ toProd_1.2
h :
  { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α }.toProd =
    { toProd := toProd_1, fst_le_snd := fst_le_snd_1 : NonemptyInterval α }.toProd
⊢ { toProd := toProd, fst_le_snd := fst_le_snd : NonemptyInterval α } =
    { toProd := toProd_1, fst_le_snd := fst_le_snd_1 }

Tactic:
congr
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
s : NonemptyInterval α
⊢ s.toDualProd = ((toDual : (a : α) → αᵒᵈ) s.toProd.1, s.toProd.2)

Tactic:
rfl

Premises used: NonemptyInterval.toDualProd, OrderDual, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := NonemptyInterval α) toDualProd

Tactic:
toProd_injective

Premises used: NonemptyInterval.toDualProd, NonemptyInterval.toProd_injective, OrderDual
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
s t : NonemptyInterval α
inst_1 : IsEmpty α
⊢ IsEmpty.{u_1 + 1} (NonemptyInterval α)

Tactic:
⟨fun s => isEmptyElim s.fst⟩

Premises used: isEmptyElim, IsEmpty.mk, Prod.fst, NonemptyInterval.toProd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
s t : NonemptyInterval α
inst_1 : Subsingleton α
⊢ Subsingleton.{u_1 + 1} (NonemptyInterval α)

Tactic:
toDualProd_injective.subsingleton

Premises used: Function.Injective.subsingleton, NonemptyInterval.toDualProd_injective
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
s t : NonemptyInterval α
⊢ s ≤ t ↔ t.toProd.1 ≤ s.toProd.1 ∧ s.toProd.2 ≤ t.toProd.2

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
s : NonemptyInterval α
⊢ Eq (α := αᵒᵈ) ((toProd ((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) s)).1 : αᵒᵈ)
    ((toDual : (a : α) → αᵒᵈ) s.toProd.2 : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
s : NonemptyInterval α
⊢ Eq (α := αᵒᵈ) ((toProd ((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) s)).2 : αᵒᵈ)
    ((toDual : (a : α) → αᵒᵈ) s.toProd.1 : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone.{u_1, u_1} (α := NonemptyInterval α) toDualProd

Tactic:
fun _ _ => id

Premises used: Monotone, id
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ StrictMono.{u_1, u_1} (α := NonemptyInterval α) toDualProd

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
x : α × α
a : α
hx : x.1 ≤ x.2
⊢ a ∈ { toProd := x, fst_le_snd := hx : NonemptyInterval α } ↔ x.1 ≤ a ∧ a ≤ x.2

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Icc
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
s : NonemptyInterval α
a : α
⊢ a ∈ s ↔ s.toProd.1 ≤ a ∧ a ≤ s.toProd.2

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Icc
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
s : NonemptyInterval α
⊢ (Icc s.toProd.1 s.toProd.2).Nonempty

Tactic:
nonempty_Icc.2 s.fst_le_snd

Premises used: Iff.mpr, Set.nonempty_Icc, NonemptyInterval.fst_le_snd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Membership.mem (γ := NonemptyInterval α) (pure a) a

Tactic:
⟨le_rfl, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := NonemptyInterval α) pure

Tactic:
fun _ _ =>
  congr_arg <| Prod.fst ∘ toProd

Premises used: Function.comp, Prod.fst, congr_arg, Function.Injective, NonemptyInterval.toProd
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := NonemptyInterval αᵒᵈ)
    ((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) (pure a) : NonemptyInterval αᵒᵈ)
    (pure ((toDual : (a : α) → αᵒᵈ) a) : NonemptyInterval αᵒᵈ)

Tactic:
rfl

Premises used: NonemptyInterval.pure, Prod.swap, OrderDual, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : NonemptyInterval α
x : α × α
a : α
inst_3 : Nonempty α
⊢ Nonempty α

Tactic:
infer_instance
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : NonemptyInterval α
x : α × α
a : α
inst_3 : Nontrivial α
⊢ Nontrivial.{u_1} (NonemptyInterval α)

Tactic:
pure_injective.nontrivial

Premises used: Function.Injective.nontrivial, NonemptyInterval.pure_injective
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : α
⊢ map f (pure a) = pure ((f : (a : α) → β) a)

Tactic:
rfl

Premises used: NonemptyInterval.pure, Prod.map, rfl, NonemptyInterval.map