awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Disjointed (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ disjointed f i = f i
have this : Iio i = ∅
Tactic: have : Iio i = ∅ := by rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ disjointed f i = f i
have rw : Eq.{u_1 + 1} (α := α) ((Iio i).sup fun (j : ι) ↦ ⊥) ⊥
Tactic: rw [disjointed_apply, sdiff_eq_left, disjoint_iff, sup_inf_distrib_left,
    sup_congr rfl <| fun j hj ↦ disjoint_iff.mp <| (hf _ (mem_Iio.mp hj)).symm]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
⊢ p (disjointed f i)
have rw : p (f i \ (Iio i).sup f)
Tactic: rw [disjointed]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
⊢ p (f i \ (Iio i).sup f)
have suffices : ∀ (s : Finset ι), p (f i \ s.sup f)
Tactic: suffices ∀ (s : Finset ι), p (f i \ s.sup f) from this _
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a : ι
s : Finset ι
ht : a ∉ s
IH : p (f i \ s.sup f)
⊢ p (f i \ (insert a s).sup f)
have insert : p ((f i \ s.sup f) \ f a)
Tactic: rw [sup_insert, sup_comm, ← sdiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
s : Finset ι
⊢ p (f i \ s.sup f)
have empty : p (f i \ sup ∅ f)
Tactic: induction s using Finset.induction with
  | empty => simpa only [sup_empty, sdiff_bot] using hpi
  | insert _ _ ht IH =>
    rw [sup_insert, sup_comm, ← sdiff_sdiff]
    exact hdiff IH
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
s : Finset ι
empty : p (f i \ sup ∅ f)
⊢ p (f i \ s.sup f)
have insert : ∀ (a : ι) (s : Finset ι) (ht : a ∉ s) (IH : p (f i \ s.sup f)), p (f i \ (insert a s).sup f)
Tactic: induction s using Finset.induction with
  | empty => simpa only [sup_empty, sdiff_bot] using hpi
  | insert _ _ ht IH =>
    rw [sup_insert, sup_comm, ← sdiff_sdiff]
    exact hdiff IH
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
intro intro₁ : ∀ ⦃i : ι⦄ (hpi : p (f i)), p (disjointed f i)
⊢ ∀ ⦃i : ι⦄, p (f i) → p (disjointed f i)
have intro₂ : ∀ ⦃i : ι⦄ (hpi : p (f i)), p (f i \ (Iio i).sup f)
Tactic: classical
  intro i hpi
  rw [disjointed]
  suffices ∀ (s : Finset ι), p (f i \ s.sup f) from this _
  intro s
  induction s using Finset.induction with
  | empty => simpa only [sup_empty, sdiff_bot] using hpi
  | insert _ _ ht IH =>
    rw [sup_insert, sup_comm, ← sdiff_sdiff]
    exact hdiff IH
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
intro intro₁ : ∀ ⦃i : ι⦄ (hpi : p (f i)), p (disjointed f i)
intro₂ : ∀ ⦃i : ι⦄ (hpi : p (f i)), p (f i \ (Iio i).sup f)
⊢ ∀ ⦃i : ι⦄, p (f i) → p (disjointed f i)
have intro₃ : ∀ ⦃i : ι⦄ (hpi : p (f i)) (s : Finset ι), p (f i \ s.sup f)
Tactic: classical
  intro i hpi
  rw [disjointed]
  suffices ∀ (s : Finset ι), p (f i \ s.sup f) from this _
  intro s
  induction s using Finset.induction with
  | empty => simpa only [sup_empty, sdiff_bot] using hpi
  | insert _ _ ht IH =>
    rw [sup_insert, sup_comm, ← sdiff_sdiff]
    exact hdiff IH
-- 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 : ι → α
⊢ Eq (α := ι →o α) (partialSups (disjointed f)) (partialSups f)
have suffices : ∀ (r : ℕ) (i : ι) (hi : #(Iio i) ≤ r),
  Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: suffices ∀ r i (hi : #(Iio i) ≤ r), partialSups (disjointed f) i = partialSups f i from
    OrderHom.ext _ _ (funext fun i ↦ this _ i le_rfl)
-- 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 : ι
hi : #(Iio i) ≤ 0
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
have hi₁ : Iio i = ∅
Tactic: simp only [Nat.le_zero, card_eq_zero] at hi
Cleared hypotheses: hi
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
have succ : ∀ (hn : #(Iio i) < n + 1),
  Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: rcases lt_or_eq_of_le hi with hn | hn
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
succ :
  ∀ (hn : #(Iio i) < n + 1),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
have succ₁ : ∀ (hn : #(Iio i) = n + 1),
  Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: rcases lt_or_eq_of_le hi with hn | hn
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
have succ : (disjointed f i ⊔ (Iio i).sup fun (x : ι) ↦ disjointed f x) = (partialSups f : (a : ι) → α) i
Tactic: simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (Iio i).biUnion Iic = Iio i
have h : ∀ (r : ι), r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i
Tactic: ext r
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (disjointed f i ⊔ (Iio i).sup fun (x : ι) ↦ disjointed f x) = (partialSups f : (a : ι) → α) i
have hun : (Iio i).biUnion Iic = Iio i
Tactic: have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ (disjointed f i ⊔ (Iio i).sup fun (x : ι) ↦ disjointed f x) = (partialSups f : (a : ι) → α) i
have succ : disjointed f i ⊔ (Iio i).sup (⇑(partialSups f) : (a : ι) → α) = (partialSups f : (a : ι) → α) i
Tactic: rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
succ : disjointed f i ⊔ (Iio i).sup (⇑(partialSups f) : (a : ι) → α) = (partialSups f : (a : ι) → α) i
⊢ (disjointed f i ⊔ (Iio i).sup fun (x : ι) ↦ disjointed f x) = (partialSups f : (a : ι) → α) i
have succ₁ : ∀ a ∈ Iio i, Eq.{u_1 + 1} (α := α) ((Iic a).sup fun (x : ι) ↦ disjointed f x : α) ((partialSups f : (a : ι) → α) a : α)
Tactic: rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup (⇑(partialSups f) : (a : ι) → α) = (partialSups f : (a : ι) → α) i
have succ : disjointed f i ⊔ (Iio i).sup f = (Iic i).sup f
Tactic: simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
-- 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 : ι → α
n : ℕ
ih :
  ∀ (i : ι) (hi : #(Iio i) ≤ n),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ ∀ a ∈ Iio i,
    Eq.{u_1 + 1} (α := α) ((Iic a).sup fun (x : ι) ↦ disjointed f x : α) ((partialSups f : (a : ι) → α) a : α)
have succ : ∀ (ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f),
  ∀ a ∈ Iio i, ((Iic a).sup fun (x : ι) ↦ disjointed f x) = (Iic a).sup f
Tactic: simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
Cleared hypotheses: ih
-- 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 : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun (x : ι) ↦ disjointed f x) = (Iic a).sup f
have succ : ∀ (x : ι) (hx : x ∈ Iio i), #(Iio x) ≤ n
Tactic: refine fun x hx ↦ ih x ?_
-- 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 : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) ≤ n
have succ : #(Iio x) < #(Iio i)
Tactic: rw [← Nat.lt_add_one_iff, ← hn]
-- 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 : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iio i)
have succ : #(Iio x) < #(Iic x)
Tactic: apply lt_of_lt_of_le (b := #(Iic x))
-- 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 : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
succ : #(Iio x) < #(Iic x)
⊢ #(Iio x) < #(Iio i)
have succ₁ : #(Iic x) ≤ #(Iio i)
Tactic: apply lt_of_lt_of_le (b := #(Iic x))
-- 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 : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iic x) ≤ #(Iio i)
have succ : ∀ (r : ι) (hr : r ∈ Iic x), r ∈ Iio i
Tactic: refine card_le_card (fun r hr ↦ ?_)
-- 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 : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι) (hi : #(Iio i) ≤ n), (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
r : ι
hr : r ∈ Iic x
⊢ r ∈ Iio i
have succ : ∀ (hx : x < i) (hr : r ≤ x), r < i
Tactic: simp only [mem_Iic, mem_Iio] at hx hr ⊢
Cleared hypotheses: hx, hr
-- 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 : ι → α
r : ℕ
i : ι
hi : #(Iio i) ≤ r
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
have zero : ∀ (i : ι) (hi : #(Iio i) ≤ 0),
  Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: induction r generalizing i with
  | zero =>
    -- Base case: `n` is minimal, so `partialSups f i = partialSups (disjointed f) n = f i`.
    simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]
  | succ n ih =>
    -- Induction step: first WLOG arrange that `#(Iio i) = r + 1`
    rcases lt_or_eq_of_le hi with hn | hn
    · exact ih _ <| Nat.le_of_lt_succ hn
    simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
    -- Key claim: we can write `Iio i` as a union of (finitely many) `Iic` intervals.
    have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
    -- Use claim and `sup_biUnion` to rewrite the supremum in the definition of `disjointed f`
    -- in terms of suprema over `Iic`'s. Then the RHS is a `sup` over `partialSups`, which we
    -- can rewrite via the induction hypothesis.
    rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
    · simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
      simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]
    · simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦ ih x ?_
      -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.
      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx
Cleared hypotheses: r, i, hi
-- 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 : ι → α
r : ℕ
i : ι
hi : #(Iio i) ≤ r
zero :
  ∀ (i : ι) (hi : #(Iio i) ≤ 0),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (i : ι) (hi : #(Iio i) ≤ n),
      Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α))
  (i : ι) (hi : #(Iio i) ≤ n + 1),
  Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: induction r generalizing i with
  | zero =>
    -- Base case: `n` is minimal, so `partialSups f i = partialSups (disjointed f) n = f i`.
    simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]
  | succ n ih =>
    -- Induction step: first WLOG arrange that `#(Iio i) = r + 1`
    rcases lt_or_eq_of_le hi with hn | hn
    · exact ih _ <| Nat.le_of_lt_succ hn
    simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
    -- Key claim: we can write `Iio i` as a union of (finitely many) `Iic` intervals.
    have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
    -- Use claim and `sup_biUnion` to rewrite the supremum in the definition of `disjointed f`
    -- in terms of suprema over `Iic`'s. Then the RHS is a `sup` over `partialSups`, which we
    -- can rewrite via the induction hypothesis.
    rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
    · simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
      simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]
    · simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦ ih x ?_
      -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.
      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx
Cleared hypotheses: r, i, hi
-- 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 : ι → α
⊢ Eq (α := ι →o α) (partialSups (disjointed f)) (partialSups f)
have We : ∀ (r : ℕ) (i : ι) (hi : #(Iio i) ≤ r),
  Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
Tactic: classical
  -- We argue by induction on the size of `Iio i`.
  suffices ∀ r i (hi : #(Iio i) ≤ r), partialSups (disjointed f) i = partialSups f i from
    OrderHom.ext _ _ (funext fun i ↦ this _ i le_rfl)
  intro r i hi
  induction r generalizing i with
  | zero =>
    -- Base case: `n` is minimal, so `partialSups f i = partialSups (disjointed f) n = f i`.
    simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]
  | succ n ih =>
    -- Induction step: first WLOG arrange that `#(Iio i) = r + 1`
    rcases lt_or_eq_of_le hi with hn | hn
    · exact ih _ <| Nat.le_of_lt_succ hn
    simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
    -- Key claim: we can write `Iio i` as a union of (finitely many) `Iic` intervals.
    have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
    -- Use claim and `sup_biUnion` to rewrite the supremum in the definition of `disjointed f`
    -- in terms of suprema over `Iic`'s. Then the RHS is a `sup` over `partialSups`, which we
    -- can rewrite via the induction hypothesis.
    rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
    · simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
      simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]
    · simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦ ih x ?_
      -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.
      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx
-- 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 : ι → α
⊢ Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
have h : ∀ (r : ι), Membership.mem (γ := Finset ι) (Finset.biUnion univ Iic) r ↔ Membership.mem (γ := Finset ι) univ r
Tactic: ext r
-- Lean 4 proof step from Mathlib.Order.Disjointed (hypothesis)
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 hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
Tactic: 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⟩
-- 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
⊢ sup univ (disjointed f) = sup univ f
have rw : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → (Iic i).sup (disjointed f) = (Iic i).sup f
Tactic: rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun 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 ι
inst_3 : Fintype ι
f : ι → α
hun : Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f
have rw : (Iic i).sup' sorry (disjointed f) = (Iic i).sup f
Tactic: rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]