awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Disjointed
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)
neg₄ neg₅ : f (succ i) = f (succ i)
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ 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]

Premises used: partialSups_apply, sdiff_sup_cancel, Monotone.partialSups_eq, Order.le_succ, Finset.sup'_eq_sup, Finset.nonempty_Iic
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
⊢ (Ioc n n).sup (disjointed f) = f n \ f n

Tactic:
simp
-- Module: Mathlib.Order.Disjointed
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
neg : ∀ (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

Tactic:
by_cases h'm : IsMax m

Premises used: IsMax
-- Module: Mathlib.Order.Disjointed
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

Tactic:
simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih

Premises used: Iff.mpr, Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.Disjointed
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
neg : (insert (succ m) (Ioc n m)).sup (disjointed f) = f (succ m) \ f n
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]

Premises used: Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
-- Module: Mathlib.Order.Disjointed
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
neg : f (succ m) \ f m ⊔ f m \ f n = f (succ m) \ f n
⊢ (insert (succ m) (Ioc n m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
simp only [sup_insert, hf.disjointed_succ h'm, ih]

Premises used: Finset.sup_insert, Monotone.disjointed_succ
-- Module: Mathlib.Order.Disjointed
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
⊢ f (succ m) \ f m ⊔ f m \ f n = f (succ m) \ f n

Tactic:
sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

Premises used: sdiff_sup_sdiff_cancel, Order.le_succ
-- Module: Mathlib.Order.Disjointed
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
⊢ f (succ m) \ f m ⊔ f m \ f n = f (succ m) \ f n

Tactic:
exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

Premises used: sdiff_sup_sdiff_cancel, Order.le_succ
-- Module: Mathlib.Order.Disjointed
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
succ :
  ∀ (m : ι) (hm : n ≤ m) (ih : (Ioc n m).sup (disjointed f) = f m \ f n),
    (Ioc n (Order.succ m)).sup (disjointed f) = f (Order.succ m) \ f n
⊢ (Ioc n m).sup (disjointed f) = f 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)

Premises used: Order.succ, Finset.sup_insert, sdiff_sup_sdiff_cancel, Order.le_succ, rfl, IsMax
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_3
ι : Type u_4
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : OrderBot ι
f : ι → Set α
hf : Monotone f
m n : ι
hm : n ≤ m
⊢ ⋃ i ∈ Ioc n m, disjointed f i = f m \ f n

Tactic:
simp [← sup_Ioc_disjointed_of_monotone hf hm]

Premises used: sup_Ioc_disjointed_of_monotone
-- Module: Mathlib.Order.Disjointed
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)
inr : ∀ (hι : Nonempty ι), ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : IsEmpty ι
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)

Tactic:
⟨f, le_rfl, rfl, Subsingleton.pairwise⟩

Premises used: le_rfl, And.intro, Exists.intro, rfl, Subsingleton.pairwise
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
ι : Type u_3
inst_1 : Fintype ι
f : ι → α
hι : IsEmpty ι
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)

Tactic:
exact ⟨f, le_rfl, rfl, Subsingleton.pairwise⟩
-- Module: Mathlib.Order.Disjointed
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 ι)) → ι)
h : ∀ (x : ι), f x = (f' ∘ (⇑R : (a : ι) → Fin (card ι))) x
⊢ f = f' ∘ (⇑R : (a : ι) → Fin (card ι))

Tactic:
ext
-- Module: Mathlib.Order.Disjointed
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 ι)) → ι)
x : ι
⊢ f x = (f' ∘ (⇑R : (a : ι) → Fin (card ι))) x

Tactic:
simp only [Function.comp_apply, Equiv.symm_apply_apply, f']

Premises used: Equiv.symm_apply_apply, Function.comp_apply
-- Module: Mathlib.Order.Disjointed
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 ι))

Tactic:
have hf' : f = f' ∘ R := by ext; simp only [Function.comp_apply, Equiv.symm_apply_apply, f']
-- Module: Mathlib.Order.Disjointed
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)

Tactic:
⟨disjointed f' ∘ R, ?_, ?_, ?_⟩

Premises used: disjointed, Function.comp, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Order.Disjointed
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
inr₂ : Pairwise (α := ι) (Disjoint on disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)))
⊢ ∃ g ≤ f, sup univ g = sup univ f ∧ Pairwise (Disjoint on g)

Tactic:
refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
-- Module: Mathlib.Order.Disjointed
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 ι))
n : ι
⊢ (disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι))) n ≤ f n

Tactic:
simpa only [hf'] using disjointed_le f' (R n)

Premises used: disjointed_le, DFunLike.coe
-- Module: Mathlib.Order.Disjointed
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 ι))
⊢ sup (β := ι) univ (disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι))) = sup univ f

Tactic:
simpa only [← sup_image, image_univ_equiv, hf'] using sup_disjointed f'

Premises used: Finset.image_univ_equiv, Fintype.sup_disjointed, Finset.sup_image
-- Module: Mathlib.Order.Disjointed
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 ι))
⊢ Pairwise (α := ι) (Disjoint on disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)))

Tactic:
fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)

Premises used: disjointed, Function.Injective.ne, Pairwise, disjoint_disjointed, Equiv.injective
-- Module: Mathlib.Order.Disjointed
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 ι))
⊢ Pairwise (α := ι) (Disjoint on disjointed f' ∘ (⇑R : (a : ι) → Fin (card ι)))

Tactic:
exact fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)

Premises used: Function.Injective.ne, disjoint_disjointed, Equiv.injective
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : CompleteBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), disjointed f i) (⨆ (i : ι), f i)

Tactic:
iSup_eq_iSup_of_partialSups_eq_partialSups (partialSups_disjointed f)

Premises used: partialSups_disjointed, iSup_eq_iSup_of_partialSups_eq_partialSups
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : CompleteBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed f i = f i ⊓ ⨅ (j : ι), ⨅ (_ : j < i), (f j)ᶜ

Tactic:
simp only [disjointed_apply, Finset.sup_eq_iSup, mem_Iio, sdiff_eq, compl_iSup]

Premises used: sdiff_eq, compl_iSup, Finset.sup_eq_iSup, disjointed_apply, Finset.mem_Iio
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
f : ι → Set α
i : ι
⊢ disjointed f i ⊆ f i

Tactic:
disjointed_le f i

Premises used: disjointed_le
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : PartialOrder ι
inst_1 : LocallyFiniteOrderBot ι
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), disjointed f i) (⋃ (i : ι), f i)

Tactic:
iSup_disjointed f

Premises used: iSup_disjointed, Set.iUnion
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
f : ι → Set α
i : ι
⊢ disjointed f i = f i ∩ ⋂ (j : ι), ⋂ (_ : j < i), (f j)ᶜ

Tactic:
disjointed_eq_inf_compl f i

Premises used: Set.iInter, disjointed_eq_inf_compl
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ (n : ℕ), x ∈ s n
inst : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (Set.preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := fun (n : ℕ) ↦ x ∈ s n) ⋯) {n}) x ↔
      x ∈ disjointed s n
⊢ Set.preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := fun (n : ℕ) ↦ x ∈ s n) ⋯) {n} = disjointed s n

Tactic:
ext x
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ (n : ℕ), x ∈ s n
inst : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
x : α
⊢ Membership.mem (γ := Set α) (Set.preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := fun (n : ℕ) ↦ x ∈ s n) ⋯) {n}) x ↔
    x ∈ disjointed s n

Tactic:
simp [Nat.find_eq_iff, disjointed_eq_inter_compl]

Premises used: disjointed_eq_inter_compl, Nat.find_eq_iff
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ disjointed f 0 = f 0

Tactic:
disjointed_bot f

Premises used: disjointed_bot
-- Module: Mathlib.Order.Extension.Linear
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
⊢ IsPreorder α s

Tactic:
haveI := (hc₁ hs).1
-- Module: Mathlib.Order.Extension.Linear
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

Tactic:
⟨sSup c, ?_, fun z hz => le_sSup hz⟩

Premises used: And.intro, Exists.intro, le_sSup, SupSet.sSup
-- Module: Mathlib.Order.Extension.Linear
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 : sSup c ∈ S
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
refine ⟨sSup c, ?_, fun z hz => le_sSup hz⟩
-- Module: Mathlib.Order.Extension.Linear
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

Tactic:
{ refl := ?_
          trans := ?_
          antisymm := ?_ }

Premises used: Set.Mem, setOf, IsPartialOrder.mk
-- Module: Mathlib.Order.Extension.Linear
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
refine_3 : ∀ (a b : α), sSup c a b → sSup c b a → a = b
⊢ sSup c ∈ S

Tactic:
refine
        { refl := ?_
          trans := ?_
          antisymm := ?_ }
-- Module: Mathlib.Order.Extension.Linear
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 : α), ∃ r ∈ c, r a a
⊢ ∀ (a : α), sSup c a a

Tactic:
simp_rw [binary_relation_sSup_iff]

Premises used: binary_relation_sSup_iff
-- Module: Mathlib.Order.Extension.Linear
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_2 : ∀ (a b c_1 : α), (∃ r ∈ c, r a b) → (∃ r ∈ c, r b c_1) → ∃ r ∈ c, r a c_1
⊢ ∀ (a b c_1 : α), sSup c a b → sSup c b c_1 → sSup c a c_1

Tactic:
simp_rw [binary_relation_sSup_iff]

Premises used: binary_relation_sSup_iff
-- Module: Mathlib.Order.Extension.Linear
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_3 : ∀ (a b : α), (∃ r ∈ c, r a b) → (∃ r ∈ c, r b a) → a = b
⊢ ∀ (a b : α), sSup c a b → sSup c b a → a = b

Tactic:
simp_rw [binary_relation_sSup_iff]

Premises used: binary_relation_sSup_iff
-- Module: Mathlib.Order.Extension.Linear
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 : α
⊢ ∃ r ∈ c, r x x

Tactic:
⟨s, hs, refl x⟩

Premises used: And.intro, Exists.intro, refl
-- Module: Mathlib.Order.Extension.Linear
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 : α
⊢ ∃ r ∈ c, r x x

Tactic:
exact ⟨s, hs, refl x⟩
-- Module: Mathlib.Order.Extension.Linear
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
⊢ IsPartialOrder α s₁

Tactic:
haveI : IsPartialOrder _ _ := hc₁ h₁s₁
-- Module: Mathlib.Order.Extension.Linear
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₁
⊢ IsPartialOrder α s₂

Tactic:
haveI : IsPartialOrder _ _ := hc₁ h₁s₂
-- Module: Mathlib.Order.Extension.Linear
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
refine_2₁ : ∀ (h : s₂ ≤ s₁), ∃ r ∈ c, r x z
⊢ ∃ r ∈ c, r x z

Tactic:
rcases hc₂.total h₁s₁ h₁s₂ with h | h

Premises used: IsChain.total
-- Module: Mathlib.Order.Extension.Linear
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₂
h : s₁ ≤ s₂
⊢ ∃ r ∈ c, r x z

Tactic:
⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩

Premises used: trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Extension.Linear
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₂
h : s₁ ≤ s₂
⊢ ∃ r ∈ c, r x z

Tactic:
exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩
-- Module: Mathlib.Order.Extension.Linear
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₂
h : s₂ ≤ s₁
⊢ ∃ r ∈ c, r x z

Tactic:
⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩

Premises used: trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Extension.Linear
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₂
h : s₂ ≤ s₁
⊢ ∃ r ∈ c, r x z

Tactic:
exact ⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩
-- Module: Mathlib.Order.Extension.Linear
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
⊢ IsPartialOrder α s₁

Tactic:
haveI : IsPartialOrder _ _ := hc₁ h₁s₁
-- Module: Mathlib.Order.Extension.Linear
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₁
⊢ IsPartialOrder α s₂

Tactic:
haveI : IsPartialOrder _ _ := hc₁ h₁s₂
-- Module: Mathlib.Order.Extension.Linear
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
refine_3₁ : ∀ (h : s₂ ≤ s₁), x = y
⊢ x = y

Tactic:
rcases hc₂.total h₁s₁ h₁s₂ with h | h

Premises used: IsChain.total
-- Module: Mathlib.Order.Extension.Linear
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₂
h : s₁ ≤ s₂
⊢ x = y

Tactic:
antisymm (h _ _ h₂s₁) h₂s₂

Premises used: antisymm