awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

Tactic:
Or.inl h2.symm

Premises used: Or.inl, Eq.symm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

Tactic:
exact Or.inl h2.symm

Premises used: Or.inl, Eq.symm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3 : c ≤ b
h2 : a < c
inr : ∀ (h3 : c = b), c = a ∨ c = b
inr₁ : ∀ (h3 : c < b), c = a ∨ c = b
⊢ c = a ∨ c = b

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

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3_1 : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

Tactic:
Or.inr h3

Premises used: Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3_1 : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

Tactic:
exact Or.inr h3

Premises used: Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3_1 : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Tactic:
(h.2 h2 h3).elim

Premises used: False.elim, And.right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
h2_1 : a ≤ c
h3_1 : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Tactic:
exact (h.2 h2 h3).elim

Premises used: False.elim, And.right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ≤ b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b

Tactic:
⟨fun h => ⟨h.le, fun _ => h.eq_or_eq⟩, And.rec wcovBy_of_eq_or_eq⟩

Premises used: And.rec, WCovBy.eq_or_eq, And.intro, Iff.intro, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩

Premises used: WCovBy.eq_or_eq, And.right, And.left, Iff.intro
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
refine : c = a ∨ c = b → a ≤ c ∧ c ≤ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

Tactic:
⟨le_rfl, h.le⟩

Premises used: le_rfl, And.intro, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c

Tactic:
⟨h.le, le_rfl⟩

Premises used: le_rfl, And.intro, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

Tactic:
exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
h₁ : ∀ (c : α), c ∈ Icc a b ↔ Membership.mem (γ := Set α) {a, b} c
⊢ Icc a b = {a, b}

Tactic:
ext c
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ Membership.mem (γ := Set α) {a, b} c

Tactic:
h.le_and_le_iff

Premises used: Set.insert, Set.Mem, setOf, Set.Icc, Set.singleton, WCovBy.le_and_le_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ Membership.mem (γ := Set α) {a, b} c

Tactic:
exact h.le_and_le_iff

Premises used: WCovBy.le_and_le_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
rw : Icc a b \ {b} ⊆ {a}
rw₁ : Subset (α := Set α) ({a, b} \ {b}) {a}
rw₂ : Subset (α := Set α) {a, b} {b, a}
rw₃ rw₄ : Subset (α := Set α) {b, a} {b, a}
⊢ Ico a b ⊆ {a}

Tactic:
rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]

Premises used: Set.diff_singleton_subset_iff, WCovBy.Icc_eq, Set.Icc_diff_right, Set.pair_comm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
rw : Icc a b \ {a} ⊆ {b}
rw₁ : Subset (α := Set α) ({a, b} \ {a}) {b}
rw₂ rw₃ : Subset (α := Set α) {a, b} {a, b}
⊢ Ioc a b ⊆ {b}

Tactic:
rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]

Premises used: Set.diff_singleton_subset_iff, Set.Icc_diff_left, WCovBy.Icc_eq
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : SemilatticeSup α
a b c : α
hac : a ⩿ c
hbc : b ⩿ c
hab : a ≠ b
⊢ a ⊔ b = c

Tactic:
(sup_le hac.le hbc.le).eq_of_not_lt fun h =>
    hab.lt_sup_or_lt_sup.elim (fun h' => hac.2 h' h) fun h' => hbc.2 h' h

Premises used: Ne.lt_sup_or_lt_sup, LE.le.eq_of_not_lt, And.right, sup_le, Or.elim, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LT α
a b : α
h : a ⋖ b
⊢ a < b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LT α
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 [CovBy, h, true_and, not_forall, exists_prop, not_not]

Premises used: Classical.not_not, CovBy, exists_prop, Classical.not_forall, true_and
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LT α
a b : α
inst_1 : DenselyOrdered α
⊢ ¬a ⋖ b

Tactic:
fun h =>
  let ⟨_, hc⟩ := exists_between h.1
  h.2 hc.1 hc.2

Premises used: False, exists_between, And.right, And.left, _private.0.not_covBy.match_1, Not
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LT α
⊢ DenselyOrdered α ↔ ∀ (a b : α), ¬a ⋖ b

Tactic:
⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h =>
    ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩

Premises used: not_covBy, exists_lt_lt_of_not_covBy, DenselyOrdered.mk, Iff.intro
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ CovBy (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ a ⋖ b

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

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

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

Premises used: and_congr_right', CovBy, forall_comm, forall_congr'
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ (Ioo a b).Nonempty

Tactic:
not_covBy_iff h

Premises used: Set.Mem, setOf, Set.Nonempty, not_covBy_iff, Set.Ioo
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⋖ b
⊢ a ≤ b

Tactic:
h.1.le

Premises used: LT.lt.le, And.left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⋖ b
⊢ a ≠ b

Tactic:
h.lt.ne

Premises used: CovBy.lt, LT.lt.ne
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⋖ b
⊢ a ⩿ b

Tactic:
⟨h.le, h.2⟩

Premises used: And.right, And.intro, WCovBy, CovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⩿ b
h2 : ¬b ≤ a
⊢ a ⋖ b

Tactic:
⟨h.le.lt_of_not_ge h2, h.2⟩

Premises used: LE.le.lt_of_not_ge, CovBy, And.right, And.intro, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⩿ b
h2 : a < b
⊢ a ⋖ b

Tactic:
⟨h2, h.2⟩

Premises used: CovBy, And.right, And.intro
-- 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: CovBy, And.right, And.intro, LE.le.trans_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
hac : a ⋖ c
hab : a < b
hbc : b ≤ c
⊢ a ⋖ b

Tactic:
⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩

Premises used: CovBy, And.right, LT.lt.trans_le, And.intro
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b c : α
h₁ : a < b
h₂ : b < c
⊢ ¬a ⋖ c

Tactic:
(not_covBy_iff (h₁.trans h₂)).2 ⟨b, h₁, h₂⟩

Premises used: Iff.mpr, And.intro, Exists.intro, LT.lt.trans, not_covBy_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ (c : α), c ∈ Ioo a b

Tactic:
not_covBy_iff h

Premises used: Set.Mem, setOf, not_covBy_iff, Set.Ioo
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ⋖ b ↔ a ⩿ b ∧ a < b

Tactic:
⟨fun h => ⟨h.wcovBy, h.lt⟩, fun h => h.1.covBy_of_lt h.2⟩

Premises used: WCovBy.covBy_of_lt, And.right, And.left, And.intro, Iff.intro, CovBy.wcovBy, CovBy.lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a

Tactic:
⟨fun h => ⟨h.wcovBy, h.lt.not_ge⟩, fun h => h.1.covBy_of_not_le h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, CovBy.wcovBy, CovBy.lt, WCovBy.covBy_of_not_le, LT.lt.not_ge
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a

Tactic:
⟨fun h => or_iff_not_imp_right.mpr fun h' => h.covBy_of_not_le fun hba => h' ⟨h.le, hba⟩,
    fun h' => h'.elim (fun h => h.wcovBy) fun h => h.1.wcovBy_of_le h.2⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, And.right, And.left, And.intro, Iff.intro, CovBy.wcovBy, WCovBy.covBy_of_not_le, Or.elim, WCovBy.le, LE.le.wcovBy_of_le
-- 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_lt hbc.lt, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩

Premises used: CovBy, And.right, And.left, And.intro, CovBy.lt, LE.le.trans_lt
-- 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_covBy, hab.trans_covBy⟩

Premises used: Iff.intro, AntisymmRel.trans_covBy, 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.lt.trans_le hbc.1, fun _ had hdb => hab.2 had <| hdb.trans_le hbc.2⟩

Premises used: CovBy, And.right, And.left, LT.lt.trans_le, And.intro, CovBy.lt
-- 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_antisymmRel hab, fun h => h.trans_antisymmRel hab.symm⟩

Premises used: Iff.intro, AntisymmRel.symm, CovBy.trans_antisymmRel
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b c : α
⊢ IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⩿ x2) fun (x1 x2 : α) ↦ x1 ⋖ x2

Tactic:
⟨fun _ _ =>
    covBy_iff_wcovBy_and_not_le.trans <| and_congr_right fun h => h.wcovBy_iff_le.not.symm⟩

Premises used: Iff.not, and_congr_right, covBy_iff_wcovBy_and_not_le, Iff.trans, WCovBy.wcovBy_iff_le, IsNonstrictStrictOrder.mk, Iff.symm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b c : α
⊢ Std.Irrefl fun (x1 x2 : α) ↦ x1 ⋖ x2

Tactic:
⟨fun _ ha => ha.ne rfl⟩

Premises used: CovBy.ne, Std.Irrefl.mk, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ⋖ b
⊢ Ioo a b = ∅

Tactic:
h.wcovBy.Ioo_eq

Premises used: WCovBy.Ioo_eq, CovBy.wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : α
f : α ↪o β
h : CovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ a ⋖ b

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

Premises used: Iff.mpr, CovBy, And.right, And.intro, Iff.mp, CovBy.lt, 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 : α) → β))
⊢ CovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
(hab.wcovBy.image f h).covBy_of_lt <| f.strictMono hab.lt

Premises used: OrderEmbedding.strictMono, WCovBy.covBy_of_lt, CovBy.wcovBy, CovBy.lt, WCovBy.image
-- 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 : α) → β))
⊢ CovBy.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a ⋖ b

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

Premises used: CovBy.image, Iff.intro, CovBy.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
⊢ CovBy.{u_2} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) ↔ a ⋖ b

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

Premises used: Set.ordConnected_range, OrderIsoClass.toOrderIso, Set.OrdConnected.apply_covBy_apply_iff, RelIso.toRelEmbedding
-- 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: CovBy, LT.lt.le, LT.lt.ne', And.intro, Or.elim, LT.lt.ne
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
h2 : a ≠ b
⊢ a ⋖ b

Tactic:
⟨h.le.lt_of_ne h2, h.2⟩

Premises used: CovBy, LE.le.lt_of_ne, And.right, And.intro, WCovBy.le
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ⋖ b ↔ a ⩿ b ∧ a ≠ b

Tactic:
⟨fun h => ⟨h.wcovBy, h.ne⟩, fun h => h.1.covBy_of_ne h.2⟩

Premises used: CovBy.ne, WCovBy.covBy_of_ne, And.right, And.left, And.intro, Iff.intro, CovBy.wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
rw₁ rw₂ : a ⋖ b ∨ a ≤ b ∧ b ≤ a ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b

Tactic:
rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]

Premises used: wcovBy_iff_covBy_or_le_and_le, le_antisymm_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a = b ∨ a ⋖ b

Tactic:
wcovBy_iff_covBy_or_eq.trans or_comm

Premises used: wcovBy_iff_covBy_or_eq, Iff.trans, or_comm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⋖ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b

Tactic:
h.wcovBy.eq_or_eq h2 h3

Premises used: WCovBy.eq_or_eq, CovBy.wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ⋖ b ↔ a < b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b

Tactic:
⟨fun h => ⟨h.lt, fun _ => h.eq_or_eq⟩, And.rec covBy_of_eq_or_eq⟩

Premises used: And.rec, CovBy.eq_or_eq, And.intro, Iff.intro, CovBy.lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⋖ b
rw : Ioo a b ∪ {a} = {a}
rw₁ : Eq (α := Set α) (∅ ∪ {a}) {a}
rw₂ rw₃ : Eq (α := Set α) {a} {a}
⊢ Ico a b = {a}

Tactic:
rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]

Premises used: Set.Ioo_union_left, Set.empty_union, CovBy.lt, CovBy.Ioo_eq
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⋖ b
⊢ Icc a b = {a, b}

Tactic:
h.wcovBy.Icc_eq

Premises used: WCovBy.Icc_eq, CovBy.wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ⩿ b
hcb : c < b
⊢ c ≤ a

Tactic:
not_lt.1 fun hac => hab.2 hac hcb

Premises used: not_lt, And.right, Iff.mp
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ⋖ b
⊢ c < b → c ≤ a

Tactic:
hab.wcovBy.le_of_lt

Premises used: WCovBy.le_of_lt, CovBy.wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
rw : Ioo a b ∪ Ici b = Ici b
rw₁ : ∅ ∪ Ici b = Ici b
rw₂ rw₃ : Ici b = Ici b
⊢ Ioi a = Ici b

Tactic:
rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]

Premises used: Set.Ioo_union_Ici_eq_Ioi, Set.empty_union, CovBy.lt, CovBy.Ioo_eq
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
rw : Iic a ∪ Ioo a b = Iic a
rw₁ : Iic a ∪ ∅ = Iic a
rw₂ rw₃ : Iic a = Iic a
⊢ Iio b = Iic a

Tactic:
rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]

Premises used: Set.union_empty, CovBy.lt, Set.Iic_union_Ioo_eq_Iio, CovBy.Ioo_eq
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
c : α
⊢ Ioo a c = Ico b c

Tactic:
subset_antisymm (fun _x hx ↦ ⟨h.ge_of_gt hx.1, hx.2⟩) <| Ico_subset_Ioo_left h.lt

Premises used: subset_antisymm, CovBy.lt, Set.Ico_subset_Ioo_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
ha : a ⋖ c
hb : b ⋖ c
⊢ a = b

Tactic:
(hb.le_of_lt ha.lt).antisymm <| ha.le_of_lt hb.lt

Premises used: CovBy.le_of_lt, LE.le.antisymm, CovBy.lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b c x : α
hab : a ⋖ b
hbc : b ⋖ c
hax : a < x
hxc : x < c
⊢ x = b

Tactic:
le_antisymm (le_of_not_gt fun h => hbc.2 h hxc) (le_of_not_gt <| hab.2 hax)

Premises used: le_of_not_gt, le_antisymm, And.right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
simp_rw : (∀ {z : α}, z < y ↔ z ≤ x) ↔ ∀ {z : α}, z ≤ x ↔ z < y
⊢ x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y

Tactic:
simp_rw [covBy_iff_lt_iff_le_left, iff_comm]

Premises used: covBy_iff_lt_iff_le_left, iff_comm
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
grind
-- Module: Mathlib.Order.Cover
Goal:
⊢ ∀ {a b : Bool}, (a ≤ b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a ≤ b

Tactic:
decide
-- Module: Mathlib.Order.Cover
Goal:
⊢ ∀ {a b : Bool}, (a < b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a < b

Tactic:
decide
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s : Set α
⊢ s ⩿ insert x s

Tactic:
wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_

Premises used: wcovBy_of_eq_or_eq, Set.subset_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s : Set α
refine : ∀ (t : Set α) (hst : s ≤ t) (h2t : t ≤ insert x s), t = s ∨ t = insert x s
⊢ s ⩿ insert x s

Tactic:
refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_

Premises used: wcovBy_of_eq_or_eq, Set.subset_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
pos : ∀ (h : x ∈ t), t = s ∨ t = insert x s
neg : ∀ (h : x ∉ t), t = s ∨ t = insert x s
⊢ t = s ∨ t = insert x s

Tactic:
by_cases h : x ∈ t
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

Tactic:
Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)

Premises used: Iff.mpr, subset_antisymm, Set.insert_subset_iff, And.intro, Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

Tactic:
exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)

Premises used: Iff.mpr, subset_antisymm, Set.insert_subset_iff, And.intro, Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
Or.inl (subset_antisymm ?_ hst)

Premises used: subset_antisymm, Or.inl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
neg : t ⊆ s
⊢ t = s ∨ t = insert x s

Tactic:
refine Or.inl (subset_antisymm ?_ hst)

Premises used: subset_antisymm, Or.inl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
neg : t \ {x} ⊆ s
neg₁ neg₂ neg₃ neg₄ : t ⊆ insert x s
⊢ t ⊆ s

Tactic:
rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]

Premises used: Set.diff_singleton_subset_iff, Set.diff_singleton_eq_self
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
pos : ∀ (ha : a ∈ s), s \ {a} ⩿ s
neg : ∀ (ha : a ∉ s), s \ {a} ⩿ s
⊢ s \ {a} ⩿ s

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⩿ insert a (s \ {a})

Tactic:
wcovBy_insert a _

Premises used: Set.wcovBy_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
h : s = insert a (s \ {a})
⊢ s \ {a} ⩿ s

Tactic:
convert! wcovBy_insert a _

Premises used: Set.wcovBy_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
h : ∀ (x : α), x ∈ s ↔ x ∈ insert a (s \ {a})
⊢ s = insert a (s \ {a})

Tactic:
ext
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x : α
⊢ x ∈ s ↔ x ∈ insert a (s \ {a})

Tactic:
simp [ha]
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s

Tactic:
simp [ha]
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
(wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha

Premises used: Set.ssubset_insert, WCovBy.covBy_of_lt, Set.wcovBy_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⋖ s

Tactic:
⟨sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _, (sdiff_singleton_wcovBy _ _).2⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.sdiff_singleton_wcovBy, CovBy, And.right, And.intro, sdiff_lt, Set.singleton_ne_empty
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s t : Set α
h : s ⋖ t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
let ⟨a, ha, hst⟩ := ssubset_iff_insert.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_insert ha).symm⟩

Premises used: Set.ssubset_insert, Membership.mem, Exists, _private.0.CovBy.exists_set_insert.match_1, Insert.insert, And, And.right, And.intro, Exists.intro, Iff.mp, HasSubset.Subset.eq_of_not_ssuperset, CovBy.lt, Eq.symm, Eq, Not, Set.ssubset_iff_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s t : Set α
h : s ⋖ t
⊢ ∃ a ∈ t, t \ {a} = s

Tactic:
let ⟨a, ha, hst⟩ := ssubset_iff_sdiff_singleton.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssubset fun h' ↦ h.2 h' <|
    sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _).symm⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.ssubset_iff_sdiff_singleton, Membership.mem, Exists, HasSubset.Subset.eq_of_not_ssubset, SDiff.sdiff, And, And.right, _private.0.CovBy.exists_set_sdiff_singleton.match_1, And.intro, Exists.intro, Iff.mp, CovBy.lt, Singleton.singleton, Eq.symm, Eq, sdiff_lt, Set.singleton_ne_empty
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
covBy_insert ha

Premises used: Set.covBy_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
exact covBy_insert ha

Premises used: Set.covBy_insert
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t

Tactic:
sdiff_singleton_covBy ha

Premises used: Set.sdiff_singleton_covBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t

Tactic:
exact sdiff_singleton_covBy ha

Premises used: Set.sdiff_singleton_covBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
h : ∀ (x y : α), x ⩿ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ⩿ x2) (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2)

Tactic:
ext x y
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
x y : α
h : x = y ∨ x ⋖ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
h₁ : y = x ∨ x ⋖ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ x ⩿ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]

Premises used: wcovBy_iff_eq_or_covBy, eq_comm, Relation.reflGen_iff