awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
neg : f (succ i) \ (Iic i).sup f ⊔ f i = f (succ i)
neg₁ : f (succ i) \ (Iic i).sup' ⋯ f ⊔ f i = f (succ i)
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
have neg₂ : f (succ i) \ (partialSups f : (a : ι) → α) i ⊔ f i = f (succ i)
Tactic: rw [this, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, hf.partialSups_eq,
      sdiff_sup_cancel <| hf <| le_succ i]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
neg : f (succ i) \ (Iic i).sup f ⊔ f i = f (succ i)
neg₁ : f (succ i) \ (Iic i).sup' ⋯ f ⊔ f i = f (succ i)
neg₂ : f (succ i) \ (partialSups f : (a : ι) → α) i ⊔ f i = f (succ i)
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
have neg₃ : f (succ i) \ f i ⊔ f i = f (succ i)
Tactic: rw [this, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, hf.partialSups_eq,
      sdiff_sup_cancel <| hf <| le_succ i]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
neg : f (succ i) \ (Iic i).sup f ⊔ f i = f (succ i)
neg₁ : f (succ i) \ (Iic i).sup' ⋯ f ⊔ f i = f (succ i)
neg₂ : f (succ i) \ (partialSups f : (a : ι) → α) i ⊔ f i = f (succ i)
neg₃ : f (succ i) \ f i ⊔ f i = f (succ i)
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
have neg₄ : f (succ i) = f (succ i)
Tactic: rw [this, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, hf.partialSups_eq,
      sdiff_sup_cancel <| hf <| le_succ i]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m_1 n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
have pos : ∀ (h'm : IsMax m), (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
Tactic: by_cases h'm : IsMax m
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m_1 n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
pos : ∀ (h'm : IsMax m), (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
have neg : ∀ (h'm : ¬IsMax m), (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
Tactic: by_cases h'm : IsMax m
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m_1 n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
have neg : (insert (succ m) (Ioc n m)).sup (disjointed f) = f (succ m) \ f n
Tactic: rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m_1 n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (insert (succ m) (Ioc n m)).sup (disjointed f) = f (succ m) \ f n
have neg : f (succ m) \ f m ⊔ f m \ f n = f (succ m) \ f n
Tactic: simp only [sup_insert, hf.disjointed_succ h'm, ih]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
⊢ (Ioc n m).sup (disjointed f) = f m \ f n
have rfl : (Ioc n n).sup (disjointed f) = f n \ f n
Tactic: induction hm using Succ.rec with
  | rfl => simp
  | succ m hm ih =>
    by_cases h'm : IsMax m
    · simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih
    · rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
      simp only [sup_insert, hf.disjointed_succ h'm, ih]
      exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
rfl : (Ioc n n).sup (disjointed f) = f n \ f n
⊢ (Ioc n m).sup (disjointed f) = f m \ f n
have succ : ∀ (m : ι) (hm : n ≤ m) (ih : (Ioc n m).sup (disjointed f) = f m \ f n),
  (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n
Tactic: induction hm using Succ.rec with
  | rfl => simp
  | succ m hm ih =>
    by_cases h'm : IsMax m
    · simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih
    · rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
      simp only [sup_insert, hf.disjointed_succ h'm, ih]
      exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
have inl : ∀ (hι : IsEmpty ι), ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
inl : ∀ (hι : IsEmpty ι), ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
have inr : ∀ (hι : Nonempty ι), ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ (⇑R.symm : (a : Fin (card ι)) → ι)
⊢ f = f' ∘ (⇑R : (a : ι) → Fin (card ι))
have h : ∀ (x : ι), f x = (f' ∘ (⇑R : (a : ι) → Fin (card ι))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Disjointed (hypothesis)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ (⇑R.symm : (a : Fin (card ι)) → ι)
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
have hf' : f = f' ∘ (⇑R : (a : ι) → Fin (card ι))
Tactic: have hf' : f = f' ∘ R := by ext; simp only [Function.comp_apply, Equiv.symm_apply_apply, f']
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ (⇑R.symm : (a : Fin (card ι)) → ι)
hf' : f = f' ∘ (⇑R : (a : ι) → Fin (card ι))
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
have inr : disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)) ≤ f
Tactic: refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ (⇑R.symm : (a : Fin (card ι)) → ι)
hf' : f = f' ∘ (⇑R : (a : ι) → Fin (card ι))
inr : disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)) ≤ f
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
have inr₁ : sup (β := ι) univ (disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι))) = sup univ f
Tactic: refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ (⇑R.symm : (a : Fin (card ι)) → ι)
hf' : f = f' ∘ (⇑R : (a : ι) → Fin (card ι))
inr : disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)) ≤ f
inr₁ : sup (β := ι) univ (disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι))) = sup univ f
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
have inr₂ : Pairwise (α := ι) (Disjoint on disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)))
Tactic: refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ (n : ℕ), x ∈ s n
inst : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
⊢ Set.preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := fun (n : ℕ) ↦ x ∈ s n) ⋯) {n} = disjointed s n
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (Set.preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := fun (n : ℕ) ↦ x ∈ s n) sorry) {n}) x ↔
    x ∈ disjointed s n
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have this : IsPreorder α s
Tactic: haveI := (hc₁ hs).1
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have refine : sSup c ∈ S
Tactic: refine ⟨sSup c, ?_, fun z hz => le_sSup hz⟩
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ sSup c ∈ S
have refine_1 : ∀ (a : α), sSup c a a
Tactic: refine
        { refl := ?_
          trans := ?_
          antisymm := ?_ }
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
refine_1 : ∀ (a : α), sSup c a a
⊢ sSup c ∈ S
have refine_2 : ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1
Tactic: refine
        { refl := ?_
          trans := ?_
          antisymm := ?_ }
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
refine_1 : ∀ (a : α), sSup c a a
refine_2 : ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1
⊢ sSup c ∈ S
have refine_3 : ∀ (a b : α), sSup c a b → sSup c b a → a = b
Tactic: refine
        { refl := ?_
          trans := ?_
          antisymm := ?_ }
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), sSup c a a
have refine_1 : ∀ (a : α), ∃ r ∈ c, r a a
Tactic: simp_rw [binary_relation_sSup_iff]
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1
have refine_2 : ∀ (a b c_1 : α), (∃ r ∈ c, r a b) → (∃ r ∈ c, r b c_1) → ∃ r ∈ c, r a c_1
Tactic: simp_rw [binary_relation_sSup_iff]
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), sSup c a b → sSup c b a → a = b
have refine_3 : ∀ (a b : α), (∃ r ∈ c, r a b) → (∃ r ∈ c, r b a) → a = b
Tactic: simp_rw [binary_relation_sSup_iff]
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
⊢ ∃ r ∈ c, r x z
have this₁ : IsPartialOrder α s₁
Tactic: haveI : IsPartialOrder _ _ := hc₁ h₁s₁
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this : IsPartialOrder α s₁
⊢ ∃ r ∈ c, r x z
have this₁ : IsPartialOrder α s₂
Tactic: haveI : IsPartialOrder _ _ := hc₁ h₁s₂
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this_2 : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ ∃ r ∈ c, r x z
have refine_2 : ∀ (h : s₁ ≤ s₂), ∃ r ∈ c, r x z
Tactic: rcases hc₂.total h₁s₁ h₁s₂ with h | h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this_2 : IsPartialOrder α s₁
this : IsPartialOrder α s₂
refine_2 : ∀ (h : s₁ ≤ s₂), ∃ r ∈ c, r x z
⊢ ∃ r ∈ c, r x z
have refine_2₁ : ∀ (h : s₂ ≤ s₁), ∃ r ∈ c, r x z
Tactic: rcases hc₂.total h₁s₁ h₁s₂ with h | h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y
have this₁ : IsPartialOrder α s₁
Tactic: haveI : IsPartialOrder _ _ := hc₁ h₁s₁
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y
have this₁ : IsPartialOrder α s₂
Tactic: haveI : IsPartialOrder _ _ := hc₁ h₁s₂
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this_2 : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ x = y
have refine_3 : ∀ (h : s₁ ≤ s₂), x = y
Tactic: rcases hc₂.total h₁s₁ h₁s₂ with h | h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this_1 : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this_2 : IsPartialOrder α s₁
this : IsPartialOrder α s₂
refine_3 : ∀ (h : s₁ ≤ s₂), x = y
⊢ x = y
have refine_3₁ : ∀ (h : s₂ ≤ s₁), x = y
Tactic: rcases hc₂.total h₁s₁ h₁s₂ with h | h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s
have hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Tactic: have hS : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub := by
    rintro c hc₁ hc₂ s hs
    haveI := (hc₁ hs).1
    refine ⟨sSup c, ?_, fun z hz => le_sSup hz⟩
    refine
        { refl := ?_
          trans := ?_
          antisymm := ?_ } <;>
      simp_rw [binary_relation_sSup_iff]
    · intro x
      exact ⟨s, hs, refl x⟩
    · rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
      haveI : IsPartialOrder _ _ := hc₁ h₁s₁
      haveI : IsPartialOrder _ _ := hc₁ h₁s₂
      rcases hc₂.total h₁s₁ h₁s₂ with h | h
      · exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩
      · exact ⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩
    · rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
      haveI : IsPartialOrder _ _ := hc₁ h₁s₁
      haveI : IsPartialOrder _ _ := hc₁ h₁s₂
      rcases hc₂.total h₁s₁ h₁s₂ with h | h
      · exact antisymm (h _ _ h₂s₁) h₂s₂
      · apply antisymm h₂s₁ (h _ _ h₂s₂)
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s
have obtain : ∀ (s : α → α → Prop) (hrs : r ≤ s) (hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s),
  ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s
Tactic: obtain ⟨s, hrs, hs⟩ := zorn_le_nonempty₀ S hS r ‹_›
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (hypothesis)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s
have this : IsPartialOrder α s
Tactic: haveI : IsPartialOrder α s := hs.prop
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
⊢ ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s
have refine : ∀ (a b : α), s a b ∨ s b a
Tactic: refine ⟨s,
    { total := ?_, refl := hs.1.refl, trans := hs.1.trans, antisymm := hs.1.antisymm }, hrs⟩
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
⊢ s x y ∨ s y x
have by_contra! : ∀ (h : ¬s x y ∧ ¬s y x), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ False
have rw : ∀ (h : ¬s' x y ∧ ¬s' y x), False
Tactic: rw [hs.eq_of_le (y := s') ?_ fun _ _ ↦ Or.inl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
rw : ∀ (h : ¬s' x y ∧ ¬s' y x), False
⊢ False
have rw₁ : s' ∈ S
Tactic: rw [hs.eq_of_le (y := s') ?_ fun _ _ ↦ Or.inl] at h
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
have refine_1 : ∀ (a b c : α), s' a b → s' b c → s' a c
Tactic: refine
    { refl := fun x ↦ Or.inl (refl _)
      trans := ?_
      antisymm := ?_ }
-- Lean 4 proof step from Mathlib.Order.Extension.Linear (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsPartialOrder α r
S : Set (α → α → Prop) := {s : α → α → Prop | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun (x1 x2 : α → α → Prop) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun (x : α → α → Prop) ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : (x' y' : α) → Prop := fun (x' y' : α) ↦ s x' y' ∨ s x' x ∧ s y y'
refine_1 : ∀ (a b c : α), s' a b → s' b c → s' a c
⊢ s' ∈ S
have refine_2 : ∀ (a b : α), s' a b → s' b a → a = b
Tactic: refine
    { refl := fun x ↦ Or.inl (refl _)
      trans := ?_
      antisymm := ?_ }