awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Disjointed
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 : α)
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 : α)
⊢ 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

Premises used: partialSups_apply, Order.succ, lt_or_eq_of_le, Finset.card_le_card, disjointed, Finset.mem_Iic, Nat.le_zero, partialSups, Finset.sup_empty, Nat.lt_add_one_iff, Nat.lt_succ_self, OrderHom.coe_mk, Finset.Iic_eq_cons_Iio, sdiff_sup_self, funext, Finset.card_cons, Finset.card_eq_zero, Finset.sup_congr, disjointed_apply, Finset.sup_cons, sdiff_bot, Finset.mem_Iio, Finset.sup_biUnion, Finset.sup'_eq_sup, rfl
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
We We₁ We₂ We₃ :
  ∀ (r : ℕ) (i : ι) (hi : #(Iio i) ≤ r),
    Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
⊢ Eq (α := ι →o α) (partialSups (disjointed f)) (partialSups f)

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

Premises used: partialSups_apply, Order.succ, Finset.card_le_card, disjointed, Finset.mem_Iic, Nat.le_zero, partialSups, Finset.sup_empty, Nat.lt_add_one_iff, Nat.lt_succ_self, OrderHom.coe_mk, Finset.Iic_eq_cons_Iio, sdiff_sup_self, funext, Finset.card_cons, Finset.card_eq_zero, Finset.sup_congr, disjointed_apply, Finset.sup_cons, sdiff_bot, Finset.mem_Iio, Finset.sup_biUnion, Finset.sup'_eq_sup, rfl
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
h : ∀ (r : ι), Membership.mem (γ := Finset ι) (Finset.biUnion univ Iic) r ↔ Membership.mem (γ := Finset ι) univ r
⊢ Eq.{u_2 + 1} (α := Finset ι) (Finset.biUnion univ Iic) univ

Tactic:
ext r
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : Fintype ι
f : ι → α
r : ι
⊢ Membership.mem (γ := Finset ι) (Finset.biUnion univ Iic) r ↔ Membership.mem (γ := Finset ι) univ r

Tactic:
simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩

Premises used: Finset.mem_univ, Finset.mem_Iic, iff_true, Finset.mem_biUnion, true_and
-- Module: Mathlib.Order.Disjointed
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

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⟩
-- Module: Mathlib.Order.Disjointed
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
rw : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → (Iic i).sup (disjointed f) = (Iic i).sup f
⊢ sup univ (disjointed f) = sup univ f

Tactic:
rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]

Premises used: Finset.sup_congr, Finset.sup_biUnion, rfl
-- Module: Mathlib.Order.Disjointed
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 : α)
rw₄ rw₅ : Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f

Tactic:
rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]

Premises used: partialSups_apply, partialSups_disjointed, Finset.sup'_eq_sup, Finset.nonempty_Iic
-- Module: Mathlib.Order.Disjointed
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
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
⊢ 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]

Premises used: partialSups_apply, partialSups_disjointed, Finset.sup_congr, Finset.sup_biUnion, Finset.sup'_eq_sup, rfl, Finset.nonempty_Iic
-- Module: Mathlib.Order.Disjointed
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

Tactic:
ext i
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
rw : (partialSups f : (a : ι) → α) i \ (f i \ (Iio i).sup f) = (Iio i).sup f
⊢ f i \ (Iio i).sup f = (partialSups f : (a : ι) → α) i \ (Iio i).sup f

Tactic:
rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]

Premises used: sdiff_eq_symm, sdiff_le, LE.le.trans, le_partialSups
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
simp : (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f
⊢ (partialSups f : (a : ι) → α) i \ (f i \ (Iio i).sup f) = (Iio i).sup f

Tactic:
simp only [funext (partialSups_apply f), sup'_eq_sup]

Premises used: partialSups_apply, funext, Finset.sup'_eq_sup
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
rw : (Iic i).sup f \ f i ≤ (Iio i).sup f
⊢ (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f

Tactic:
rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]

Premises used: Finset.Iio_subset_Iic_self, sup_eq_right, Finset.sup_mono, sdiff_sdiff_eq_sdiff_sup
-- Module: Mathlib.Order.Disjointed
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

Tactic:
simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]

Premises used: le_sup_right, Finset.Iic_eq_cons_Iio, sup_sdiff_left_self, Finset.sup_cons, sdiff_le_iff
-- Module: Mathlib.Order.Disjointed
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

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]
-- Module: Mathlib.Order.Disjointed
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
h : (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) i = disjointed f i

Tactic:
simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]

Premises used: partialSups_apply, funext, disjointed_apply, Finset.sup_biUnion, Finset.sup'_eq_sup
-- Module: Mathlib.Order.Disjointed
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
h : ∀ (r : ι), r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i
⊢ (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f

Tactic:
congr 2 with r
-- Module: Mathlib.Order.Disjointed
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
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i

Tactic:
simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

Premises used: Finset.mem_Iic, Finset.mem_Iio, Finset.mem_biUnion
-- Module: Mathlib.Order.Disjointed
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
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
⊢ disjointed (⇑(partialSups f) : (a : ι) → α) = disjointed 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⟩⟩

Premises used: partialSups_apply, Finset.mem_Iic, funext, disjointed_apply, Finset.mem_Iio, Finset.sup_biUnion, Finset.sup'_eq_sup, Finset.mem_biUnion
-- Module: Mathlib.Order.Disjointed
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)
rw : d = disjointed d
⊢ d = disjointed f

Tactic:
rw [← disjointed_partialSups, ← hsups, disjointed_partialSups]

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

Tactic:
funext fun _ ↦ (disjointed_eq_self (fun _ hj ↦ hdisj hj)).symm

Premises used: disjointed_eq_self, funext, Eq.symm
-- Module: Mathlib.Order.Disjointed
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 d

Tactic:
exact funext fun _ ↦ (disjointed_eq_self (fun _ hj ↦ hdisj hj)).symm

Premises used: disjointed_eq_self, funext, Eq.symm
-- Module: Mathlib.Order.Disjointed
Goal:
ι : Type u_2
inst : PartialOrder ι
inst_1 : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
rw : Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i) (⨆ (j : ι), ⨆ (_ : j ≤ n), disjointed f j)
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i)
    (((partialSups f : OrderHom.{u_2, u_3} ι (Set α)) : (a : ι) → Set α) n)

Tactic:
rw [← partialSups_disjointed, partialSups_eq_biSup]

Premises used: partialSups_disjointed, partialSups_eq_biSup
-- Module: Mathlib.Order.Disjointed
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) (⨆ (j : ι), ⨆ (_ : j ≤ n), disjointed f j)

Tactic:
simp
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_3
f : ℕ → Set α
n : ℕ
rw : Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ Iic n, disjointed f i) ((partialSups f : (a : ℕ) → Set α) n)
rw₁ rw₂ : Eq (α := Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α)
⊢ Eq.{u_3 + 1} (α := Set α) (⋃ i ∈ range (n + 1), disjointed f i) ((partialSups f : (a : ℕ) → Set α) n)

Tactic:
rw [Nat.range_succ_eq_Iic, biUnion_Iic_disjointed]

Premises used: Nat.range_succ_eq_Iic, biUnion_Iic_disjointed
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ Pairwise (Disjoint on disjointed f)

Tactic:
(pairwise_disjoint_on _).mpr fun _ _ ↦ disjoint_disjointed_of_lt f

Premises used: Iff.mpr, disjoint_disjointed_of_lt, pairwise_disjoint_on
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : Pairwise (Disjoint on d)
hsups : Eq (α := ι →o α) (partialSups d) (partialSups f)
⊢ d = disjointed f

Tactic:
disjointed_unique (fun hij ↦ hdisj hij.ne) hsups

Premises used: disjointed_unique, LT.lt.ne
-- Module: Mathlib.Order.Disjointed
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)
rw₄ rw₅ : (Iic n).biUnion (disjointed t) = (Iic n).biUnion (disjointed t)
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = ((partialSups 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]

Premises used: partialSups_apply, Finset.disjiUnion_eq_biUnion, partialSups_disjointed, Finset.sup_eq_biUnion, Finset.sup'_eq_sup
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
rw : f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f : (a : ι) → α) i

Tactic:
rw [disjointed_apply, partialSups_apply, sup'_eq_sup]

Premises used: partialSups_apply, disjointed_apply, Finset.sup'_eq_sup
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
e_a : ∀ (m : ι), m ∈ Iio (succ i) ↔ m ∈ Iic i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f

Tactic:
congr 2 with m
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
m : ι
⊢ m ∈ Iio (succ i) ↔ m ∈ Iic i

Tactic:
simpa only [mem_Iio, mem_Iic] using lt_succ_iff_of_not_isMax hi

Premises used: Finset.mem_Iic, Order.lt_succ_iff_of_not_isMax, Finset.mem_Iio
-- 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 : ι
hn : ¬IsMax i
rwa : f (succ i) \ (partialSups f : (a : ι) → α) i = f (succ i) \ f i
hi : ¬IsMax i
rwa₁ : f (succ i) \ f i = f (succ i) \ f i
hi₁ : ¬IsMax i
rwa₂ : f (succ i) \ f i = f (succ i) \ f i
hi₂ hi₃ hi₄ : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i

Tactic:
rwa [disjointed_succ, hf.partialSups_eq]

Premises used: Monotone.partialSups_eq, disjointed_succ
-- 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 : ι
pos : ∀ (h : IsMax i), disjointed f (succ i) ⊔ f i = f (succ i)
neg : ∀ (h : ¬IsMax i), disjointed f (succ i) ⊔ f i = f (succ i)
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
by_cases h : IsMax i

Premises used: IsMax
-- 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
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
simpa only [succ_eq_iff_isMax.mpr h, sup_eq_right] using disjointed_le f i

Premises used: Iff.mpr, Order.succ_eq_iff_isMax, disjointed_le, sup_eq_right
-- 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
neg : f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
rw [disjointed_apply]

Premises used: disjointed_apply
-- 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
h₁ : ∀ (a : ι), a ∈ Iio (succ i) ↔ a ∈ Iic i
⊢ Iio (succ i) = Iic i

Tactic:
ext
-- 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
a : ι
⊢ a ∈ Iio (succ i) ↔ a ∈ Iic i

Tactic:
simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]

Premises used: Or.comm, Finset.mem_Iic, Order.lt_succ_iff_eq_or_lt_of_not_isMax, le_iff_lt_or_eq, Finset.mem_Iio
-- 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
⊢ 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]