awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
have inr : ∀ (h3 : c = b), c = a ∨ c = b
Tactic: rcases h3.eq_or_lt with (h3 | h3)
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ c = a ∨ c = b
have inr₁ : ∀ (h3 : c < b), c = a ∨ c = b
Tactic: rcases h3.eq_or_lt with (h3 | h3)
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
have refine : c = a ∨ c = b → a ≤ c ∧ c ≤ b
Tactic: refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b = {a, b}
have h₁ : ∀ (c : α), c ∈ Icc a b ↔ Membership.mem (γ := Set α) {a, b} c
Tactic: ext c
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ico a b ⊆ {a}
have rw : Icc a b \ {b} ⊆ {a}
Tactic: rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
rw : Icc a b \ {b} ⊆ {a}
⊢ Ico a b ⊆ {a}
have rw₁ : Subset (α := Set α) ({a, b} \ {b}) {a}
Tactic: rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
rw : Icc a b \ {b} ⊆ {a}
rw₁ : Subset (α := Set α) ({a, b} \ {b}) {a}
⊢ Ico a b ⊆ {a}
have rw₂ : Subset (α := Set α) {a, b} {b, a}
Tactic: rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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}
⊢ Ico a b ⊆ {a}
have rw₃ : Subset (α := Set α) {b, a} {b, a}
Tactic: rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ioc a b ⊆ {b}
have rw : Icc a b \ {a} ⊆ {b}
Tactic: rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
rw : Icc a b \ {a} ⊆ {b}
⊢ Ioc a b ⊆ {b}
have rw₁ : Subset (α := Set α) ({a, b} \ {a}) {b}
Tactic: rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⩿ b
rw : Icc a b \ {a} ⊆ {b}
rw₁ : Subset (α := Set α) ({a, b} \ {a}) {b}
⊢ Ioc a b ⊆ {b}
have rw₂ : Subset (α := Set α) {a, b} {a, b}
Tactic: rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LT α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw : ¬(a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ ¬a ⋖ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₁ : ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ ¬a ⋖ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₂ : (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ ¬a ⋖ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₃ : (∃ (x : α) (_ : a < x), ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ ¬a ⋖ b ↔ ∃ (c : α), a < c ∧ c < b
have simp_rw₄ : (∃ (x : α), a < x ∧ ¬¬x < b) ↔ ∃ (c : α), a < c ∧ c < b
Tactic: simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b
have rw : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
Tactic: rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b
have rw₁ : a ⋖ b ∨ a ≤ b ∧ b ≤ a ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
Tactic: rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⋖ b
⊢ Ico a b = {a}
have rw : Ioo a b ∪ {a} = {a}
Tactic: rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⋖ b
rw : Ioo a b ∪ {a} = {a}
⊢ Ico a b = {a}
have rw₁ : Eq (α := Set α) (∅ ∪ {a}) {a}
Tactic: rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ⋖ b
rw : Ioo a b ∪ {a} = {a}
rw₁ : Eq (α := Set α) (∅ ∪ {a}) {a}
⊢ Ico a b = {a}
have rw₂ : Eq (α := Set α) {a} {a}
Tactic: rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ioi a = Ici b
have rw : Ioo a b ∪ Ici b = Ici b
Tactic: rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
rw : Ioo a b ∪ Ici b = Ici b
⊢ Ioi a = Ici b
have rw₁ : ∅ ∪ Ici b = Ici b
Tactic: rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
rw : Ioo a b ∪ Ici b = Ici b
rw₁ : ∅ ∪ Ici b = Ici b
⊢ Ioi a = Ici b
have rw₂ : Ici b = Ici b
Tactic: rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iio b = Iic a
have rw : Iic a ∪ Ioo a b = Iic a
Tactic: rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
rw : Iic a ∪ Ioo a b = Iic a
⊢ Iio b = Iic a
have rw₁ : Iic a ∪ ∅ = Iic a
Tactic: rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ⋖ b
rw : Iic a ∪ Ioo a b = Iic a
rw₁ : Iic a ∪ ∅ = Iic a
⊢ Iio b = Iic a
have rw₂ : Iic a = Iic a
Tactic: rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y
have simp_rw : (∀ {z : α}, z < y ↔ z ≤ x) ↔ ∀ {z : α}, z ≤ x ↔ z < y
Tactic: simp_rw [covBy_iff_lt_iff_le_left, iff_comm]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
x : α
s : Set α
⊢ s ⩿ insert x s
have refine : ∀ (t : Set α) (hst : s ≤ t) (h2t : t ≤ insert x s), t = s ∨ t = insert x s
Tactic: refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
⊢ t = s ∨ t = insert x s
have pos : ∀ (h : x ∈ t), t = s ∨ t = insert x s
Tactic: by_cases h : x ∈ t
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ t = s ∨ t = insert x s
have neg : ∀ (h : x ∉ t), t = s ∨ t = insert x s
Tactic: by_cases h : x ∈ t
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
have neg : t ⊆ s
Tactic: refine Or.inl (subset_antisymm ?_ hst)
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
⊢ t ⊆ s
have neg : t \ {x} ⊆ s
Tactic: rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
neg : t \ {x} ⊆ s
⊢ t ⊆ s
have neg₁ : t ⊆ insert x s
Tactic: rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⩿ s
have pos : ∀ (ha : a ∈ s), s \ {a} ⩿ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
s : Set α
a : α
pos : ∀ (ha : a ∈ s), s \ {a} ⩿ s
⊢ s \ {a} ⩿ s
have neg : ∀ (ha : a ∉ s), s \ {a} ⩿ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⩿ s
have h : s = insert a (s \ {a})
Tactic: convert! wcovBy_insert a _
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s = insert a (s \ {a})
have h : ∀ (x : α), x ∈ s ↔ x ∈ insert a (s \ {a})
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ⩿ x2) (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
have h : ∀ (x y : α), x ⩿ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
x y : α
⊢ x ⩿ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have h : 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]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
x y : α
h : x = y ∨ x ⋖ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ x ⩿ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
have h₁ : y = x ∨ x ⋖ y ↔ ReflGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
Tactic: simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (TransGen fun (x1 x2 : α) ↦ x1 ⩿ x2) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
have rw : Eq.{u_1 + 1} (α := α → α → Prop) (TransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2)) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
Tactic: rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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)
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (TransGen fun (x1 x2 : α) ↦ x1 ⩿ x2) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
have rw₁ : Eq.{u_1 + 1} (α := α → α → Prop) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
Tactic: rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq.{u_1 + 1} (α := (a : α) → α → Prop) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⩿ x2)
    (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
have rw : Eq.{u_1 + 1} (α := (a : α) → α → Prop) (ReflTransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2))
  (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
Tactic: rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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)
⊢ Eq.{u_1 + 1} (α := (a : α) → α → Prop) (ReflTransGen fun (x1 x2 : α) ↦ x1 ⩿ x2)
    (ReflTransGen fun (x1 x2 : α) ↦ x1 ⋖ x2)
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
h : x ⩿ y
⊢ x.1 = y.1 ∨ x.2 = y.2
have by_contra! : ∀ (ha : x.1 ≠ y.1) (hb : x.2 ≠ y.2), False
Tactic: by_contra! ⟨ha, hb⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
have refine : ∀ (h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂) (c : α × β) (h₁ : (a₁, b) < c) (h₂ : c < (a₂, b)), False
Tactic: refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
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)
⊢ False
have this : c.2 = b
Tactic: have : c.2 = b := h₂.le.2.antisymm h₁.le.2
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
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
⊢ False
have h₃ : a₁ < c.1
Tactic: rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂
Cleared hypotheses: h₁, h₂, this
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
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
⊢ False
have h₄ : c.1 < a₂
Tactic: rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂
Cleared hypotheses: h₁, h₂, this
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
have simp_rw : (a₁, b) ⩿ (a₂, b) ∧ (a₁, b) < (a₂, b) ↔ a₁ ⩿ a₂ ∧ a₁ < a₂
Tactic: simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
have simp_rw₁ : a₁ ⩿ a₂ ∧ (a₁, b) < (a₂, b) ↔ a₁ ⩿ a₂ ∧ a₁ < a₂
Tactic: simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
have simp_rw : (a, b₁) ⩿ (a, b₂) ∧ (a, b₁) < (a, b₂) ↔ b₁ ⩿ b₂ ∧ b₁ < b₂
Tactic: simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
have simp_rw₁ : b₁ ⩿ b₂ ∧ (a, b₁) < (a, b₂) ↔ b₁ ⩿ b₂ ∧ b₁ < b₂
Tactic: simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂
have refine_1 : ∀ (h : (a₁, b₁) ⩿ (a₂, b₂)), a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
have refine_2 : a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
have refine_1 : ∀ (h : (a₁, b₁) ⩿ (a₁, b₂)), a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁
Tactic: obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h
Cleared hypotheses: a₂, h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₁
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
have refine_1₁ : ∀ (h : (a₁, b₁) ⩿ (a₂, b₁)), a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂
Tactic: obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h
Cleared hypotheses: b₂, h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂
have refine_1 : ∀ (h : (a₁, b₁) ⋖ (a₂, b₂)), a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
have refine_2 : a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
have refine_1 : ∀ (h : (a₁, b₁) ⋖ (a₁, b₂)), 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
Cleared hypotheses: a₂, h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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₁
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
have refine_1₁ : ∀ (h : (a₁, b₁) ⋖ (a₂, b₁)), 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
Cleared hypotheses: b₂, h
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
⊢ x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1
have 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
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
y : α × β
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
have 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
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
x y : α × β
⊢ x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1
have 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
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
y : α × β
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
have 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
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
⊢ a i ⩿ b i
have refine : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i), False
Tactic: refine ⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
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
⊢ False
have hcb : 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
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ False
have refine : ¬b ≤ Function.update (β := α) a i ci
Tactic: refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
⊢ a i ⩿ b i
have refine : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i), False
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]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
have refine₁ : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i) (hcb : Function.update (β := α) a i ci ≤ b), False
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]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ a i ⩿ b i
have refine₂ : ∀ (ci : α i) (h₁ : a i < ci) (h₂ : ci < b i) (hcb : Function.update (β := α) a i ci ≤ b),
  ¬b ≤ Function.update (β := α) a i ci
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]