/-
Copyright (c) 2021 Aaron Anderson, Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson, Kevin Buzzard, Yaël Dillies, Eric Wieser

! This file was ported from Lean 3 source module order.sup_indep
! leanprover-community/mathlib commit 1c857a1f6798cb054be942199463c2cf904cb937
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Pairwise
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.Basic

/-!
# Supremum independence

In this file, we define supremum independence of indexed sets. An indexed family `f : ι → α` is
sup-independent if, for all `a`, `f a` and the supremum of the rest are disjoint.

## Main definitions

* `Finset.SupIndep s f`: a family of elements `f` are supremum independent on the finite set `s`.
* `CompleteLattice.SetIndependent s`: a set of elements are supremum independent.
* `CompleteLattice.Independent f`: a family of elements are supremum independent.

## Main statements

* In a distributive lattice, supremum independence is equivalent to pairwise disjointness:
  * `Finset.supIndep_iff_pairwiseDisjoint`
  * `CompleteLattice.setIndependent_iff_pairwiseDisjoint`
  * `CompleteLattice.independent_iff_pairwiseDisjoint`
* Otherwise, supremum independence is stronger than pairwise disjointness:
  * `Finset.SupIndep.pairwiseDisjoint`
  * `CompleteLattice.SetIndependent.pairwiseDisjoint`
  * `CompleteLattice.Independent.pairwiseDisjoint`

## Implementation notes

For the finite version, we avoid the "obvious" definition
`∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)` because `erase` would require decidable equality on
`ι`.
-/


variable {α: Type ?u.24525
α β: Type ?u.17
β ι: Type ?u.8
ι ι': Type ?u.24534
ι' : Type _: Type (?u.51970+1)
Type _}

/-! ### On lattices with a bottom element, via `Finset.sup` -/


namespace Finset

section Lattice

variable [Lattice: Type ?u.4788 → Type ?u.4788
Lattice α: Type ?u.4776
α] [OrderBot: (α : Type ?u.1607) → [inst : LE α] → Type ?u.1607
OrderBot α: Type ?u.14
α]

/-- Supremum independence of finite sets. We avoid the "obvious" definition using `s.erase i`
because `erase` would require decidable equality on `ι`. -/
def SupIndep: Finset ι → (ι → α) → Prop
SupIndep (s: Finset ι
s : Finset: Type ?u.674 → Type ?u.674
Finset ι: Type ?u.350
ι) (f: ι → α
f : ι: Type ?u.350
ι → α: Type ?u.344
α) : Prop: Type
Prop :=
  ∀ ⦃t: ?m.685
t⦄, t: ?m.685
t ⊆ s: Finset ι
s → ∀ ⦃i: ?m.707
i⦄, i: ?m.707
i ∈ s: Finset ι
s → i: ?m.707
i ∉ t: ?m.685
t → Disjoint: {α : Type ?u.752} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (f: ι → α
f i: ?m.707
i) (t: ?m.685
t.sup: {α : Type ?u.825} → {β : Type ?u.824} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: ι → α
f)
#align finset.sup_indep Finset.SupIndep: {α : Type u_1} → {ι : Type u_2} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
Finset.SupIndep

variable {s: Finset ι
s t: Finset ι
t : Finset: Type ?u.5109 → Type ?u.5109
Finset ι: Type ?u.1256
ι} {f: ι → α
f : ι: Type ?u.1598
ι → α: Type ?u.4262
α} {i: ι
i : ι: Type ?u.4782
ι}

instance: {α : Type u_1} →
  {ι : Type u_2} →
    [inst : Lattice α] →
      [inst_1 : OrderBot α] →
        {s : Finset ι} → {f : ι → α} → [inst_2 : DecidableEq ι] → [inst_3 : DecidableEq α] → Decidable (SupIndep s f)
instance [DecidableEq: Sort ?u.1934 → Sort (max1?u.1934)
DecidableEq ι: Type ?u.1598
ι] [DecidableEq: Sort ?u.1943 → Sort (max1?u.1943)
DecidableEq α: Type ?u.1592
α] : Decidable: Prop → Type
Decidable (SupIndep: {α : Type ?u.1953} → {ι : Type ?u.1952} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep s: Finset ι
s f: ι → α
f) := by
Goals accomplished! 🐙
  α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

Decidable (SupIndep s f)refine @Finset.decidableForallOfDecidableSubsets: {α : Type ?u.1990} →
  {s : Finset α} →
    {p : (t : Finset α) → t ⊆ s → Prop} →
      [inst : (t : Finset α) → (h : t ⊆ s) → Decidable (p t h)] → Decidable (∀ (t : Finset α) (h : t ⊆ s), p t h)
Finset.decidableForallOfDecidableSubsets _: Type ?u.1990
_ _: Finset ?m.1991
_ _: (t : Finset ?m.1991) → t ⊆ ?m.1992 → Prop
_ (?_: (t : Finset ?m.1991) → (h : t ⊆ ?m.1992) → Decidable (?m.1993 t h)
?_)α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

(t : Finset ι) → t ⊆ s → Decidable (∀ ⦃i : ι⦄, i ∈ s → ¬i ∈ t → Disjoint (f i) (sup t f))
  α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

Decidable (SupIndep s f)rintro t: Finset ?m.1991
t -: t ⊆ ?m.1992
-α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t✝: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

t: Finset ι

Decidable (∀ ⦃i : ι⦄, i ∈ s → ¬i ∈ t → Disjoint (f i) (sup t f))
  α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

Decidable (SupIndep s f)refine @Finset.decidableDforallFinset: {α : Type ?u.2016} →
  {s : Finset α} →
    {p : (a : α) → a ∈ s → Prop} →
      [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] → Decidable (∀ (a : α) (h : a ∈ s), p a h)
Finset.decidableDforallFinset _: Type ?u.2016
_ _: Finset ?m.2017
_ _: (a : ?m.2017) → a ∈ ?m.2018 → Prop
_ (?_: (a : ?m.2017) → (h : a ∈ ?m.2018) → Decidable (?m.2019 a h)
?_)α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t✝: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

t: Finset ι

(a : ι) → a ∈ s → Decidable (¬a ∈ t → Disjoint (f a) (sup t f))
  α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

Decidable (SupIndep s f)rintro i: ?m.2017
i -: i ∈ ?m.2018
-α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

t: Finset ι

i: ι

Decidable (¬i ∈ t → Disjoint (f i) (sup t f))
  α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

Decidable (SupIndep s f)have : Decidable: Prop → Type
Decidable (Disjoint: {α : Type ?u.2041} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (f: ι → α
f i: ?m.2017
i) (sup: {α : Type ?u.2046} → {β : Type ?u.2045} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup t: Finset ?m.1991
t f: ι → α
f)) := decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' (_: ?m.2431
_ = ⊥: ?m.2434
⊥) disjoint_iff: ∀ {α : Type ?u.2507} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b = ⊥
disjoint_iffα: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

t: Finset ι

i: ι

this: Decidable (Disjoint (f i) (sup t f))

Decidable (¬i ∈ t → Disjoint (f i) (sup t f))
  α: Type ?u.1592

β: Type ?u.1595

ι: Type ?u.1598

ι': Type ?u.1601

inst✝³: Lattice α

inst✝²: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝¹: DecidableEq ι

inst✝: DecidableEq α

Decidable (SupIndep s f)infer_instance
Goals accomplished! 🐙

theorem SupIndep.subset: SupIndep t f → s ⊆ t → SupIndep s f
SupIndep.subset (ht: SupIndep t f
ht : t: Finset ι
t.SupIndep: {α : Type ?u.3984} → {ι : Type ?u.3983} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f) (h: s ⊆ t
h : s: Finset ι
s ⊆ t: Finset ι
t) : s: Finset ι
s.SupIndep: {α : Type ?u.4087} → {ι : Type ?u.4086} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f := fun _: ?m.4156
_ hu: ?m.4159
hu _: ?m.4162
_ hi: ?m.4165
hi =>
  ht: SupIndep t f
ht (hu: ?m.4159
hu.trans: ∀ {α : Type ?u.4168} [inst : HasSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊆ x_1] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
trans h: s ⊆ t
h) (h: s ⊆ t
h hi: ?m.4165
hi)
#align finset.sup_indep.subset Finset.SupIndep.subset: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s t : Finset ι} {f : ι → α},
  SupIndep t f → s ⊆ t → SupIndep s f
Finset.SupIndep.subset

theorem supIndep_empty: ∀ (f : ι → α), SupIndep ∅ f
supIndep_empty (f: ι → α
f : ι: Type ?u.4268
ι → α: Type ?u.4262
α) : (∅: ?m.4611
∅ : Finset: Type ?u.4609 → Type ?u.4609
Finset ι: Type ?u.4268
ι).SupIndep: {α : Type ?u.4657} → {ι : Type ?u.4656} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f := fun _: ?m.4742
_ _: ?m.4745
_ a: ?m.4748
a ha: ?m.4751
ha =>
  (not_mem_empty: ∀ {α : Type ?u.4753} (a : α), ¬a ∈ ∅
not_mem_empty a: ?m.4748
a ha: ?m.4751
ha).elim: ∀ {C : Sort ?u.4755}, False → C
elim
#align finset.sup_indep_empty Finset.supIndep_empty: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] (f : ι → α), SupIndep ∅ f
Finset.supIndep_empty

theorem supIndep_singleton: ∀ (i : ι) (f : ι → α), SupIndep {i} f
supIndep_singleton (i: ι
i : ι: Type ?u.4782
ι) (f: ι → α
f : ι: Type ?u.4782
ι → α: Type ?u.4776
α) : ({i: ι
i} : Finset: Type ?u.5125 → Type ?u.5125
Finset ι: Type ?u.4782
ι).SupIndep: {α : Type ?u.5152} → {ι : Type ?u.5151} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f :=
  fun s: ?m.5239
s hs: ?m.5242
hs j: ?m.5245
j hji: ?m.5248
hji hj: ?m.5251
hj => by
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) (sup s f)rw [α: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) (sup s f)eq_empty_of_ssubset_singleton: ∀ {α : Type ?u.5261} {s : Finset α} {x : α}, s ⊂ {x} → s = ∅
eq_empty_of_ssubset_singleton ⟨hs: s ⊆ {i}
hs, fun h: ?m.5285
h => hj: ¬j ∈ s
hj (h: ?m.5285
h hji: j ∈ {i}
hji)⟩,α: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) (sup ∅ f) α: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) (sup s f)sup_empty: ∀ {α : Type ?u.5299} {β : Type ?u.5300} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, sup ∅ f = ⊥
sup_emptyα: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) ⊥]α: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) ⊥
    α: Type u_1

β: Type ?u.4779

ι: Type u_2

ι': Type ?u.4785

inst✝¹: Lattice α

inst✝: OrderBot α

s✝, t: Finset ι

f✝: ι → α

i✝, i: ι

f: ι → α

s: Finset ι

hs: s ⊆ {i}

j: ι

hji: j ∈ {i}

hj: ¬j ∈ s

Disjoint (f j) (sup s f)exact disjoint_bot_right: ∀ {α : Type ?u.5445} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a ⊥
disjoint_bot_right
Goals accomplished! 🐙
#align finset.sup_indep_singleton Finset.supIndep_singleton: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] (i : ι) (f : ι → α), SupIndep {i} f
Finset.supIndep_singleton

theorem SupIndep.pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f → Set.PairwiseDisjoint (↑s) f
SupIndep.pairwiseDisjoint (hs: SupIndep s f
hs : s: Finset ι
s.SupIndep: {α : Type ?u.6186} → {ι : Type ?u.6185} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f) : (s: Finset ι
s : Set: Type ?u.6271 → Type ?u.6271
Set ι: Type ?u.5849
ι).PairwiseDisjoint: {α : Type ?u.6373} → {ι : Type ?u.6372} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f :=
  fun _: ?m.6758
_ ha: ?m.6761
ha _: ?m.6764
_ hb: ?m.6767
hb hab: ?m.6770
hab =>
    sup_singleton: ∀ {α : Type ?u.6772} {β : Type ?u.6773} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
  sup {b} f = f b
sup_singleton.subst: ∀ {α : Sort ?u.6830} {motive : α → Prop} {a b : α}, a = b → motive a → motive b
subst <| hs: SupIndep s f
hs (singleton_subset_iff: ∀ {α : Type ?u.6847} {s : Finset α} {a : α}, {a} ⊆ s ↔ a ∈ s
singleton_subset_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hb: ?m.6767
hb) ha: ?m.6761
ha <| not_mem_singleton: ∀ {α : Type ?u.6891} {a b : α}, ¬a ∈ {b} ↔ a ≠ b
not_mem_singleton.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hab: ?m.6770
hab
#align finset.sup_indep.pairwise_disjoint Finset.SupIndep.pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f → Set.PairwiseDisjoint (↑s) f
Finset.SupIndep.pairwiseDisjoint

/-- The RHS looks like the definition of `CompleteLattice.Independent`. -/
theorem supIndep_iff_disjoint_erase: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  [inst_2 : DecidableEq ι], SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (sup (erase s i) f)
supIndep_iff_disjoint_erase [DecidableEq: Sort ?u.7295 → Sort (max1?u.7295)
DecidableEq ι: Type ?u.6959
ι] :
    s: Finset ι
s.SupIndep: {α : Type ?u.7305} → {ι : Type ?u.7304} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f ↔ ∀ i: ?m.7339
i ∈ s: Finset ι
s, Disjoint: {α : Type ?u.7372} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (f: ι → α
f i: ?m.7339
i) ((s: Finset ι
s.erase: {α : Type ?u.7444} → [inst : DecidableEq α] → Finset α → α → Finset α
erase i: ?m.7339
i).sup: {α : Type ?u.7492} → {β : Type ?u.7491} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: ι → α
f) :=
  ⟨fun hs: ?m.7891
hs _: ?m.7894
_ hi: ?m.7897
hi => hs: ?m.7891
hs (erase_subset: ∀ {α : Type ?u.7900} [inst : DecidableEq α] (a : α) (s : Finset α), erase s a ⊆ s
erase_subset _: ?m.7901
_ _: Finset ?m.7901
_) hi: ?m.7897
hi (not_mem_erase: ∀ {α : Type ?u.8036} [inst : DecidableEq α] (a : α) (s : Finset α), ¬a ∈ erase s a
not_mem_erase _: ?m.8037
_ _: Finset ?m.8037
_), fun hs: ?m.8134
hs _: ?m.8139
_ ht: ?m.8142
ht i: ?m.8145
i hi: ?m.8148
hi hit: ?m.8151
hit =>
    (hs: ?m.8134
hs i: ?m.8145
i hi: ?m.8148
hi).mono_right: ∀ {α : Type ?u.8153} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a b
mono_right (sup_mono: ∀ {α : Type ?u.8246} {β : Type ?u.8245} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α},
  s₁ ⊆ s₂ → sup s₁ f ≤ sup s₂ f
sup_mono fun _: ?m.8317
_ hj: ?m.8320
hj => mem_erase: ∀ {α : Type ?u.8322} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ∈ erase s b ↔ a ≠ b ∧ a ∈ s
mem_erase.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨ne_of_mem_of_not_mem: ∀ {α : Type ?u.8417} {β : Type ?u.8418} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → ¬b ∈ s → a ≠ b
ne_of_mem_of_not_mem hj: ?m.8320
hj hit: ?m.8151
hit, ht: ?m.8142
ht hj: ?m.8320
hj⟩)⟩
#align finset.sup_indep_iff_disjoint_erase Finset.supIndep_iff_disjoint_erase: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  [inst_2 : DecidableEq ι], SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (sup (erase s i) f)
Finset.supIndep_iff_disjoint_erase

@[simp]
theorem supIndep_pair: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι] {i j : ι},
  i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))
supIndep_pair [DecidableEq: Sort ?u.9172 → Sort (max1?u.9172)
DecidableEq ι: Type ?u.8836
ι] {i: ι
i j: ι
j : ι: Type ?u.8836
ι} (hij: i ≠ j
hij : i: ι
i ≠ j: ι
j) :
    ({i: ι
i, j: ι
j} : Finset: Type ?u.9190 → Type ?u.9190
Finset ι: Type ?u.8836
ι).SupIndep: {α : Type ?u.9269} → {ι : Type ?u.9268} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f ↔ Disjoint: {α : Type ?u.9301} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (f: ι → α
f i: ι
i) (f: ι → α
f j: ι
j) :=
  ⟨fun h: ?m.9620
h => h: ?m.9620
h.pairwiseDisjoint: ∀ {α : Type ?u.9622} {ι : Type ?u.9623} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f → Set.PairwiseDisjoint (↑s) f
pairwiseDisjoint (by
Goals accomplished! 🐙 α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: SupIndep {i, j} f

i ∈ ↑{i, j}simp
Goals accomplished! 🐙) (by
Goals accomplished! 🐙 α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: SupIndep {i, j} f

j ∈ ↑{i, j}simp
Goals accomplished! 🐙) hij: i ≠ j
hij,
   fun h: ?m.9694
h => by
Goals accomplished! 🐙
    α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} frw [α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} fsupIndep_iff_disjoint_erase: ∀ {α : Type ?u.10249} {ι : Type ?u.10248} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  [inst_2 : DecidableEq ι], SupIndep s f ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (sup (erase s i) f)
supIndep_iff_disjoint_eraseα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

∀ (i_1 : ι), i_1 ∈ {i, j} → Disjoint (f i_1) (sup (erase {i, j} i_1) f)]α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

∀ (i_1 : ι), i_1 ∈ {i, j} → Disjoint (f i_1) (sup (erase {i, j} i_1) f)
    α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} fintro k: ι
k hk: k ∈ {i, j}
hkα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k ∈ {i, j}

Disjoint (f k) (sup (erase {i, j} k) f)
    α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} frw [α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k ∈ {i, j}

Disjoint (f k) (sup (erase {i, j} k) f)Finset.mem_insert: ∀ {α : Type ?u.10528} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ insert b s ↔ a = b ∨ a ∈ s
Finset.mem_insert,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k = i ∨ k ∈ {j}

Disjoint (f k) (sup (erase {i, j} k) f) α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k ∈ {i, j}

Disjoint (f k) (sup (erase {i, j} k) f)Finset.mem_singleton: ∀ {α : Type ?u.10702} {a b : α}, b ∈ {a} ↔ b = a
Finset.mem_singletonα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k = i ∨ k = j

Disjoint (f k) (sup (erase {i, j} k) f)]α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k = i ∨ k = j

Disjoint (f k) (sup (erase {i, j} k) f) at hk: k = i ∨ k ∈ {j}
hkα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

k: ι

hk: k = i ∨ k = j

Disjoint (f k) (sup (erase {i, j} k) f)
    α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} fobtain rfl: k = i
rflrfl | rfl: k = i ∨ k = j
 | rfl: k = j
rfl := hk: k = i ∨ k = j
hkα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

inlDisjoint (f k) (sup (erase {k, j} k) f)
α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

inrDisjoint (f k) (sup (erase {i, k} k) f)
    α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} f·α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

inlDisjoint (f k) (sup (erase {k, j} k) f) α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

inlDisjoint (f k) (sup (erase {k, j} k) f)
α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

inrDisjoint (f k) (sup (erase {i, k} k) f)convert h: Disjoint (f k) (f j)
h using 1α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5sup (erase {k, j} k) f = f j
      α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

inlDisjoint (f k) (sup (erase {k, j} k) f)rw [α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5sup (erase {k, j} k) f = f jFinset.erase_insert: ∀ {α : Type ?u.11436} [inst : DecidableEq α] {a : α} {s : Finset α}, ¬a ∈ s → erase (insert a s) a = s
Finset.erase_insert,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5sup {j} f = f j
α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5¬k ∈ {j} α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5sup (erase {k, j} k) f = f jFinset.sup_singleton: ∀ {α : Type ?u.11612} {β : Type ?u.11613} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
  sup {b} f = f b
Finset.sup_singletonα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5f j = f j
α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5¬k ∈ {j}]α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

h.e'_5¬k ∈ {j}
      α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

j, k: ι

hij: k ≠ j

h: Disjoint (f k) (f j)

inlDisjoint (f k) (sup (erase {k, j} k) f)simpa using hij: k ≠ j
hij
Goals accomplished! 🐙
    α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, j: ι

hij: i ≠ j

h: Disjoint (f i) (f j)

SupIndep {i, j} f·α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

inrDisjoint (f k) (sup (erase {i, k} k) f) α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

inrDisjoint (f k) (sup (erase {i, k} k) f)convert h: Disjoint (f i) (f k)
h.symm: ∀ {α : Type ?u.11850} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b a
symm using 1α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

h.e'_5sup (erase {i, k} k) f = f i
      α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

inrDisjoint (f k) (sup (erase {i, k} k) f)have : ({i: ι
i, k: ι
k} : Finset: Type ?u.12707 → Type ?u.12707
Finset ι: Type u_1
ι).erase: {α : Type ?u.12768} → [inst : DecidableEq α] → Finset α → α → Finset α
erase k: ι
k = {i: ι
i} := α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

h.e'_5sup (erase {i, k} k) f = f iby
Goals accomplished! 🐙
        α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

erase {i, k} k = {i}extα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}
        α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

erase {i, k} k = {i}rw [α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_erase: ∀ {α : Type ?u.12873} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ∈ erase s b ↔ a ≠ b ∧ a ∈ s
mem_erase,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ≠ k ∧ a✝ ∈ {i, k} ↔ a✝ ∈ {i} α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_insert: ∀ {α : Type ?u.13037} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ insert b s ↔ a = b ∨ a ∈ s
mem_insert,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ≠ k ∧ (a✝ = i ∨ a✝ ∈ {k}) ↔ a✝ ∈ {i} α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_singleton: ∀ {α : Type ?u.13201} {a b : α}, b ∈ {a} ↔ b = a
mem_singleton,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ≠ k ∧ (a✝ = i ∨ a✝ = k) ↔ a✝ ∈ {i} α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}mem_singleton: ∀ {α : Type ?u.13208} {a b : α}, b ∈ {a} ↔ b = a
mem_singleton,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ≠ k ∧ (a✝ = i ∨ a✝ = k) ↔ a✝ = i α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}and_or_left: ∀ {a b c : Prop}, a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c
and_or_left,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ≠ k ∧ a✝ = i ∨ a✝ ≠ k ∧ a✝ = k ↔ a✝ = i α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}Ne.def: ∀ {α : Sort ?u.13223} (a b : α), (a ≠ b) = ¬a = b
Ne.def,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

a¬a✝ = k ∧ a✝ = i ∨ ¬a✝ = k ∧ a✝ = k ↔ a✝ = i
          α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}not_and_self_iff: ∀ (a : Prop), ¬a ∧ a ↔ False
not_and_self_iff,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

a¬a✝ = k ∧ a✝ = i ∨ False ↔ a✝ = i α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}or_false_iff: ∀ (p : Prop), p ∨ False ↔ p
or_false_iff,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

a¬a✝ = k ∧ a✝ = i ↔ a✝ = i α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}and_iff_right_of_imp: ∀ {b a : Prop}, (b → a) → (a ∧ b ↔ b)
and_iff_right_of_impα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ = i ↔ a✝ = i
α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ = i → ¬a✝ = k]α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

a✝: ι

aa✝ = i → ¬a✝ = k
        α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

erase {i, k} k = {i}rintro rfl: ?m.13242
rflα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

inst✝: DecidableEq ι

k, a✝: ι

hij: a✝ ≠ k

h: Disjoint (f a✝) (f k)

a¬a✝ = k
        α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

erase {i, k} k = {i}exact hij: a✝ ≠ k
hij
Goals accomplished! 🐙
      α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

inrDisjoint (f k) (sup (erase {i, k} k) f)rw [α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

this: erase {i, k} k = {i}

h.e'_5sup (erase {i, k} k) f = f ithis: erase {i, k} k = ?m.12796
this,α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

this: erase {i, k} k = {i}

h.e'_5sup {i} f = f i α: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

this: erase {i, k} k = {i}

h.e'_5sup (erase {i, k} k) f = f iFinset.sup_singleton: ∀ {α : Type ?u.13280} {β : Type ?u.13281} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
  sup {b} f = f b
Finset.sup_singletonα: Type u_2

β: Type ?u.8833

ι: Type u_1

ι': Type ?u.8839

inst✝²: Lattice α

inst✝¹: OrderBot α

s, t: Finset ι

f: ι → α

i✝: ι

inst✝: DecidableEq ι

i, k: ι

hij: i ≠ k

h: Disjoint (f i) (f k)

this: erase {i, k} k = {i}

h.e'_5f i = f i]
Goals accomplished! 🐙⟩
#align finset.sup_indep_pair Finset.supIndep_pair: ∀ {α : Type u_2} {ι : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι] {i j : ι},
  i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))
Finset.supIndep_pair

theorem supIndep_univ_bool: ∀ (f : Bool → α), SupIndep univ f ↔ Disjoint (f false) (f true)
supIndep_univ_bool (f: Bool → α
f : Bool: Type
Bool → α: Type ?u.13540
α) :
    (Finset.univ: {α : Type ?u.13888} → [inst : Fintype α] → Finset α
Finset.univ : Finset: Type ?u.13887 → Type ?u.13887
Finset Bool: Type
Bool).SupIndep: {α : Type ?u.13925} → {ι : Type ?u.13924} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: Bool → α
f ↔ Disjoint: {α : Type ?u.13957} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (f: Bool → α
f false: Bool
false) (f: Bool → α
f true: Bool
true) :=
  haveI : true: Bool
true ≠ false: Bool
false := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.13543

ι: Type ?u.13546

ι': Type ?u.13549

inst✝¹: Lattice α

inst✝: OrderBot α

s, t: Finset ι

f✝: ι → α

i: ι

f: Bool → α

true ≠ falsesimp only [Ne.def: ∀ {α : Sort ?u.14822} (a b : α), (a ≠ b) = ¬a = b
Ne.def, not_false_iff: ¬False ↔ True
not_false_iff]
Goals accomplished! 🐙
  (supIndep_pair: ∀ {α : Type ?u.14268} {ι : Type ?u.14267} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι]
  {i j : ι}, i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))
supIndep_pair this: true ≠ false
this).trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans disjoint_comm: ∀ {α : Type ?u.14417} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ Disjoint b a
disjoint_comm
#align finset.sup_indep_univ_bool Finset.supIndep_univ_bool: ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Bool → α), SupIndep univ f ↔ Disjoint (f false) (f true)
Finset.supIndep_univ_bool

@[simp]
theorem supIndep_univ_fin_two: ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Fin 2 → α), SupIndep univ f ↔ Disjoint (f 0) (f 1)
supIndep_univ_fin_two (f: Fin 2 → α
f : Fin: ℕ → Type
Fin 2: ?m.15226
2 → α: Type ?u.14882
α) :
    (Finset.univ: {α : Type ?u.15243} → [inst : Fintype α] → Finset α
Finset.univ : Finset: Type ?u.15239 → Type ?u.15239
Finset (Fin: ℕ → Type
Fin 2: ?m.15241
2)).SupIndep: {α : Type ?u.15283} → {ι : Type ?u.15282} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: Fin 2 → α
f ↔ Disjoint: {α : Type ?u.15316} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (f: Fin 2 → α
f 0: ?m.15321
0) (f: Fin 2 → α
f 1: ?m.15347
1) :=
  haveI : (0: ?m.15668
0 : Fin: ℕ → Type
Fin 2: ?m.15665
2) ≠ 1: ?m.15671
1 := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.14885

ι: Type ?u.14888

ι': Type ?u.14891

inst✝¹: Lattice α

inst✝: OrderBot α

s, t: Finset ι

f✝: ι → α

i: ι

f: Fin 2 → α

0 ≠ 1simp
Goals accomplished! 🐙
  supIndep_pair: ∀ {α : Type ?u.15676} {ι : Type ?u.15675} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} [inst_2 : DecidableEq ι]
  {i j : ι}, i ≠ j → (SupIndep {i, j} f ↔ Disjoint (f i) (f j))
supIndep_pair this: 0 ≠ 1
this
#align finset.sup_indep_univ_fin_two Finset.supIndep_univ_fin_two: ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (f : Fin 2 → α), SupIndep univ f ↔ Disjoint (f 0) (f 1)
Finset.supIndep_univ_fin_two

theorem SupIndep.attach: SupIndep s f → SupIndep (Finset.attach s) (f ∘ Subtype.val)
SupIndep.attach (hs: SupIndep s f
hs : s: Finset ι
s.SupIndep: {α : Type ?u.16971} → {ι : Type ?u.16970} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f) : s: Finset ι
s.attach: {α : Type ?u.17055} → (s : Finset α) → Finset { x // x ∈ s }
attach.SupIndep: {α : Type ?u.17058} → {ι : Type ?u.17057} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep (f: ι → α
f ∘ Subtype.val: {α : Sort ?u.17129} → {p : α → Prop} → Subtype p → α
Subtype.val) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

hs: SupIndep s f

SupIndep (Finset.attach s) (f ∘ Subtype.val)intro t: Finset { x // x ∈ s }
t _: t ⊆ Finset.attach s
_ i: { x // x ∈ s }
i _: i ∈ Finset.attach s
_ hi: ¬i ∈ t
hiα: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))
  α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t: Finset ι

f: ι → α

i: ι

hs: SupIndep s f

SupIndep (Finset.attach s) (f ∘ Subtype.val)classical
    α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))rw [α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))← Finset.sup_image: ∀ {α : Type ?u.17170} {β : Type ?u.17168} {γ : Type ?u.17169} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α), sup (image f s) g = sup s (g ∘ f)
Finset.sup_imageα: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup (image Subtype.val t) f)]α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup (image Subtype.val t) f)
    α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))refine' hs: SupIndep s f
hs (image_subset_iff: ∀ {α : Type ?u.17646} {β : Type ?u.17645} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  image f s ⊆ t ↔ ∀ (x : α), x ∈ s → f x ∈ t
image_subset_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun (j: { x // x ∈ s }
j : { x: ?m.17746
x // x: ?m.17746
x ∈ s: Finset ι
s }) _: ?m.17768
_ => j: { x // x ∈ s }
j.2: ∀ {α : Sort ?u.17770} {p : α → Prop} (self : Subtype p), p ↑self
2) i: { x // x ∈ s }
i.2: ∀ {α : Sort ?u.17819} {p : α → Prop} (self : Subtype p), p ↑self
2 fun hi': ?m.17824
hi' => hi: ¬i ∈ t
hi _: i ∈ t
_α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

hi': ↑i ∈ image (fun j => ↑j) t

i ∈ t
    α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))rw [α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

hi': ↑i ∈ image (fun j => ↑j) t

i ∈ tmem_image: ∀ {α : Type ?u.17832} {β : Type ?u.17831} [inst : DecidableEq β] {f : α → β} {s : Finset α} {b : β},
  b ∈ image f s ↔ ∃ a, a ∈ s ∧ f a = b
mem_imageα: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

hi': ∃ a, a ∈ t ∧ ↑a = ↑i

i ∈ t]α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

hi': ∃ a, a ∈ t ∧ ↑a = ↑i

i ∈ t at hi': ?m.17824
hi'α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

hi': ∃ a, a ∈ t ∧ ↑a = ↑i

i ∈ t
    α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))obtain ⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i
⟨j: { x // x ∈ s }
j⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i
, hj: j ∈ t
hj⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i
, hji: ↑j = ↑i
hji⟨j, hj, hji⟩: ∃ a, a ∈ t ∧ ↑a = ↑i
⟩ := hi': ∃ a, a ∈ t ∧ ↑a = ↑i
hi'α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

j: { x // x ∈ s }

hj: j ∈ t

hji: ↑j = ↑i

intro.introi ∈ t
    α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

Disjoint ((f ∘ Subtype.val) i) (sup t (f ∘ Subtype.val))rwa [α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

j: { x // x ∈ s }

hj: j ∈ t

hji: ↑j = ↑i

intro.introi ∈ tSubtype.ext: ∀ {α : Sort ?u.18080} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext hji: ↑j = ↑i
hjiα: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

j: { x // x ∈ s }

hj: i ∈ t

hji: ↑j = ↑i

intro.introi ∈ t]α: Type u_1

β: Type ?u.16631

ι: Type u_2

ι': Type ?u.16637

inst✝¹: Lattice α

inst✝: OrderBot α

s, t✝: Finset ι

f: ι → α

i✝: ι

hs: SupIndep s f

t: Finset { x // x ∈ s }

a✝¹: t ⊆ Finset.attach s

i: { x // x ∈ s }

a✝: i ∈ Finset.attach s

hi: ¬i ∈ t

j: { x // x ∈ s }

hj: i ∈ t

hji: ↑j = ↑i

intro.introi ∈ t at hj: j ∈ t
hj
Goals accomplished! 🐙
#align finset.sup_indep.attach Finset.SupIndep.attach: ∀ {α : Type u_1} {ι : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f → SupIndep (attach s) (f ∘ Subtype.val)
Finset.SupIndep.attach

end Lattice

section DistribLattice

variable [DistribLattice: Type ?u.18176 → Type ?u.18176
DistribLattice α: Type ?u.22021
α] [OrderBot: (α : Type ?u.18572) → [inst : LE α] → Type ?u.18572
OrderBot α: Type ?u.18164
α] {s: Finset ι
s : Finset: Type ?u.20333 → Type ?u.20333
Finset ι: Type ?u.18563
ι} {f: ι → α
f : ι: Type ?u.18170
ι → α: Type ?u.18164
α}

theorem supIndep_iff_pairwiseDisjoint: SupIndep s f ↔ Set.PairwiseDisjoint (↑s) f
supIndep_iff_pairwiseDisjoint : s: Finset ι
s.SupIndep: {α : Type ?u.18951} → {ι : Type ?u.18950} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f ↔ (s: Finset ι
s : Set: Type ?u.19068 → Type ?u.19068
Set ι: Type ?u.18563
ι).PairwiseDisjoint: {α : Type ?u.19170} → {ι : Type ?u.19169} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint f: ι → α
f :=
  ⟨SupIndep.pairwiseDisjoint: ∀ {α : Type ?u.19523} {ι : Type ?u.19524} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f → Set.PairwiseDisjoint (↑s) f
SupIndep.pairwiseDisjoint, fun hs: ?m.19712
hs _: ?m.19715
_ ht: ?m.19718
ht _: ?m.19721
_ hi: ?m.19724
hi hit: ?m.19727
hit =>
    Finset.disjoint_sup_right: ∀ {α : Type ?u.19729} {ι : Type ?u.19730} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  {a : α}, Disjoint a (sup s f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)
Finset.disjoint_sup_right.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun _: ?m.19835
_ hj: ?m.19838
hj => hs: ?m.19712
hs hi: ?m.19724
hi (ht: ?m.19718
ht hj: ?m.19838
hj) (ne_of_mem_of_not_mem: ∀ {α : Type ?u.19856} {β : Type ?u.19857} [inst : Membership α β] {s : β} {a b : α}, a ∈ s → ¬b ∈ s → a ≠ b
ne_of_mem_of_not_mem hj: ?m.19838
hj hit: ?m.19727
hit).symm: ∀ {α : Sort ?u.19881} {a b : α}, a ≠ b → b ≠ a
symm⟩
#align finset.sup_indep_iff_pairwise_disjoint Finset.supIndep_iff_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f ↔ Set.PairwiseDisjoint (↑s) f
Finset.supIndep_iff_pairwiseDisjoint

alias supIndep_iff_pairwiseDisjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f ↔ Set.PairwiseDisjoint (↑s) f
supIndep_iff_pairwiseDisjoint ↔
  sup_indep.pairwise_disjoint: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f → Set.PairwiseDisjoint (↑s) f
sup_indep.pairwise_disjoint _root_.Set.PairwiseDisjoint.supIndep: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  Set.PairwiseDisjoint (↑s) f → SupIndep s f
_root_.Set.PairwiseDisjoint.supIndep
#align set.pairwise_disjoint.sup_indep Set.PairwiseDisjoint.supIndep: ∀ {α : Type u_1} {ι : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  Set.PairwiseDisjoint (↑s) f → SupIndep s f
Set.PairwiseDisjoint.supIndep

/-- Bind operation for `SupIndep`. -/
theorem SupIndep.sup: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
  {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (SupIndep s fun i => Finset.sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.sup s g) f
SupIndep.sup [DecidableEq: Sort ?u.20340 → Sort (max1?u.20340)
DecidableEq ι: Type ?u.19953
ι] {s: Finset ι'
s : Finset: Type ?u.20349 → Type ?u.20349
Finset ι': Type ?u.19956
ι'} {g: ι' → Finset ι
g : ι': Type ?u.19956
ι' → Finset: Type ?u.20354 → Type ?u.20354
Finset ι: Type ?u.19953
ι} {f: ι → α
f : ι: Type ?u.19953
ι → α: Type ?u.19947
α}
    (hs: SupIndep s fun i => Finset.sup (g i) f
hs : s: Finset ι'
s.SupIndep: {α : Type ?u.20362} → {ι : Type ?u.20361} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep fun i: ?m.20426
i => (g: ι' → Finset ι
g i: ?m.20426
i).sup: {α : Type ?u.20429} → {β : Type ?u.20428} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: ι → α
f) (hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
hg : ∀ i': ?m.20678
i' ∈ s: Finset ι'
s, (g: ι' → Finset ι
g i': ?m.20678
i').SupIndep: {α : Type ?u.20712} → {ι : Type ?u.20711} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f) :
    (s: Finset ι'
s.sup: {α : Type ?u.20782} → {β : Type ?u.20781} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup g: ι' → Finset ι
g).SupIndep: {α : Type ?u.20860} → {ι : Type ?u.20859} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f := by
Goals accomplished! 🐙
  α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.sup s g) fsimp_rw [α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.sup s g) fsupIndep_iff_pairwiseDisjoint: ∀ {α : Type ?u.21075} {ι : Type ?u.21076} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIndep s f ↔ Set.PairwiseDisjoint (↑s) f
supIndep_iff_pairwiseDisjointα: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (↑(Finset.sup s g)) f] at hs: SupIndep s fun i => Finset.sup (g i) f
hs hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
hg⊢α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (↑(Finset.sup s g)) f
  α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.sup s g) frw [α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (↑(Finset.sup s g)) fsup_eq_biUnion: ∀ {α : Type ?u.21418} {β : Type ?u.21419} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β),
  Finset.sup s t = Finset.biUnion s t
sup_eq_biUnion,α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (↑(Finset.biUnion s g)) f α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (↑(Finset.sup s g)) fcoe_biUnion: ∀ {α : Type ?u.21629} {β : Type ?u.21628} [inst : DecidableEq β] {s : Finset α} {t : α → Finset β},
  ↑(Finset.biUnion s t) = Set.iUnion fun x => Set.iUnion fun h => ↑(t x)
coe_biUnionα: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (Set.iUnion fun x => Set.iUnion fun h => ↑(g x)) f]α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f

Set.PairwiseDisjoint (Set.iUnion fun x => Set.iUnion fun h => ↑(g x)) f
  α: Type u_3

β: Type ?u.19950

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.sup s g) fexact hs: Set.PairwiseDisjoint ↑s fun i => Finset.sup (g i) f
hs.biUnion_finset: ∀ {α : Type ?u.21813} {ι : Type ?u.21812} {ι' : Type ?u.21811} [inst : Lattice α] [inst_1 : OrderBot α] {s : Set ι'}
  {g : ι' → Finset ι} {f : ι → α},
  (Set.PairwiseDisjoint s fun i' => Finset.sup (g i') f) →
    (∀ (i : ι'), i ∈ s → Set.PairwiseDisjoint (↑(g i)) f) →
      Set.PairwiseDisjoint (Set.iUnion fun i => Set.iUnion fun h => ↑(g i)) f
biUnion_finset hg: ∀ (i' : ι'), i' ∈ s → Set.PairwiseDisjoint (↑(g i')) f
hg
Goals accomplished! 🐙
#align finset.sup_indep.sup Finset.SupIndep.sup: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
  {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (SupIndep s fun i => sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (sup s g) f
Finset.SupIndep.sup

/-- Bind operation for `SupIndep`. -/
theorem SupIndep.biUnion: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
  {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (SupIndep s fun i => Finset.sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.biUnion s g) f
SupIndep.biUnion [DecidableEq: Sort ?u.22414 → Sort (max1?u.22414)
DecidableEq ι: Type ?u.22027
ι] {s: Finset ι'
s : Finset: Type ?u.22423 → Type ?u.22423
Finset ι': Type ?u.22030
ι'} {g: ι' → Finset ι
g : ι': Type ?u.22030
ι' → Finset: Type ?u.22428 → Type ?u.22428
Finset ι: Type ?u.22027
ι} {f: ι → α
f : ι: Type ?u.22027
ι → α: Type ?u.22021
α}
    (hs: SupIndep s fun i => Finset.sup (g i) f
hs : s: Finset ι'
s.SupIndep: {α : Type ?u.22436} → {ι : Type ?u.22435} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep fun i: ?m.22500
i => (g: ι' → Finset ι
g i: ?m.22500
i).sup: {α : Type ?u.22503} → {β : Type ?u.22502} → [inst : SemilatticeSup α] → [inst : OrderBot α] → Finset β → (β → α) → α
sup f: ι → α
f) (hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
hg : ∀ i': ?m.22752
i' ∈ s: Finset ι'
s, (g: ι' → Finset ι
g i': ?m.22752
i').SupIndep: {α : Type ?u.22786} → {ι : Type ?u.22785} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f) :
    (s: Finset ι'
s.biUnion: {α : Type ?u.22856} → {β : Type ?u.22855} → [inst : DecidableEq β] → Finset α → (α → Finset β) → Finset β
biUnion g: ι' → Finset ι
g).SupIndep: {α : Type ?u.22910} → {ι : Type ?u.22909} → [inst : Lattice α] → [inst : OrderBot α] → Finset ι → (ι → α) → Prop
SupIndep f: ι → α
f := by
Goals accomplished! 🐙
  α: Type u_3

β: Type ?u.22024

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.biUnion s g) frw [α: Type u_3

β: Type ?u.22024

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.biUnion s g) f← sup_eq_biUnion: ∀ {α : Type ?u.22996} {β : Type ?u.22997} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β),
  Finset.sup s t = Finset.biUnion s t
sup_eq_biUnionα: Type u_3

β: Type ?u.22024

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.sup s g) f]α: Type u_3

β: Type ?u.22024

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.sup s g) f
  α: Type u_3

β: Type ?u.22024

ι: Type u_1

ι': Type u_2

inst✝²: DistribLattice α

inst✝¹: OrderBot α

s✝: Finset ι

f✝: ι → α

inst✝: DecidableEq ι

s: Finset ι'

g: ι' → Finset ι

f: ι → α

hs: SupIndep s fun i => Finset.sup (g i) f

hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f

SupIndep (Finset.biUnion s g) fexact hs: SupIndep s fun i => Finset.sup (g i) f
hs.sup: ∀ {α : Type ?u.23205} {ι : Type ?u.23203} {ι' : Type ?u.23204} [inst : DistribLattice α] [inst_1 : OrderBot α]
  [inst_2 : DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (SupIndep s fun i => Finset.sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.sup s g) f
sup hg: ∀ (i' : ι'), i' ∈ s → SupIndep (g i') f
hg
Goals accomplished! 🐙
#align finset.sup_indep.bUnion Finset.SupIndep.biUnion: ∀ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq ι]
  {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (SupIndep s fun i => sup (g i) f) → (∀ (i' : ι'), i' ∈ s → SupIndep (g i') f) → SupIndep (Finset.biUnion s g) f
Finset.SupIndep.biUnion

end DistribLattice

end Finset

/-! ### On complete lattices via `sSup` -/


namespace CompleteLattice

variable [CompleteLattice: Type ?u.26923 → Type ?u.26923
CompleteLattice α: Type ?u.23352
α]

open Set Function

/-- An independent set of elements in a complete lattice is one in which every element is disjoint
  from the `Sup` of the rest. -/
def SetIndependent: {α : Type u_1} → [inst : CompleteLattice α] → Set α → Prop
SetIndependent (s: Set α
s : Set: Type ?u.23382 → Type ?u.23382
Set α: Type ?u.23367
α) : Prop: Type
Prop :=
  ∀ ⦃a: ?m.23388
a⦄, a: ?m.23388
a ∈ s: Set α
s → Disjoint: {α : Type ?u.23422} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint a: ?m.23388
a (sSup: {α : Type ?u.23497} → [self : SupSet α] → Set α → α
sSup (s: Set α
s \ {a: ?m.23388
a}))
#align complete_lattice.set_independent CompleteLattice.SetIndependent: {α : Type u_1} → [inst : CompleteLattice α] → Set α → Prop
CompleteLattice.SetIndependent

variable {s: Set α
s : Set: Type ?u.50592 → Type ?u.50592
Set α: Type ?u.50577
α} (hs: SetIndependent s
hs : SetIndependent: {α : Type ?u.36305} → [inst : CompleteLattice α] → Set α → Prop
SetIndependent s: Set α
s)

@[simp]
theorem setIndependent_empty: SetIndependent ∅
setIndependent_empty : SetIndependent: {α : Type ?u.23748} → [inst : CompleteLattice α] → Set α → Prop
SetIndependent (∅: ?m.23764
∅ : Set: Type ?u.23762 → Type ?u.23762
Set α: Type ?u.23706
α) := fun x: ?m.23817
x hx: ?m.23820
hx =>
  (Set.not_mem_empty: ∀ {α : Type ?u.23822} (x : α), ¬x ∈ ∅
Set.not_mem_empty x: ?m.23817
x hx: ?m.23820
hx).elim: ∀ {C : Sort ?u.23824}, False → C
elim
#align complete_lattice.set_independent_empty CompleteLattice.setIndependent_empty: ∀ {α : Type u_1} [inst : CompleteLattice α], SetIndependent ∅
CompleteLattice.setIndependent_empty

theorem SetIndependent.mono: ∀ {t : Set α}, t ⊆ s → SetIndependent t
SetIndependent.mono {t: Set α
t : Set: Type ?u.23891 → Type ?u.23891
Set α: Type ?u.23849
α} (hst: t ⊆ s
hst : t: Set α
t ⊆ s: Set α
s) : SetIndependent: {α : Type ?u.23915} → [inst : CompleteLattice α] → Set α → Prop
SetIndependent t: Set α
t := fun _: ?m.23942
_ ha: ?m.23945
ha =>
  (hs: SetIndependent s
hs (hst: t ⊆ s
hst ha: ?m.23945
ha)).mono_right: ∀ {α : Type ?u.23954} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a b
mono_right (sSup_le_sSup: ∀ {α : Type ?u.24054} [inst : CompleteSemilatticeSup α] {s t : Set α}, s ⊆ t → sSup s ≤ sSup t
sSup_le_sSup (diff_subset_diff_left: ∀ {α : Type ?u.24099} {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ \ t ⊆ s₂ \ t
diff_subset_diff_left hst: t ⊆ s
hst))
#align complete_lattice.set_independent.mono CompleteLattice.SetIndependent.mono: ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → ∀ {t : Set α}, t ⊆ s → SetIndependent t
CompleteLattice.SetIndependent.mono

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
theorem SetIndependent.pairwiseDisjoint: PairwiseDisjoint s id
SetIndependent.pairwiseDisjoint : s: Set α
s.PairwiseDisjoint: {α : Type ?u.24246} → {ι : Type ?u.24245} → [inst : PartialOrder α] → [inst : OrderBot α] → Set ι → (ι → α) → Prop
PairwiseDisjoint id: {α : Sort ?u.24329} → α → α
id := fun _: ?m.24409
_ hx: ?m.24412
hx y: ?m.24415
y hy: ?m.24418
hy h: ?m.24421
h =>
  disjoint_sSup_right: ∀ {α : Type ?u.24423} [inst : CompleteLattice α] {a : Set α} {b : α},
  Disjoint b (sSup a) → ∀ {i : α}, i ∈ a → Disjoint b i
disjoint_sSup_right (hs: SetIndependent s
hs hx: ?m.24412
hx) ((mem_diff: ∀ {α : Type ?u.24467} {s t : Set α} (x : α), x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t
mem_diff y: ?m.24415
y).mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨hy: ?m.24418
hy, h: ?m.24421
h.symm: ∀ {α : Sort ?u.24487} {a b : α}, a ≠ b → b ≠ a
symm⟩)
#align complete_lattice.set_independent.pairwise_disjoint CompleteLattice.SetIndependent.pairwiseDisjoint: ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → PairwiseDisjoint s id
CompleteLattice.SetIndependent.pairwiseDisjoint

theorem setIndependent_pair: ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, a ≠ b → (SetIndependent {a, b} ↔ Disjoint a b)
setIndependent_pair {a: α
a b: α
b : α: Type ?u.24525
α} (hab: a ≠ b
hab : a: α
a ≠ b: α
b) :
    SetIndependent: {α : Type ?u.24575} → [inst : CompleteLattice α] → Set α → Prop
SetIndependent ({a: α
a, b: α
b} : Set: Type ?u.24579 → Type ?u.24579
Set α: Type ?u.24525
α) ↔ Disjoint: {α : Type ?u.24636} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint a: α
a b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

SetIndependent {a, b} ↔ Disjoint a bconstructorα: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mpSetIndependent {a, b} → Disjoint a b
α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mprDisjoint a b → SetIndependent {a, b}
  α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

SetIndependent {a, b} ↔ Disjoint a b·α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mpSetIndependent {a, b} → Disjoint a b α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mpSetIndependent {a, b} → Disjoint a b
α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mprDisjoint a b → SetIndependent {a, b}intro h: ?a
hα: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

h: SetIndependent {a, b}

mpDisjoint a b
    α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mpSetIndependent {a, b} → Disjoint a bexact h: ?a
h.pairwiseDisjoint: ∀ {α : Type ?u.24730} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → PairwiseDisjoint s id
pairwiseDisjoint (mem_insert: ∀ {α : Type ?u.24753} (x : α) (s : Set α), x ∈ insert x s
mem_insert _: ?m.24754
_ _: Set ?m.24754
_) (mem_insert_of_mem: ∀ {α : Type ?u.24781} {x : α} {s : Set α} (y : α), x ∈ s → x ∈ insert y s
mem_insert_of_mem _: ?m.24782
_ (mem_singleton: ∀ {α : Type ?u.24786} (a : α), a ∈ {a}
mem_singleton _: ?m.24787
_)) hab: a ≠ b
hab
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

SetIndependent {a, b} ↔ Disjoint a b·α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mprDisjoint a b → SetIndependent {a, b} α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mprDisjoint a b → SetIndependent {a, b}rintro h: ?b
h c: α
c ((rfl : c = a) | (rfl : c = b)): c ∈ {a, b}
((rfl : c = a) | (rfl : c = b): c ∈ {a, b}
(rfl: c = a
rflrfl : c = a: c = a
 : c: α
crfl : c = a: c = a
 = a: α
a(rfl : c = a) | (rfl : c = b): c ∈ {a, b}
) | (rfl: c = b
rflrfl : c = b: c ∈ {b}
 : c: α
crfl : c = b: c ∈ {b}
 = b: α
b(rfl : c = a) | (rfl : c = b): c ∈ {a, b}
)((rfl : c = a) | (rfl : c = b)): c ∈ {a, b}
)α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

b, c: α

hab: c ≠ b

h: Disjoint c b

mpr.inlDisjoint c (sSup ({c, b} \ {c}))
α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, c: α

hab: a ≠ c

h: Disjoint a c

mpr.inrDisjoint c (sSup ({a, c} \ {c}))
    α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mprDisjoint a b → SetIndependent {a, b}·α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

b, c: α

hab: c ≠ b

h: Disjoint c b

mpr.inlDisjoint c (sSup ({c, b} \ {c})) α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

b, c: α

hab: c ≠ b

h: Disjoint c b

mpr.inlDisjoint c (sSup ({c, b} \ {c}))
α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, c: α

hab: a ≠ c

h: Disjoint a c

mpr.inrDisjoint c (sSup ({a, c} \ {c}))convert h: Disjoint c b
h using 1α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

b, c: α

hab: c ≠ b

h: Disjoint c b

h.e'_5sSup ({c, b} \ {c}) = b
      α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

b, c: α

hab: c ≠ b

h: Disjoint c b

mpr.inlDisjoint c (sSup ({c, b} \ {c}))simp [hab: c ≠ b
hab, sSup_singleton: ∀ {α : Type ?u.25195} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = a
sSup_singleton]
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, b: α

hab: a ≠ b

mprDisjoint a b → SetIndependent {a, b}·α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, c: α

hab: a ≠ c

h: Disjoint a c

mpr.inrDisjoint c (sSup ({a, c} \ {c})) α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, c: α

hab: a ≠ c

h: Disjoint a c

mpr.inrDisjoint c (sSup ({a, c} \ {c}))convert h: Disjoint a c
h.symm: ∀ {α : Type ?u.25691} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b a
symm using 1α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, c: α

hab: a ≠ c

h: Disjoint a c

h.e'_5sSup ({a, c} \ {c}) = a
      α: Type u_1

β: Type ?u.24528

ι: Type ?u.24531

ι': Type ?u.24534

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

a, c: α

hab: a ≠ c

h: Disjoint a c

mpr.inrDisjoint c (sSup ({a, c} \ {c}))simp [hab: a ≠ c
hab, sSup_singleton: ∀ {α : Type ?u.26033} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = a
sSup_singleton]
Goals accomplished! 🐙
#align complete_lattice.set_independent_pair CompleteLattice.setIndependent_pair: ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, a ≠ b → (SetIndependent {a, b} ↔ Disjoint a b)
CompleteLattice.setIndependent_pair

/-- If the elements of a set are independent, then any element is disjoint from the `sSup` of some
subset of the rest. -/
theorem SetIndependent.disjoint_sSup: ∀ {x : α} {y : Set α}, x ∈ s → y ⊆ s → ¬x ∈ y → Disjoint x (sSup y)
SetIndependent.disjoint_sSup {x: α
x : α: Type ?u.26448
α} {y: Set α
y : Set: Type ?u.26492 → Type ?u.26492
Set α: Type ?u.26448
α} (hx: x ∈ s
hx : x: α
x ∈ s: Set α
s) (hy: y ⊆ s
hy : y: Set α
y ⊆ s: Set α
s) (hxy: ¬x ∈ y
hxy : x: α
x ∉ y: Set α
y) :
    Disjoint: {α : Type ?u.26552} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint x: α
x (sSup: {α : Type ?u.26627} → [self : SupSet α] → Set α → α
sSup y: Set α
y) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

Disjoint x (sSup y)have := (hs: SetIndependent s
hs.mono: ∀ {α : Type ?u.26744} [inst : CompleteLattice α] {s : Set α}, SetIndependent s → ∀ {t : Set α}, t ⊆ s → SetIndependent t
mono <| insert_subset: ∀ {α : Type ?u.26766} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
insert_subset.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ⟨hx: x ∈ s
hx, hy: y ⊆ s
hy⟩) (mem_insert: ∀ {α : Type ?u.26803} (x : α) (s : Set α), x ∈ insert x s
mem_insert x: α
x _: Set ?m.26804
_)α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup (insert x y \ {x}))

Disjoint x (sSup y)
  α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

Disjoint x (sSup y)rw [α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup (insert x y \ {x}))

Disjoint x (sSup y)insert_diff_of_mem: ∀ {α : Type ?u.26820} {a : α} {t : Set α} (s : Set α), a ∈ t → insert a s \ t = s \ t
insert_diff_of_mem _: Set ?m.26821
_ (mem_singleton: ∀ {α : Type ?u.26825} (a : α), a ∈ {a}
mem_singleton _: ?m.26826
_),α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup (y \ {x}))

Disjoint x (sSup y) α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup (insert x y \ {x}))

Disjoint x (sSup y)diff_singleton_eq_self: ∀ {α : Type ?u.26869} {a : α} {s : Set α}, ¬a ∈ s → s \ {a} = s
diff_singleton_eq_self hxy: ¬x ∈ y
hxyα: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup y)

Disjoint x (sSup y)]α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup y)

Disjoint x (sSup y) at this: Disjoint x (sSup (y \ {x}))
thisα: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

this: Disjoint x (sSup y)

Disjoint x (sSup y)
  α: Type u_1

β: Type ?u.26451

ι: Type ?u.26454

ι': Type ?u.26457

inst✝: CompleteLattice α

s: Set α

hs: SetIndependent s

x: α

y: Set α

hx: x ∈ s

hy: y ⊆ s

hxy: ¬x ∈ y

Disjoint x (sSup y)exact this: Disjoint x (sSup y)
this
Goals accomplished! 🐙
#align complete_lattice.set_independent.disjoint_Sup CompleteLattice.SetIndependent.disjoint_sSup: ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α},
  SetIndependent s → ∀ {x : α} {y : Set α}, x ∈ s → y ⊆ s → ¬x ∈ y → Disjoint x (sSup y)
CompleteLattice.SetIndependent.disjoint_sSup

/-- An independent indexed family of elements in a complete lattice is one in which every element
  is disjoint from the `iSup` of the rest.

  Example: an indexed family of non-zero elements in a
  vector space is linearly independent iff the indexed family of subspaces they generate is
  independent in this sense.

  Example: an indexed family of submodules of a module is independent in this sense if
  and only the natural map from the direct sum of the submodules to the module is injective. -/
-- Porting note: needed to use `_H`
def Independent: {ι : Sort ?u.26953} → {α : Type ?u.26956} → [inst : CompleteLattice α] → (ι → α) → Prop
Independent {ι: Sort ?u.26953
ι : Sort _: Type ?u.26953
SortSort _: Type ?u.26953
 _} {α: Type ?u.26956
α : Type _: Type (?u.26956+1)
Type _} [CompleteLattice: Type ?u.26959 → Type ?u.26959
CompleteLattice α: Type ?u.26956
α] (t: ι → α
t : ι: Sort ?u.26953
ι → α: Type ?u.26956
α) :