awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
a₁ a₂ : α
f : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hf : f ∈ our_ideal
ha₁ : (a₁, (↑(F a₁) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
intro :
  ∀ (g : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) (hg : g ∈ our_ideal)
    (ha₂ : (a₂, (↑(F a₂) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑g : Finset (α × (↑(Set.Ioo x y) : Type u_2)))),
    a₁ < a₂ →
      LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
        ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)
⊢ a₁ < a₂ →
    LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
      ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)

Tactic:
rcases (F a₂).prop with ⟨g, hg, ha₂⟩

Premises used: Subtype.prop
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
a₁ a₂ : α
f : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hf : f ∈ our_ideal
ha₁ : (a₁, (↑(F a₁) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
g : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hg : g ∈ our_ideal
ha₂ : (a₂, (↑(F a₂) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑g : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
intro :
  ∀ (m : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2))
    (_hm : m ∈ (↑our_ideal : Set (PartialIso α (↑(Set.Ioo x y) : Type u_2)))) (fm : f ≤ m) (gm : g ≤ m),
    a₁ < a₂ →
      LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
        ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)
⊢ a₁ < a₂ →
    LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
      ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)

Tactic:
rcases our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩

Premises used: Order.Ideal.directed
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
a₁ a₂ : α
f : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hf : f ∈ our_ideal
ha₁ : (a₁, (↑(F a₁) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
g : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hg : g ∈ our_ideal
ha₂ : (a₂, (↑(F a₂) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑g : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
m : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
_hm : m ∈ (↑our_ideal : Set (PartialIso α (↑(Set.Ioo x y) : Type u_2)))
fm : f ≤ m
gm : g ≤ m
⊢ a₁ < a₂ →
    LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
      ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)

Tactic:
(lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp

Premises used: lt_iff_lt_of_cmp_eq_cmp, Prod.mk, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered β
inst_4 : Nontrivial β
val : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty.{u_2 + 1} (↑(Set.Ioo x y) : Type u_2)
our_ideal : Ideal (PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)) :=
  idealOfCofinals default (definedAtLeft (↑(Set.Ioo x y) : Type u_2))
F : (a : α) →
  { b : (↑(Set.Ioo x y) : Type u_2) // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2))) } :=
  fun (a : α) ↦ funOfIdeal a our_ideal ⋯
a₁ a₂ : α
f : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hf : f ∈ our_ideal
ha₁ : (a₁, (↑(F a₁) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑f : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
g : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
hg : g ∈ our_ideal
ha₂ : (a₂, (↑(F a₂) : (↑(Set.Ioo x y) : Type u_2))) ∈ (↑g : Finset (α × (↑(Set.Ioo x y) : Type u_2)))
m : PartialIso.{u_1, u_2} α (↑(Set.Ioo x y) : Type u_2)
_hm : m ∈ (↑our_ideal : Set (PartialIso α (↑(Set.Ioo x y) : Type u_2)))
fm : f ≤ m
gm : g ≤ m
⊢ a₁ < a₂ →
    LT.lt.{u_2} (α := (↑(Set.Ioo x y) : Type u_2)) ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₁)
      ((fun (a : α) ↦ (↑(F a) : (↑(Set.Ioo x y) : Type u_2))) a₂)

Tactic:
exact (lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp

Premises used: lt_iff_lt_of_cmp_eq_cmp, Prod.mk, Subtype.prop, Iff.mp
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
intro : ∀ (val : Encodable α), Nonempty (α ≃o β)
⊢ Nonempty (α ≃o β)

Tactic:
cases nonempty_encodable α

Premises used: nonempty_encodable
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
intro : ∀ (val : Encodable β), Nonempty (α ≃o β)
⊢ Nonempty (α ≃o β)

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
rcases :
  ∀ (f : PartialIso α β) (hf : f ∈ our_ideal) (ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))),
    cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b

Tactic:
rcases (F a).prop with ⟨f, hf, ha⟩

Premises used: Subtype.prop
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))
rcases :
  ∀ (g : PartialIso α β) (hg : g ∈ our_ideal) (hb : ((↑(G b) : α), b) ∈ (↑g : Finset (α × β))),
    cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b

Tactic:
rcases (G b).prop with ⟨g, hg, hb⟩

Premises used: Subtype.prop
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))
g : PartialIso α β
hg : g ∈ our_ideal
hb : ((↑(G b) : α), b) ∈ (↑g : Finset (α × β))
rcases :
  ∀ m ∈ (↑our_ideal : Set (PartialIso α β)),
    ∀ (fm : f ≤ m) (gm : g ≤ m), cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b

Tactic:
rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩

Premises used: Order.Ideal.directed
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))
g : PartialIso α β
hg : g ∈ our_ideal
hb : ((↑(G b) : α), b) ∈ (↑g : Finset (α × β))
m : PartialIso α β
left : m ∈ (↑our_ideal : Set (PartialIso α β))
fm : f ≤ m
gm : g ≤ m
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b

Tactic:
m.prop (a, _) (fm ha) (_, b) (gm hb)

Premises used: Prod.mk, Subtype.prop
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, (↑(F a) : β)) ∈ (↑f : Finset (α × β))
g : PartialIso α β
hg : g ∈ our_ideal
hb : ((↑(G b) : α), b) ∈ (↑g : Finset (α × β))
m : PartialIso α β
left : m ∈ (↑our_ideal : Set (PartialIso α β))
fm : f ≤ m
gm : g ≤ m
⊢ cmp a ((fun (b : β) ↦ (↑(G b) : α)) b) = cmp ((fun (a : α) ↦ (↑(F a) : β)) a) b

Tactic:
exact m.prop (a, _) (fm ha) (_, b) (gm hb)

Premises used: Prod.mk, Subtype.prop
-- Module: Mathlib.Order.CountableDenseLinearOrder
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
val : Encodable α
val_1 : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) :=
  fun (p : α ⊕ β) ↦
    Sum.recOn (motive := fun (x : α ⊕ β) ↦ Cofinal (PartialIso α β)) p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b : β // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (a : α) ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a : α // ∃ f ∈ our_ideal, (a, b) ∈ (↑f : Finset (α × β)) } := fun (b : β) ↦ invOfIdeal b our_ideal ⋯
⊢ Nonempty (α ≃o β)

Tactic:
exact ⟨OrderIso.ofCmpEqCmp (fun a ↦ (F a).val) (fun b ↦ (G b).val) fun a b ↦ by
      rcases (F a).prop with ⟨f, hf, ha⟩
      rcases (G b).prop with ⟨g, hg, hb⟩
      rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
      exact m.prop (a, _) (fm ha) (_, b) (gm hb)⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⩿ b
⊢ a ≤ b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ a ⩿ a

Tactic:
⟨le_rfl, fun _ hc => hc.not_gt⟩

Premises used: le_rfl, And.intro, WCovBy, LT.lt.not_gt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ a ⩿ a

Tactic:
WCovBy.refl a

Premises used: WCovBy.refl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a = b
⊢ a ⩿ b

Tactic:
h ▸ WCovBy.rfl

Premises used: Eq.rec, WCovBy.rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h1 : a ≤ b
h2 : b ≤ a
⊢ a ⩿ b

Tactic:
⟨h1, fun _ hac hcb => (hac.trans hcb).not_ge h2⟩

Premises used: And.intro, WCovBy, LT.lt.trans, LT.lt.not_ge
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ⩿ b

Tactic:
wcovBy_of_le_of_le h.1 h.2

Premises used: wcovBy_of_le_of_le, And.right, And.left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a ⩿ b
⊢ b ⩿ a ↔ b ≤ a

Tactic:
⟨fun h => h.le, fun h => h.wcovBy_of_le hab.le⟩

Premises used: Iff.intro, WCovBy.le, LE.le.wcovBy_of_le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a ≤ b
h : ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b
⊢ a ⩿ b

Tactic:
⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩

Premises used: LT.lt.le, LT.lt.ne', And.intro, WCovBy, Or.elim, LT.lt.ne
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
hbc : b ⩿ c
⊢ a ⩿ c

Tactic:
⟨hab.1.trans hbc.le, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩

Premises used: And.right, And.left, And.intro, WCovBy, LE.le.trans, LE.le.trans_lt, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ⩿ c ↔ b ⩿ c

Tactic:
⟨hab.symm.trans_wcovBy, hab.trans_wcovBy⟩

Premises used: Iff.intro, AntisymmRel.trans_wcovBy, AntisymmRel.symm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : a ⩿ b
hbc : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ a ⩿ c

Tactic:
⟨hab.le.trans hbc.1, fun _ had hdc => hab.2 had <| hdc.trans_le hbc.2⟩

Premises used: And.right, And.left, LT.lt.trans_le, And.intro, WCovBy, LE.le.trans, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hab : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ c ⩿ a ↔ c ⩿ b

Tactic:
⟨fun h => h.trans_antisymm_rel hab, fun h => h.trans_antisymm_rel hab.symm⟩

Premises used: WCovBy.trans_antisymm_rel, Iff.intro, AntisymmRel.symm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
simp_rw : ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₁ : ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₂ : (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₃ : (∃ (x : α) (_ : a < x), ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
simp_rw₄ : (∃ (x : α), a < x ∧ ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
⊢ ¬a ⩿ b ↔ ∃ (c : α), a < c ∧ c < b

Tactic:
simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]

Premises used: Classical.not_not, exists_prop, WCovBy, Classical.not_forall, true_and
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b c : α
⊢ Std.Refl fun (x1 x2 : α) ↦ x1 ⩿ x2

Tactic:
⟨WCovBy.refl⟩

Premises used: Std.Refl.mk, WCovBy.refl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⩿ b
⊢ Ioo a b = ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun _ hx => h.2 hx.1 hx.2

Premises used: Iff.mpr, And.right, And.left, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅

Tactic:
simp [eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hac : a ⩿ c
hab : a ≤ b
hbc : b ≤ c
⊢ b ⩿ c

Tactic:
⟨hbc, fun _x hbx hxc ↦ hac.2 (hab.trans_lt hbx) hxc⟩

Premises used: And.right, And.intro, WCovBy, LE.le.trans_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
h : WCovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ a ⩿ b

Tactic:
⟨f.le_iff_le.mp h.le, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩

Premises used: Iff.mpr, And.right, And.intro, WCovBy, Iff.mp, OrderEmbedding.lt_iff_lt, OrderEmbedding.le_iff_le, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ WCovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
⟨f.monotone hab.le, fun c ha hb => ?_⟩

Premises used: OrderEmbedding.monotone, And.intro, WCovBy, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
refine : ∀ (c : β) (ha : (f : (a : α) → β) a < c) (hb : c < (f : (a : α) → β) b), False
⊢ WCovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : β
ha : (f : (a : α) → β) a < c
hb : c < (f : (a : α) → β) b
obtain :
  ∀ (c : α) (ha : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β))
    (hb : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) b : β)), False
⊢ False

Tactic:
obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩

Premises used: Set.mem_range_self, Set.OrdConnected.out, LT.lt.le, WCovBy.rfl, And.intro
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : α
ha : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β)
hb : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) b : β)
⊢ a < c

Tactic:
rw [f.lt_iff_lt] at ha hb

Premises used: OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : α
ha : LT.lt.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β)
hb : LT.lt.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) b : β)
ha₁ : a < c
⊢ c < b

Tactic:
rw [f.lt_iff_lt] at ha hb

Premises used: OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : α
ha : a < c
hb : c < b
⊢ False

Tactic:
hab.2 ha hb

Premises used: And.right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
c : α
ha : a < c
hb : c < b
⊢ False

Tactic:
exact hab.2 ha hb

Premises used: And.right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
h : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ WCovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a ⩿ b

Tactic:
⟨fun h2 => h2.of_image f, fun hab => hab.image f h⟩

Premises used: Iff.intro, WCovBy.image, WCovBy.of_image
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
E : Type u_3
inst_2 : EquivLike E α β
inst_3 : OrderIsoClass E α β
e : E
⊢ WCovBy.{u_2} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) ↔ a ⩿ b

Tactic:
(ordConnected_range (e : α ≃o β)).apply_wcovBy_apply_iff ((e : α ≃o β) : α ↪o β)

Premises used: Set.ordConnected_range, OrderIsoClass.toOrderIso, RelIso.toRelEmbedding, Set.OrdConnected.apply_wcovBy_apply_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ WCovBy (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ a ⩿ b

Tactic:
and_congr_right' <| forall_congr' fun _ => forall_comm

Premises used: and_congr_right', forall_comm, WCovBy, forall_congr'
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : αᵒᵈ
⊢ WCovBy (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ⩿ a

Tactic:
and_congr_right' <| forall_congr' fun _ => forall_comm

Premises used: and_congr_right', forall_comm, WCovBy, forall_congr'
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
inl : ∀ (h2 : a = c), c = a ∨ c = b
inr : ∀ (h2 : a < c), c = a ∨ c = b
⊢ c = a ∨ c = b

Tactic:
rcases h2.eq_or_lt with (h2 | h2)

Premises used: LE.le.eq_or_lt