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 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
i : ι
h : Membership.mem (γ := Finset ι) univ i
rw : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup f
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f
have rw₁ : (Iic i).sup' sorry (disjointed f) = (Iic i).sup' sorry f
Tactic: rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
i : ι
h : Membership.mem (γ := Finset ι) univ i
rw : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup f
rw₁ : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup' ⋯ f
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f
have rw₂ : (partialSups (disjointed f) : (a : ι) → α) i = (Iic i).sup' sorry f
Tactic: rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
i : ι
h : Membership.mem (γ := Finset ι) univ i
rw : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup f
rw₁ : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup' ⋯ f
rw₂ : (partialSups (disjointed f) : (a : ι) → α) i = (Iic i).sup' ⋯ f
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f
have rw₃ : Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
i : ι
h : Membership.mem (γ := Finset ι) univ i
rw : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup f
rw₁ : (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup' ⋯ f
rw₂ : (partialSups (disjointed f) : (a : ι) → α) i = (Iic i).sup' ⋯ f
rw₃ : Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f
have rw₄ : Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
⊢ sup univ (disjointed f) = sup univ f
have have : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
Tactic: classical
  have hun : univ.biUnion Iic = (univ : Finset ι) := by
    ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩
  rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]
  rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
have : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
⊢ sup univ (disjointed f) = sup univ f
have have₁ : ∀ (hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ), sup univ (disjointed f) = sup univ f
Tactic: classical
  have hun : univ.biUnion Iic = (univ : Finset ι) := by
    ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩
  rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]
  rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
have : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
have₁ : ∀ (hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ), sup univ (disjointed f) = sup univ f
have₂ : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
have₃ have₄ :
  ∀ (hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ), sup univ (disjointed f) = sup univ f
⊢ sup univ (disjointed f) = sup univ f
have have₅ : ∀ (hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ) (i : ι),
  Membership.mem (γ := Finset ι) univ i → (Iic i).sup (disjointed f) = (Iic i).sup f
Tactic: classical
  have hun : univ.biUnion Iic = (univ : Finset ι) := by
    ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩
  rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]
  rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) = disjointed f
have h : ∀ (i : ι), disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f
have rw : (partialSups f : (a : ι) → α) i \ (f i \ (Iio i).sup f) = (Iio i).sup f
Tactic: rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (partialSups f : (a : ι) → α) i \ (f i \ (Iio i).sup f) = (Iio i).sup f
have simp : (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f
Tactic: simp only [funext (partialSups_apply f), sup'_eq_sup]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f
have rw : (Iic i).sup f \ f i ≤ (Iio i).sup f
Tactic: rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
-- Lean 4 proof step from Mathlib.Order.Disjointed (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
have step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f
Tactic: have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
have h : (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f
Tactic: simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f
⊢ (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f
have h : ∀ (r : ι), r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i
Tactic: congr 2 with r
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) = disjointed f
have h : ∀ (i : ι), disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
Tactic: classical
  ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
h : ∀ (i : ι), disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) = disjointed f
have h₁ : ∀ (i : ι) (step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f),
  disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
Tactic: classical
  ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
h : ∀ (i : ι), disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
h₁ :
  ∀ (i : ι) (step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f),
    disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) = disjointed f
have h₂ : ∀ (i : ι) (step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f),
  (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f
Tactic: classical
  ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
h : ∀ (i : ι), disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
h₁ :
  ∀ (i : ι) (step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f),
    disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i
h₂ :
  ∀ (i : ι) (step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f),
    (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) = disjointed f
have h₃ : ∀ (i : ι) (step1 : f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f) (r : ι),
  r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i
Tactic: classical
  ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : Eq (α := ι →o α) (partialSups d) (partialSups f)
⊢ d = disjointed f
have rw : d = disjointed d
Tactic: rw [← disjointed_partialSups, ← hsups, disjointed_partialSups]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
ι : Type u_2
inst : PartialOrder ι
inst_1 : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i)
    (((partialSups f : OrderHom.{u_2, u_3} ι (Set α)) : (a : ι) → Set α) n)
have rw : Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i) (⨆ (j : ι), ⨆ (_ : j ≤ n), disjointed f j)
Tactic: rw [← partialSups_disjointed, partialSups_eq_biSup]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ range (n + 1), disjointed f i) ((partialSups f : (a : ℕ) → Set α) n)
have rw : Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i) ((partialSups f : (a : ℕ) → Set α) n)
Tactic: rw [Nat.range_succ_eq_Iic, biUnion_Iic_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_3
f : ℕ → Set α
n : ℕ
rw : Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i) ((partialSups f : (a : ℕ) → Set α) n)
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ range (n + 1), disjointed f i) ((partialSups f : (a : ℕ) → Set α) n)
have rw₁ : Eq (α := Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α)
Tactic: rw [Nat.range_succ_eq_Iic, biUnion_Iic_disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = ((partialSups t : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
have rw : (Iic n).disjiUnion (disjointed t) sorry =
  ((partialSups (disjointed t) : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
Tactic: rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DecidableEq α
n : ι
t : ι → Finset α
rw :
  (Iic n).disjiUnion (disjointed t) ⋯ =
    ((partialSups (disjointed t) : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = ((partialSups t : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
have rw₁ : (Iic n).disjiUnion (disjointed t) sorry = (Iic n).sup' sorry (disjointed t)
Tactic: rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DecidableEq α
n : ι
t : ι → Finset α
rw :
  (Iic n).disjiUnion (disjointed t) ⋯ =
    ((partialSups (disjointed t) : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
rw₁ : (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup' ⋯ (disjointed t)
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = ((partialSups t : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
have rw₂ : (Iic n).disjiUnion (disjointed t) sorry = (Iic n).sup (disjointed t)
Tactic: rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DecidableEq α
n : ι
t : ι → Finset α
rw :
  (Iic n).disjiUnion (disjointed t) ⋯ =
    ((partialSups (disjointed t) : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
rw₁ : (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup' ⋯ (disjointed t)
rw₂ : (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup (disjointed t)
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = ((partialSups t : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
have rw₃ : (Iic n).disjiUnion (disjointed t) sorry = (Iic n).biUnion (disjointed t)
Tactic: rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DecidableEq α
n : ι
t : ι → Finset α
rw :
  (Iic n).disjiUnion (disjointed t) ⋯ =
    ((partialSups (disjointed t) : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
rw₁ : (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup' ⋯ (disjointed t)
rw₂ : (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup (disjointed t)
rw₃ : (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).biUnion (disjointed t)
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = ((partialSups t : OrderHom.{u_2, u_1} ι (Finset α)) : (a : ι) → Finset α) n
have rw₄ : (Iic n).biUnion (disjointed t) = (Iic n).biUnion (disjointed t)
Tactic: rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]
-- 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 : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f : (a : ι) → α) i
have rw : f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f
Tactic: rw [disjointed_apply, partialSups_apply, sup'_eq_sup]
-- 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 : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f
have e_a : ∀ (m : ι), m ∈ Iio (succ i) ↔ m ∈ Iic i
Tactic: congr 2 with m
-- 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 : ι
hn : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i
have rwa : f (succ i) \ (partialSups f : (a : ι) → α) i = f (succ i) \ f i
Tactic: rwa [disjointed_succ, hf.partialSups_eq]
-- 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 : ι
hn : ¬IsMax i
rwa : f (succ i) \ (partialSups f : (a : ι) → α) i = f (succ i) \ f i
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i
have rwa₁ : f (succ i) \ f i = f (succ i) \ f i
Tactic: rwa [disjointed_succ, hf.partialSups_eq]
-- 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 : ι
⊢ disjointed f (succ i) ⊔ f i = f (succ i)
have pos : ∀ (h : IsMax i), disjointed f (succ i) ⊔ f i = f (succ i)
Tactic: by_cases h : IsMax 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 : ι
pos : ∀ (h : IsMax i), disjointed f (succ i) ⊔ f i = f (succ i)
⊢ disjointed f (succ i) ⊔ f i = f (succ i)
have neg : ∀ (h : ¬IsMax i), disjointed f (succ i) ⊔ f i = f (succ i)
Tactic: by_cases h : IsMax 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
⊢ disjointed f (succ i) ⊔ f i = f (succ i)
have neg : f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
Tactic: rw [disjointed_apply]
-- 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
⊢ Iio (succ i) = Iic i
have h₁ : ∀ (a : ι), a ∈ Iio (succ i) ↔ a ∈ Iic i
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Disjointed (hypothesis)
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
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
have this : Iio (succ i) = Iic i
Tactic: have : Iio (succ i) = Iic i := by
      ext
      simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]
-- 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
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
have neg : f (succ i) \ (Iic 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]
-- 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)
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
have neg₁ : f (succ i) \ (Iic i).sup' sorry 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]