awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
rw :
  Eq.{u_1 + 1} (α := α → α → Prop) (TransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2))
    (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := α → α → Prop) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (TransGen fun (x1 x2 : α) ↦ x1 ⩿ x2) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)

Tactic:
rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]

Premises used: Relation.transGen_reflGen, wcovBy_eq_reflGen_covBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : PartialOrder α
rw :
  Eq.{u_1 + 1} (α := (a : α) → α → Prop) (ReflTransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2))
    (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := (a : α) → α → Prop) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
    (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
⊢ Eq.{u_1 + 1} (α := (a : α) → α → Prop) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⩿ x2)
    (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)

Tactic:
rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen]

Premises used: Relation.reflTransGen_reflGen, wcovBy_eq_reflGen_covBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
⊢ x.swap ⩿ y.swap ↔ x ⩿ y

Tactic:
apply_wcovBy_apply_iff (OrderIso.prodComm : α × β ≃o β × α)

Premises used: OrderIso.prodComm, apply_wcovBy_apply_iff, Prod.swap
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
⊢ x.swap ⋖ y.swap ↔ x ⋖ y

Tactic:
apply_covBy_apply_iff (OrderIso.prodComm : α × β ≃o β × α)

Premises used: OrderIso.prodComm, apply_covBy_apply_iff, Prod.swap
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
h : x ⩿ y
by_contra! : ∀ (ha : x.1 ≠ y.1) (hb : x.2 ≠ y.2), False
⊢ x.1 = y.1 ∨ x.2 = y.2

Tactic:
by_contra! ⟨ha, hb⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
h : x ⩿ y
ha : x.1 ≠ y.1
hb : x.2 ≠ y.2
⊢ False

Tactic:
h.2 (mk_lt_mk.2 <| Or.inl ⟨ha.lt_of_le h.1.1, le_rfl⟩)
      (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hb.lt_of_le h.1.2⟩)

Premises used: Iff.mpr, le_rfl, And.right, And.left, And.intro, Or.inl, Prod.mk_lt_mk, Ne.lt_of_le, Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
h : x ⩿ y
ha : x.1 ≠ y.1
hb : x.2 ≠ y.2
⊢ False

Tactic:
exact
    h.2 (mk_lt_mk.2 <| Or.inl ⟨ha.lt_of_le h.1.1, le_rfl⟩)
      (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hb.lt_of_le h.1.2⟩)

Premises used: Iff.mpr, le_rfl, And.right, And.left, And.intro, Or.inl, Prod.mk_lt_mk, Ne.lt_of_le, Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
h : x ⩿ y
⊢ x.1 ⩿ y.1

Tactic:
⟨h.1.1, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_left.2 h₁) ⟨⟨h₂.le, h.1.2⟩, fun hc => h₂.not_ge hc.1⟩⟩

Premises used: Iff.mpr, LT.lt.le, And.right, And.left, And.intro, WCovBy, LT.lt.not_ge, Prod.mk_lt_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
h : x ⩿ y
⊢ x.2 ⩿ y.2

Tactic:
⟨h.1.2, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_right.2 h₁) ⟨⟨h.1.1, h₂.le⟩, fun hc => h₂.not_ge hc.2⟩⟩

Premises used: Iff.mpr, LT.lt.le, And.right, And.left, Prod.mk_lt_mk_iff_right, And.intro, WCovBy, LT.lt.not_ge
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Tactic:
⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩

Premises used: Iff.mpr, And.imp, WCovBy.fst, Iff.intro, Prod.mk_le_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
refine : ∀ (h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂) (c : α × β) (h₁ : (a₁, b) < c) (h₂ : c < (a₂, b)), False
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Tactic:
refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
⊢ c.2 = b

Tactic:
have : c.2 = b := h₂.le.2.antisymm h₁.le.2
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
⊢ a₁ < c.1

Tactic:
rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂

Premises used: Prod.mk.eta, Prod.mk_lt_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
h₃ : a₁ < c.1
⊢ c.1 < a₂

Tactic:
rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂

Premises used: Prod.mk.eta, Prod.mk_lt_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
h₃ : a₁ < c.1
h₄ : c.1 < a₂
⊢ c.2 = b

Tactic:
rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂

Premises used: Prod.mk.eta, Prod.mk_lt_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : a₁ < c.1
h₂ : c.1 < a₂
this : c.2 = b
⊢ False

Tactic:
h h₁ h₂
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : a₁ < c.1
h₂ : c.1 < a₂
this : c.2 = b
⊢ False

Tactic:
exact h h₁ h₂
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂

Tactic:
swap_wcovBy_swap.trans mk_wcovBy_mk_iff_left

Premises used: Prod.swap_wcovBy_swap, Iff.trans, Prod.swap, Prod.mk_wcovBy_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
simp_rw : (a₁, b) ⩿ (a₂, b) ∧ (a₁, b) < (a₂, b) ↔ a₁ ⩿ a₂ ∧ a₁ < a₂
simp_rw₁ : a₁ ⩿ a₂ ∧ (a₁, b) < (a₂, b) ↔ a₁ ⩿ a₂ ∧ a₁ < a₂
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂

Tactic:
simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]

Premises used: Prod.mk_lt_mk_iff_left, covBy_iff_wcovBy_and_lt, Prod.mk_wcovBy_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a : α
b₁ b₂ : β
simp_rw : (a, b₁) ⩿ (a, b₂) ∧ (a, b₁) < (a, b₂) ↔ b₁ ⩿ b₂ ∧ b₁ < b₂
simp_rw₁ : b₁ ⩿ b₂ ∧ (a, b₁) < (a, b₂) ↔ b₁ ⩿ b₂ ∧ b₁ < b₂
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂

Tactic:
simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]

Premises used: Prod.mk_wcovBy_mk_iff_right, Prod.mk_lt_mk_iff_right, covBy_iff_wcovBy_and_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
refine_1 : ∀ (h : (a₁, b₁) ⩿ (a₂, b₂)), a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
refine_2 : a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₂, b₂)
⊢ a₁ = a₂ ∨ b₁ = b₂

Tactic:
fst_eq_or_snd_eq_of_wcovBy h

Premises used: Prod.fst_eq_or_snd_eq_of_wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₂, b₂)
refine_1 : ∀ (h : (a₁, b₁) ⩿ (a₁, b₂)), a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁
refine_1₁ : ∀ (h : (a₁, b₁) ⩿ (a₂, b₁)), a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h

Premises used: Prod.fst_eq_or_snd_eq_of_wcovBy, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₁, b₂)
⊢ a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁

Tactic:
Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩

Premises used: Prod.mk_wcovBy_mk_iff_right, And.intro, Iff.mp, Or.inr, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₁, b₂)
⊢ a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁

Tactic:
exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⩿ (a₂, b₁)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂

Tactic:
Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩

Premises used: And.intro, Iff.mp, Or.inl, Prod.mk_wcovBy_mk_iff_left, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⩿ (a₂, b₁)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂

Tactic:
exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)

Tactic:
mk_wcovBy_mk_iff_left.2 h

Premises used: Iff.mpr, Prod.mk_wcovBy_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)

Tactic:
exact mk_wcovBy_mk_iff_left.2 h

Premises used: Iff.mpr, Prod.mk_wcovBy_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Tactic:
mk_wcovBy_mk_iff_right.2 h

Premises used: Iff.mpr, Prod.mk_wcovBy_mk_iff_right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Tactic:
exact mk_wcovBy_mk_iff_right.2 h

Premises used: Iff.mpr, Prod.mk_wcovBy_mk_iff_right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
refine_1 : ∀ (h : (a₁, b₁) ⋖ (a₂, b₂)), a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
refine_2 : a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ = a₂ ∨ b₁ = b₂

Tactic:
fst_eq_or_snd_eq_of_wcovBy h.wcovBy

Premises used: CovBy.wcovBy, Prod.fst_eq_or_snd_eq_of_wcovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
refine_1 : ∀ (h : (a₁, b₁) ⋖ (a₁, b₂)), a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁
refine_1₁ : ∀ (h : (a₁, b₁) ⋖ (a₂, b₁)), a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h.wcovBy

Premises used: CovBy.wcovBy, Prod.fst_eq_or_snd_eq_of_wcovBy, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁

Tactic:
Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩

Premises used: Prod.mk_covBy_mk_iff_right, And.intro, Iff.mp, Or.inr, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁

Tactic:
exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂

Tactic:
Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

Premises used: Prod.mk_covBy_mk_iff_left, And.intro, Iff.mp, Or.inl, rfl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂

Tactic:
exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)

Tactic:
mk_covBy_mk_iff_left.2 h

Premises used: Iff.mpr, Prod.mk_covBy_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)

Tactic:
exact mk_covBy_mk_iff_left.2 h

Premises used: Iff.mpr, Prod.mk_covBy_mk_iff_left
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)

Tactic:
mk_covBy_mk_iff_right.2 h

Premises used: Iff.mpr, Prod.mk_covBy_mk_iff_right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)

Tactic:
exact mk_covBy_mk_iff_right.2 h

Premises used: Iff.mpr, Prod.mk_covBy_mk_iff_right
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
mk :
  ∀ (fst : α) (snd : β),
    (fst, snd) ⩿ y ↔ (fst, snd).1 ⩿ y.1 ∧ (fst, snd).2 = y.2 ∨ (fst, snd).2 ⩿ y.2 ∧ (fst, snd).1 = y.1
⊢ x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1

Tactic:
cases x
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
y : α × β
fst : α
snd : β
mk :
  ∀ (fst_1 : α) (snd_1 : β),
    (fst, snd) ⩿ (fst_1, snd_1) ↔
      (fst, snd).1 ⩿ (fst_1, snd_1).1 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
        (fst, snd).2 ⩿ (fst_1, snd_1).2 ∧ (fst, snd).1 = (fst_1, snd_1).1
⊢ (fst, snd) ⩿ y ↔ (fst, snd).1 ⩿ y.1 ∧ (fst, snd).2 = y.2 ∨ (fst, snd).2 ⩿ y.2 ∧ (fst, snd).1 = y.1

Tactic:
cases y
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
fst : α
snd : β
fst_1 : α
snd_1 : β
⊢ (fst, snd) ⩿ (fst_1, snd_1) ↔
    (fst, snd).1 ⩿ (fst_1, snd_1).1 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
      (fst, snd).2 ⩿ (fst_1, snd_1).2 ∧ (fst, snd).1 = (fst_1, snd_1).1

Tactic:
mk_wcovBy_mk_iff

Premises used: Prod.mk_wcovBy_mk_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
fst : α
snd : β
fst_1 : α
snd_1 : β
⊢ (fst, snd) ⩿ (fst_1, snd_1) ↔
    (fst, snd).1 ⩿ (fst_1, snd_1).1 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
      (fst, snd).2 ⩿ (fst_1, snd_1).2 ∧ (fst, snd).1 = (fst_1, snd_1).1

Tactic:
exact mk_wcovBy_mk_iff

Premises used: Prod.mk_wcovBy_mk_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
mk :
  ∀ (fst : α) (snd : β),
    (fst, snd) ⋖ y ↔ (fst, snd).1 ⋖ y.1 ∧ (fst, snd).2 = y.2 ∨ (fst, snd).2 ⋖ y.2 ∧ (fst, snd).1 = y.1
⊢ x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1

Tactic:
cases x
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
y : α × β
fst : α
snd : β
mk :
  ∀ (fst_1 : α) (snd_1 : β),
    (fst, snd) ⋖ (fst_1, snd_1) ↔
      (fst, snd).1 ⋖ (fst_1, snd_1).1 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
        (fst, snd).2 ⋖ (fst_1, snd_1).2 ∧ (fst, snd).1 = (fst_1, snd_1).1
⊢ (fst, snd) ⋖ y ↔ (fst, snd).1 ⋖ y.1 ∧ (fst, snd).2 = y.2 ∨ (fst, snd).2 ⋖ y.2 ∧ (fst, snd).1 = y.1

Tactic:
cases y
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
fst : α
snd : β
fst_1 : α
snd_1 : β
⊢ (fst, snd) ⋖ (fst_1, snd_1) ↔
    (fst, snd).1 ⋖ (fst_1, snd_1).1 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
      (fst, snd).2 ⋖ (fst_1, snd_1).2 ∧ (fst, snd).1 = (fst_1, snd_1).1

Tactic:
mk_covBy_mk_iff

Premises used: Prod.mk_covBy_mk_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
fst : α
snd : β
fst_1 : α
snd_1 : β
⊢ (fst, snd) ⋖ (fst_1, snd_1) ↔
    (fst, snd).1 ⋖ (fst_1, snd_1).1 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
      (fst, snd).2 ⋖ (fst_1, snd_1).2 ∧ (fst, snd).1 = (fst_1, snd_1).1

Tactic:
exact mk_covBy_mk_iff

Premises used: Prod.mk_covBy_mk_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
⊢ a i ⩿ b i

Tactic:
⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩

Premises used: And.left, And.intro, WCovBy
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
refine : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i), False
⊢ a i ⩿ b i

Tactic:
refine ⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ Function.update (β := α) a i ci ≤ b

Tactic:
simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j

Premises used: LT.lt.le, And.left, update_le_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ Function.update (β := α) a i ci ≤ b

Tactic:
have hcb : Function.update a i ci ≤ b := by simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update (β := α) a i ci ≤ b
⊢ a < Function.update (β := α) a i ci

Tactic:
simpa
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update (β := α) a i ci ≤ b
refine : ¬b ≤ Function.update (β := α) a i ci
⊢ False

Tactic:
refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)

Premises used: And.right, lt_of_le_not_ge
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update (β := α) a i ci ≤ b
⊢ ¬b ≤ Function.update (β := α) a i ci

Tactic:
simp [le_update_iff, h₂.not_ge]

Premises used: le_update_iff, LT.lt.not_ge
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
refine : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i), False
refine₁ : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i) (hcb : Function.update (β := α) a i ci ≤ b), False
refine₂ :
  ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i) (hcb : Function.update (β := α) a i ci ≤ b),
    ¬b ≤ Function.update (β := α) a i ci
⊢ a i ⩿ b i

Tactic:
classical
  refine ⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩
  have hcb : Function.update a i ci ≤ b := by simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j
  refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)
  simp [le_update_iff, h₂.not_ge]

Premises used: le_update_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
    ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x

Tactic:
simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h

Premises used: and_imp, Pi.lt_def, CovBy, forall_exists_index, not_exists, not_and
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h :
  (a ≤ b ∧ ∃ (i : ι), a i < b i) ∧
    ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
obtain :
  ∀ (h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x) (hab : a ≤ b) (i : ι)
    (hi : a i < b i), ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
⟨i, fun j hj ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
refine : ∀ (j : ι) (hj : j ≠ i), AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) ↦ x1 ≤ x2) (a j) (b j)

Tactic:
refine ⟨i, fun j hj ↦ ?_⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
⊢ c ≤ b

Tactic:
simpa [update_le_iff, c] using fun k hk ↦ hab k

Premises used: update_le_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
⊢ c ≤ b

Tactic:
have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
h₁ : c ≤ b
⊢ a ≤ c

Tactic:
simp [c, hi.le]

Premises used: LT.lt.le
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
h₁ : c ≤ b
⊢ a i < c i

Tactic:
simpa [c]
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι) (h : a x < c x), c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update (β := α) a i (b i)
h₁ : c ≤ b
⊢ ¬c j < b j

Tactic:
have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j