awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ Disjoint a b
rw₁ : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ a ⊓ b = ⊥
rw₂ : (↑(a ⊓ b) : α) = ⊥ ↔ a ⊓ b = ⊥
rw₃ : (↑(a ⊓ b) : α) = (↑⊥ : α) ↔ a ⊓ b = ⊥
rw₄ rw₅ : a ⊓ b = ⊥ ↔ a ⊓ b = ⊥
⊢ Disjoint (↑a : α) (↑b : α) ↔ Disjoint a b

Tactic:
rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]

Premises used: disjoint_iff, Complementeds.coe_inf, Complementeds.coe_bot, Complementeds.coe_inj
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ Codisjoint a b
rw₁ : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ a ⊔ b = ⊤
rw₂ : (↑(a ⊔ b) : α) = ⊤ ↔ a ⊔ b = ⊤
rw₃ : (↑(a ⊔ b) : α) = (↑⊤ : α) ↔ a ⊔ b = ⊤
rw₄ rw₅ : a ⊔ b = ⊤ ↔ a ⊔ b = ⊤
⊢ Codisjoint (↑a : α) (↑b : α) ↔ Codisjoint a b

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]

Premises used: codisjoint_iff, Complementeds.coe_top, Complementeds.coe_sup, Complementeds.coe_inj
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
simp_rw : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint a b ∧ Codisjoint a b
simp_rw₁ : Disjoint a b ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint a b ∧ Codisjoint a b
⊢ IsCompl (↑a : α) (↑b : α) ↔ IsCompl a b

Tactic:
simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]

Premises used: Complementeds.codisjoint_coe, isCompl_iff, Complementeds.disjoint_coe
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ ComplementedLattice.{u_1} (Complementeds α)

Tactic:
⟨fun ⟨a, b, h⟩ => ⟨⟨b, a, h.symm⟩, isCompl_coe.1 h⟩⟩

Premises used: ComplementedLattice.mk, _private.0.Complementeds.instComplementedLattice.match_1, Exists, Subtype.mk, IsCompl, Exists.intro, Iff.mp, Complementeds.isCompl_coe, IsCompl.symm
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed f i = f i \ (Iio i).sup f

Tactic:
rfl

Premises used: disjointed, rfl
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
rwa : (↑(Iio i) : Set ι) = ∅
rwa₁ : Set.Iio i = ∅
rwa₂ rwa₃ rwa₄ rwa₅ : IsMin i
⊢ Iio i = ∅

Tactic:
rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]

Premises used: Finset.coe_eq_empty, Set.Iio_eq_empty_iff, Finset.coe_Iio
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ Iio i = ∅

Tactic:
have : Iio i = ∅ := by rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
this : Iio i = ∅
⊢ disjointed f i = f i

Tactic:
simp only [disjointed_apply, this, sup_empty, sdiff_bot]

Premises used: Finset.sup_empty, disjointed_apply, sdiff_bot
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : OrderBot ι
f : ι → α
⊢ disjointed f ⊥ = f ⊥

Tactic:
disjointed_of_isMin _ isMin_bot

Premises used: disjointed_of_isMin, isMin_bot
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
⊢ LE.le (α := (f : ι → α) → (i : ι) → α) disjointed id

Tactic:
fun _ _ ↦ sdiff_le

Premises used: disjointed, sdiff_le
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed f ≤ f

Tactic:
disjointed_le_id f

Premises used: disjointed_le_id
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i j : ι
h : i < j
⊢ Disjoint (disjointed f i) (disjointed f j)

Tactic:
(disjoint_sdiff_self_right.mono_left <| le_sup (mem_Iio.mpr h)).mono_left (disjointed_le f i)

Premises used: Iff.mpr, disjoint_sdiff_self_right, Disjoint.mono_left, disjointed_le, Finset.mem_Iio, Finset.le_sup
-- Module: Mathlib.Order.Disjointed
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)
rw : Eq.{u_1 + 1} (α := α) ((Iio i).sup fun (j : ι) ↦ ⊥) ⊥
⊢ disjointed f i = f i

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]

Premises used: Finset.sup_inf_distrib_left, disjoint_iff, Disjoint.symm, Finset.sup_congr, Iff.mp, disjointed_apply, sdiff_eq_left, Finset.mem_Iio, rfl
-- Module: Mathlib.Order.Disjointed
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)
⊢ Eq.{u_1 + 1} (α := α) ((Iio i).sup fun (j : ι) ↦ ⊥) ⊥

Tactic:
sup_bot _

Premises used: Finset.sup_bot
-- Module: Mathlib.Order.Disjointed
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)
⊢ Eq.{u_1 + 1} (α := α) ((Iio i).sup fun (j : ι) ↦ ⊥) ⊥

Tactic:
exact sup_bot _

Premises used: Finset.sup_bot
-- Module: Mathlib.Order.Disjointed
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)
rw : p (f i \ (Iio i).sup f)
⊢ p (disjointed f i)

Tactic:
rw [disjointed]

Premises used: disjointed
-- Module: Mathlib.Order.Disjointed
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)
suffices : ∀ (s : Finset ι), p (f i \ s.sup f)
⊢ p (f i \ (Iio i).sup f)

Tactic:
suffices ∀ (s : Finset ι), p (f i \ s.sup f) from this _
-- Module: Mathlib.Order.Disjointed
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 \ sup ∅ f)

Tactic:
simpa only [sup_empty, sdiff_bot] using hpi

Premises used: Finset.sup_empty, sdiff_bot
-- Module: Mathlib.Order.Disjointed
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)
insert : p ((f i \ s.sup f) \ f a)
⊢ p (f i \ (Insert.insert a s).sup f)

Tactic:
rw [sup_insert, sup_comm, ← sdiff_sdiff]

Premises used: Finset.sup_insert, sdiff_sdiff, sup_comm
-- Module: Mathlib.Order.Disjointed
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 \ s.sup f) \ f a)

Tactic:
hdiff IH
-- Module: Mathlib.Order.Disjointed
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 \ s.sup f) \ f a)

Tactic:
exact hdiff IH
-- Module: Mathlib.Order.Disjointed
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)
insert : ∀ (a : ι) (s : Finset ι) (ht : a ∉ s) (IH : p (f i \ s.sup f)), p (f i \ (Insert.insert a s).sup f)
⊢ p (f i \ 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

Premises used: Finset.sup_insert, Finset.sup_empty, Insert.insert, sdiff_sdiff, sup_comm, sdiff_bot
-- Module: Mathlib.Order.Disjointed
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)
intro₃ intro₄ : ∀ ⦃i : ι⦄ (hpi : p (f i)) (s : Finset ι), p (f i \ s.sup f)
⊢ ∀ ⦃i : ι⦄, p (f i) → p (disjointed f i)

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

Premises used: Finset.sup_insert, disjointed, Finset.sup_empty, Insert.insert, sdiff_sdiff, sup_comm, sdiff_bot
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
suffices :
  ∀ (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:
suffices ∀ r i (hi : #(Iio i) ≤ r), partialSups (disjointed f) i = partialSups f i from
    OrderHom.ext _ _ (funext fun i ↦ this _ i le_rfl)
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hi : #(Iio i) ≤ 0
⊢ Iio i = ∅

Tactic:
simp only [Nat.le_zero, card_eq_zero] at hi

Premises used: Nat.le_zero, Finset.card_eq_zero
-- Module: Mathlib.Order.Disjointed
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hi : Iio i = ∅
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)

Tactic:
simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]

Premises used: partialSups_apply, Finset.sup_empty, Finset.Iic_eq_cons_Iio, disjointed_apply, Finset.sup_cons, sdiff_bot, Finset.sup'_eq_sup
-- Module: Mathlib.Order.Disjointed
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 : α)
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 : α)

Tactic:
rcases lt_or_eq_of_le hi with hn | hn

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

Tactic:
ih _ <| Nat.le_of_lt_succ hn

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Order.Disjointed
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 : α)

Tactic:
exact ih _ <| Nat.le_of_lt_succ hn

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Order.Disjointed
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
succ : (disjointed f i ⊔ (Iio i).sup fun (x : ι) ↦ disjointed f x) = (partialSups f : (a : ι) → α) i
⊢ Eq.{u_1 + 1} (α := α) ((partialSups (disjointed f) : (a : ι) → α) i : α) ((partialSups f : (a : ι) → α) i : α)

Tactic:
simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]

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

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

Tactic:
simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
-- Module: Mathlib.Order.Disjointed
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

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⟩⟩
-- Module: Mathlib.Order.Disjointed
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
succ₁ :
  ∀ a ∈ Iio i,
    Eq.{u_1 + 1} (α := α) ((Iic a).sup fun (x : ι) ↦ disjointed f x : α) ((partialSups f : (a : ι) → α) a : α)
⊢ (disjointed f i ⊔ (Iio i).sup fun (x : ι) ↦ disjointed f x) = (partialSups f : (a : ι) → α) i

Tactic:
rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]

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 ι
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 f = (Iic i).sup f
⊢ disjointed f i ⊔ (Iio i).sup (⇑(partialSups f) : (a : ι) → α) = (partialSups f : (a : ι) → α) i

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

Premises used: partialSups_apply, funext, 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 : ι → α
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 f = (Iic i).sup f

Tactic:
simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]

Premises used: disjointed, Finset.Iic_eq_cons_Iio, sdiff_sup_self, Finset.sup_cons
-- Module: Mathlib.Order.Disjointed
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 :
  ∀ (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
⊢ ∀ a ∈ Iio i,
    Eq.{u_1 + 1} (α := α) ((Iic a).sup fun (x : ι) ↦ disjointed f x : α) ((partialSups f : (a : ι) → α) a : α)

Tactic:
simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢

Premises used: partialSups, OrderHom.coe_mk, Finset.sup'_eq_sup
-- Module: Mathlib.Order.Disjointed
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

Tactic:
fun x hx ↦ ih x ?_
-- Module: Mathlib.Order.Disjointed
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
succ : ∀ (x : ι) (hx : x ∈ Iio i), #(Iio x) ≤ n
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun (x : ι) ↦ disjointed f x) = (Iic a).sup f

Tactic:
refine fun x hx ↦ ih x ?_
-- Module: Mathlib.Order.Disjointed
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) < #(Iio i)
⊢ #(Iio x) ≤ n

Tactic:
rw [← Nat.lt_add_one_iff, ← hn]

Premises used: Nat.lt_add_one_iff
-- Module: Mathlib.Order.Disjointed
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)
succ₁ : #(Iic x) ≤ #(Iio i)
⊢ #(Iio x) < #(Iio i)

Tactic:
apply lt_of_lt_of_le (b := #(Iic x))

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Order.Disjointed
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) < #(Iic x)

Tactic:
simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _

Premises used: Nat.lt_succ_self, Finset.Iic_eq_cons_Iio, Finset.card_cons
-- Module: Mathlib.Order.Disjointed
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)

Tactic:
card_le_card (fun r hr ↦ ?_)

Premises used: Finset.card_le_card
-- Module: Mathlib.Order.Disjointed
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 : ∀ (r : ι) (hr : r ∈ Iic x), r ∈ Iio i
⊢ #(Iic x) ≤ #(Iio i)

Tactic:
refine card_le_card (fun r hr ↦ ?_)

Premises used: Finset.card_le_card
-- Module: Mathlib.Order.Disjointed
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
succ : ∀ (hx : x < i) (hr : r ≤ x), r < i
⊢ r ∈ Iio i

Tactic:
simp only [mem_Iic, mem_Iio] at hx hr ⊢

Premises used: Finset.mem_Iic, Finset.mem_Iio
-- Module: Mathlib.Order.Disjointed
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 r : ι
hx : x < i
hr : r ≤ x
⊢ r < i

Tactic:
hr.trans_lt hx

Premises used: LE.le.trans_lt
-- Module: Mathlib.Order.Disjointed
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 r : ι
hx : x < i
hr : r ≤ x
⊢ r < i

Tactic:
exact hr.trans_lt hx

Premises used: LE.le.trans_lt