[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : OrderBot α
s t : Finset ι
f : ι → α
i : ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
⊢ Decidable (SupIndep s f)
[PROOFSTEP]
refine @Finset.decidableForallOfDecidableSubsets _ _ _ (?_)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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))
[PROOFSTEP]
rintro t -
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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))
[PROOFSTEP]
refine @Finset.decidableDforallFinset _ _ _ (?_)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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))
[PROOFSTEP]
rintro i -
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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))
[PROOFSTEP]
have : Decidable (Disjoint (f i) (sup t f)) := decidable_of_iff' (_ = ⊥) disjoint_iff
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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)
[PROOFSTEP]
rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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) ⊥
[PROOFSTEP]
exact disjoint_bot_right
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : SupIndep s f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
⊢ f i ≤ sup t f ↔ i ∈ t
[PROOFSTEP]
refine' ⟨fun h => _, le_sup⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : SupIndep s f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ sup t f
⊢ i ∈ t
[PROOFSTEP]
by_contra hit
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : SupIndep s f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
h : f i ≤ sup t f
hit : ¬i ∈ t
⊢ False
[PROOFSTEP]
exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t : Finset ι
f : ι → α
i : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
⊢ SupIndep (Finset.image g s) f
[PROOFSTEP]
intro t ht i hi hit
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι
hi : i ∈ Finset.image g s
hit : ¬i ∈ t
⊢ Disjoint (f i) (sup t f)
[PROOFSTEP]
rw [mem_image] at hi
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι
hi : ∃ a, a ∈ s ∧ g a = i
hit : ¬i ∈ t
⊢ Disjoint (f i) (sup t f)
[PROOFSTEP]
obtain ⟨i, hi, rfl⟩ := hi
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
⊢ Disjoint (f (g i)) (sup t f)
[PROOFSTEP]
haveI : DecidableEq ι' := Classical.decEq _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
this : DecidableEq ι'
⊢ Disjoint (f (g i)) (sup t f)
[PROOFSTEP]
suffices hts : t ⊆ (s.erase i).image g
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
this : DecidableEq ι'
hts : t ⊆ Finset.image g (erase s i)
⊢ Disjoint (f (g i)) (sup t f)
[PROOFSTEP]
refine' (supIndep_iff_disjoint_erase.1 hs i hi).mono_right ((sup_mono hts).trans _)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
this : DecidableEq ι'
hts : t ⊆ Finset.image g (erase s i)
⊢ sup (Finset.image g (erase s i)) f ≤ sup (erase s i) (f ∘ g)
[PROOFSTEP]
rw [sup_image]
[GOAL]
case hts
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
this : DecidableEq ι'
⊢ t ⊆ Finset.image g (erase s i)
[PROOFSTEP]
rintro j hjt
[GOAL]
case hts
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
this : DecidableEq ι'
j : ι
hjt : j ∈ t
⊢ j ∈ Finset.image g (erase s i)
[PROOFSTEP]
obtain ⟨j, hj, rfl⟩ := mem_image.1 (ht hjt)
[GOAL]
case hts.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : SupIndep s (f ∘ g)
t : Finset ι
ht : t ⊆ Finset.image g s
i : ι'
hi : i ∈ s
hit : ¬g i ∈ t
this : DecidableEq ι'
j : ι'
hj : j ∈ s
hjt : g j ∈ t
⊢ g j ∈ Finset.image g (erase s i)
[PROOFSTEP]
exact mem_image_of_mem _ (mem_erase.2 ⟨ne_of_apply_ne g (ne_of_mem_of_not_mem hjt hit), hj⟩)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f : ι → α
i : ι
s : Finset ι'
g : ι' ↪ ι
⊢ SupIndep (map g s) f ↔ SupIndep s (f ∘ ↑g)
[PROOFSTEP]
refine' ⟨fun hs t ht i hi hit => _, fun hs => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
s : Finset ι'
g : ι' ↪ ι
hs : SupIndep (map g s) f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : ¬i ∈ t
⊢ Disjoint ((f ∘ ↑g) i) (sup t (f ∘ ↑g))
[PROOFSTEP]
rw [← sup_map]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
s : Finset ι'
g : ι' ↪ ι
hs : SupIndep (map g s) f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : ¬i ∈ t
⊢ Disjoint ((f ∘ ↑g) i) (sup (map g t) f)
[PROOFSTEP]
exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa [mem_map'])
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t✝ : Finset ι
f : ι → α
i✝ : ι
s : Finset ι'
g : ι' ↪ ι
hs : SupIndep (map g s) f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : ¬i ∈ t
⊢ ¬↑g i ∈ map g t
[PROOFSTEP]
rwa [mem_map']
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f : ι → α
i : ι
s : Finset ι'
g : ι' ↪ ι
hs : SupIndep s (f ∘ ↑g)
⊢ SupIndep (map g s) f
[PROOFSTEP]
classical
rw [map_eq_image]
exact hs.image
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f : ι → α
i : ι
s : Finset ι'
g : ι' ↪ ι
hs : SupIndep s (f ∘ ↑g)
⊢ SupIndep (map g s) f
[PROOFSTEP]
rw [map_eq_image]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f : ι → α
i : ι
s : Finset ι'
g : ι' ↪ ι
hs : SupIndep s (f ∘ ↑g)
⊢ SupIndep (image (↑g) s) f
[PROOFSTEP]
exact hs.image
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
h : SupIndep {i, j} f
⊢ i ∈ ↑{i, j}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
h : SupIndep {i, j} f
⊢ j ∈ ↑{i, j}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
[PROOFSTEP]
rw [supIndep_iff_disjoint_erase]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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)
[PROOFSTEP]
intro k hk
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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)
[PROOFSTEP]
rw [Finset.mem_insert, Finset.mem_singleton] at hk
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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)
[PROOFSTEP]
obtain rfl | rfl := hk
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
inst✝ : DecidableEq ι
j k : ι
hij : k ≠ j
h : Disjoint (f k) (f j)
⊢ Disjoint (f k) (sup (erase {k, j} k) f)
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
inst✝ : DecidableEq ι
j k : ι
hij : k ≠ j
h : Disjoint (f k) (f j)
⊢ sup (erase {k, j} k) f = f j
[PROOFSTEP]
rw [Finset.erase_insert, Finset.sup_singleton]
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
inst✝ : DecidableEq ι
j k : ι
hij : k ≠ j
h : Disjoint (f k) (f j)
⊢ ¬k ∈ {j}
[PROOFSTEP]
simpa using hij
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
i k : ι
hij : i ≠ k
h : Disjoint (f i) (f k)
⊢ Disjoint (f k) (sup (erase {i, k} k) f)
[PROOFSTEP]
convert h.symm using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
i k : ι
hij : i ≠ k
h : Disjoint (f i) (f k)
⊢ sup (erase {i, k} k) f = f i
[PROOFSTEP]
have : ({ i, k } : Finset ι).erase k = { i } := by
  ext
  rw [mem_erase, mem_insert, mem_singleton, mem_singleton, and_or_left, Ne.def, not_and_self_iff, or_false_iff,
    and_iff_right_of_imp]
  rintro rfl
  exact hij
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
i k : ι
hij : i ≠ k
h : Disjoint (f i) (f k)
a✝ : ι
⊢ a✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}
[PROOFSTEP]
rw [mem_erase, mem_insert, mem_singleton, mem_singleton, and_or_left, Ne.def, not_and_self_iff, or_false_iff,
  and_iff_right_of_imp]
[GOAL]
case a
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i✝ : ι
inst✝ : DecidableEq ι
i k : ι
hij : i ≠ k
h : Disjoint (f i) (f k)
a✝ : ι
⊢ a✝ = i → ¬a✝ = k
[PROOFSTEP]
rintro rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
inst✝ : DecidableEq ι
k a✝ : ι
hij : a✝ ≠ k
h : Disjoint (f a✝) (f k)
⊢ ¬a✝ = k
[PROOFSTEP]
exact hij
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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}
⊢ sup (erase {i, k} k) f = f i
[PROOFSTEP]
rw [this, Finset.sup_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f✝ : ι → α
i : ι
f : Bool → α
⊢ true ≠ false
[PROOFSTEP]
simp only [Ne.def, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f✝ : ι → α
i : ι
f : Fin 2 → α
⊢ 0 ≠ 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : SupIndep s f
⊢ SupIndep (Finset.attach s) fun a => f ↑a
[PROOFSTEP]
intro t _ i _ hi
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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 ((fun a => f ↑a) i) (sup t fun a => f ↑a)
[PROOFSTEP]
classical
have : (fun (a : { x // x ∈ s }) => f ↑a) = f ∘ (fun a : { x // x ∈ s } => ↑a) := rfl
rw [this, ← Finset.sup_image]
refine' hs (image_subset_iff.2 fun (j : { x // x ∈ s }) _ => j.2) i.2 fun hi' => hi _
rw [mem_image] at hi'
obtain ⟨j, hj, hji⟩ := hi'
rwa [Subtype.ext hji] at hj
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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 ((fun a => f ↑a) i) (sup t fun a => f ↑a)
[PROOFSTEP]
have : (fun (a : { x // x ∈ s }) => f ↑a) = f ∘ (fun a : { x // x ∈ s } => ↑a) := rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
this : (fun a => f ↑a) = f ∘ fun a => ↑a
⊢ Disjoint ((fun a => f ↑a) i) (sup t fun a => f ↑a)
[PROOFSTEP]
rw [this, ← Finset.sup_image]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
this : (fun a => f ↑a) = f ∘ fun a => ↑a
⊢ Disjoint ((f ∘ fun a => ↑a) i) (sup (Finset.image (fun a => ↑a) t) f)
[PROOFSTEP]
refine' hs (image_subset_iff.2 fun (j : { x // x ∈ s }) _ => j.2) i.2 fun hi' => hi _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
this : (fun a => f ↑a) = f ∘ fun a => ↑a
hi' : (fun a => ↑a) i ∈ Finset.image (fun j => ↑j) t
⊢ i ∈ t
[PROOFSTEP]
rw [mem_image] at hi'
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
this : (fun a => f ↑a) = f ∘ fun a => ↑a
hi' : ∃ a, a ∈ t ∧ ↑a = (fun a => ↑a) i
⊢ i ∈ t
[PROOFSTEP]
obtain ⟨j, hj, hji⟩ := hi'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
this : (fun a => f ↑a) = f ∘ fun a => ↑a
j : { x // x ∈ s }
hj : j ∈ t
hji : ↑j = (fun a => ↑a) i
⊢ i ∈ t
[PROOFSTEP]
rwa [Subtype.ext hji] at hj
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
⊢ (SupIndep (attach s) fun a => f ↑a) ↔ SupIndep s f
[PROOFSTEP]
refine' ⟨fun h t ht i his hit => _, SupIndep.attach⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t✝ : Finset ι
f : ι → α
i✝ : ι
h : SupIndep (attach s) fun a => f ↑a
t : Finset ι
ht : t ⊆ s
i : ι
his : i ∈ s
hit : ¬i ∈ t
⊢ Disjoint (f i) (sup t f)
[PROOFSTEP]
classical
convert
  h (filter_subset (fun (i : { x // x ∈ s }) => (i : ι) ∈ t) _) (mem_attach _ ⟨i, ‹_›⟩) fun hi =>
    hit <| by simpa using hi using
  1
refine' eq_of_forall_ge_iff _
simp only [Finset.sup_le_iff, mem_filter, mem_attach, true_and_iff, Function.comp_apply, Subtype.forall, Subtype.coe_mk]
exact fun a => forall_congr' fun j => ⟨fun h _ => h, fun h hj => h (ht hj) hj⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t✝ : Finset ι
f : ι → α
i✝ : ι
h : SupIndep (attach s) fun a => f ↑a
t : Finset ι
ht : t ⊆ s
i : ι
his : i ∈ s
hit : ¬i ∈ t
⊢ Disjoint (f i) (sup t f)
[PROOFSTEP]
convert
  h (filter_subset (fun (i : { x // x ∈ s }) => (i : ι) ∈ t) _) (mem_attach _ ⟨i, ‹_›⟩) fun hi =>
    hit <| by simpa using hi using
  1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t✝ : Finset ι
f : ι → α
i✝ : ι
h : SupIndep (attach s) fun a => f ↑a
t : Finset ι
ht : t ⊆ s
i : ι
his : i ∈ s
hit : ¬i ∈ t
hi : { val := i, property := his } ∈ filter (fun i => ↑i ∈ t) (attach s)
⊢ i ∈ t
[PROOFSTEP]
simpa using hi
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t✝ : Finset ι
f : ι → α
i✝ : ι
h : SupIndep (attach s) fun a => f ↑a
t : Finset ι
ht : t ⊆ s
i : ι
his : i ∈ s
hit : ¬i ∈ t
⊢ sup t f = sup (filter (fun i => ↑i ∈ t) (attach s)) fun a => f ↑a
[PROOFSTEP]
refine' eq_of_forall_ge_iff _
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t✝ : Finset ι
f : ι → α
i✝ : ι
h : SupIndep (attach s) fun a => f ↑a
t : Finset ι
ht : t ⊆ s
i : ι
his : i ∈ s
hit : ¬i ∈ t
⊢ ∀ (c : α), sup t f ≤ c ↔ (sup (filter (fun i => ↑i ∈ t) (attach s)) fun a => f ↑a) ≤ c
[PROOFSTEP]
simp only [Finset.sup_le_iff, mem_filter, mem_attach, true_and_iff, Function.comp_apply, Subtype.forall, Subtype.coe_mk]
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t✝ : Finset ι
f : ι → α
i✝ : ι
h : SupIndep (attach s) fun a => f ↑a
t : Finset ι
ht : t ⊆ s
i : ι
his : i ∈ s
hit : ¬i ∈ t
⊢ ∀ (c : α), (∀ (b : ι), b ∈ t → f b ≤ c) ↔ ∀ (a : ι), a ∈ s → a ∈ t → f a ≤ c
[PROOFSTEP]
exact fun a => forall_congr' fun j => ⟨fun h _ => h, fun h hj => h (ht hj) hj⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
[PROOFSTEP]
simp_rw [supIndep_iff_pairwiseDisjoint] at hs hg ⊢
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
[PROOFSTEP]
rw [sup_eq_biUnion, coe_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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 (⋃ (x : ι') (_ : x ∈ ↑s), ↑(g x)) f
[PROOFSTEP]
exact hs.biUnion_finset hg
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
[PROOFSTEP]
rw [← sup_eq_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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
[PROOFSTEP]
exact hs.sup hg
[GOAL]
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
⊢ SupIndep (Finset.sigma s g) f
[PROOFSTEP]
rintro t ht ⟨i, b⟩ hi hit
[GOAL]
case mk
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b } ∈ Finset.sigma s g
hit : ¬{ fst := i, snd := b } ∈ t
⊢ Disjoint (f { fst := i, snd := b }) (Finset.sup t f)
[PROOFSTEP]
rw [Finset.disjoint_sup_right]
[GOAL]
case mk
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b } ∈ Finset.sigma s g
hit : ¬{ fst := i, snd := b } ∈ t
⊢ ∀ ⦃i_1 : (i : ι) × β i⦄, i_1 ∈ t → Disjoint (f { fst := i, snd := b }) (f i_1)
[PROOFSTEP]
rintro ⟨j, c⟩ hj
[GOAL]
case mk.mk
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b } ∈ Finset.sigma s g
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hj : { fst := j, snd := c } ∈ t
⊢ Disjoint (f { fst := i, snd := b }) (f { fst := j, snd := c })
[PROOFSTEP]
have hbc := (ne_of_mem_of_not_mem hj hit).symm
[GOAL]
case mk.mk
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b } ∈ Finset.sigma s g
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hj : { fst := j, snd := c } ∈ t
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
⊢ Disjoint (f { fst := i, snd := b }) (f { fst := j, snd := c })
[PROOFSTEP]
replace hj := ht hj
[GOAL]
case mk.mk
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b } ∈ Finset.sigma s g
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c } ∈ Finset.sigma s g
⊢ Disjoint (f { fst := i, snd := b }) (f { fst := j, snd := c })
[PROOFSTEP]
rw [mem_sigma] at hi hj
[GOAL]
case mk.mk
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c }.fst ∈ s ∧ { fst := j, snd := c }.snd ∈ g { fst := j, snd := c }.fst
⊢ Disjoint (f { fst := i, snd := b }) (f { fst := j, snd := c })
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case mk.mk.inl
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
c : β i
hbc : { fst := i, snd := b } ≠ { fst := i, snd := c }
hj : { fst := i, snd := c }.fst ∈ s ∧ { fst := i, snd := c }.snd ∈ g { fst := i, snd := c }.fst
⊢ Disjoint (f { fst := i, snd := b }) (f { fst := i, snd := c })
[PROOFSTEP]
exact (hg _ hj.1).pairwiseDisjoint hi.2 hj.2 (sigma_mk_injective.ne_iff.1 hbc)
[GOAL]
case mk.mk.inr
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c }.fst ∈ s ∧ { fst := j, snd := c }.snd ∈ g { fst := j, snd := c }.fst
hij : i ≠ j
⊢ Disjoint (f { fst := i, snd := b }) (f { fst := j, snd := c })
[PROOFSTEP]
refine' (hs.pairwiseDisjoint hi.1 hj.1 hij).mono _ _
[GOAL]
case mk.mk.inr.refine'_1
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c }.fst ∈ s ∧ { fst := j, snd := c }.snd ∈ g { fst := j, snd := c }.fst
hij : i ≠ j
⊢ f { fst := i, snd := b } ≤ (fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }) { fst := i, snd := b }.fst
[PROOFSTEP]
convert le_sup (α := α) hi.2
[GOAL]
case h.e'_3
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c }.fst ∈ s ∧ { fst := j, snd := c }.snd ∈ g { fst := j, snd := c }.fst
hij : i ≠ j
⊢ f { fst := i, snd := b } = f { fst := { fst := i, snd := b }.fst, snd := { fst := i, snd := b }.snd }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.refine'_2
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c }.fst ∈ s ∧ { fst := j, snd := c }.snd ∈ g { fst := j, snd := c }.fst
hij : i ≠ j
⊢ f { fst := j, snd := c } ≤ (fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }) { fst := j, snd := c }.fst
[PROOFSTEP]
convert le_sup (α := α) hj.2
[GOAL]
case h.e'_3
α : Type u_1
β✝ : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : SupIndep s fun i => Finset.sup (g i) fun b => f { fst := i, snd := b }
hg : ∀ (i : ι), i ∈ s → SupIndep (g i) fun b => f { fst := i, snd := b }
t : Finset ((i : ι) × β i)
ht : t ⊆ Finset.sigma s g
i : ι
b : β i
hi : { fst := i, snd := b }.fst ∈ s ∧ { fst := i, snd := b }.snd ∈ g { fst := i, snd := b }.fst
hit : ¬{ fst := i, snd := b } ∈ t
j : ι
c : β j
hbc : { fst := i, snd := b } ≠ { fst := j, snd := c }
hj : { fst := j, snd := c }.fst ∈ s ∧ { fst := j, snd := c }.snd ∈ g { fst := j, snd := c }.fst
hij : i ≠ j
⊢ f { fst := j, snd := c } = f { fst := { fst := j, snd := c }.fst, snd := { fst := j, snd := c }.snd }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
⊢ SupIndep (s ×ˢ t) f
[PROOFSTEP]
rintro u hu ⟨i, i'⟩ hi hiu
[GOAL]
case mk
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : ¬(i, i') ∈ u
⊢ Disjoint (f (i, i')) (Finset.sup u f)
[PROOFSTEP]
rw [Finset.disjoint_sup_right]
[GOAL]
case mk
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : ¬(i, i') ∈ u
⊢ ∀ ⦃i_1 : ι × ι'⦄, i_1 ∈ u → Disjoint (f (i, i')) (f i_1)
[PROOFSTEP]
rintro ⟨j, j'⟩ hj
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hj : (j, j') ∈ u
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
have hij := (ne_of_mem_of_not_mem hj hiu).symm
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hj : (j, j') ∈ u
hij : (i, i') ≠ (j, j')
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
replace hj := hu hj
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij : (i, i') ≠ (j, j')
hj : (j, j') ∈ s ×ˢ t
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
rw [mem_product] at hi hj
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij : (i, i') ≠ (j, j')
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
⊢ Disjoint (f (i, i')) (f (i, j'))
[PROOFSTEP]
refine' (ht.pairwiseDisjoint hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 hij).mono _ _
[GOAL]
case mk.mk.inl.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
⊢ f (i, i') ≤ (fun i' => Finset.sup s fun i => f (i, i')) (i, i').snd
[PROOFSTEP]
convert le_sup (α := α) hi.1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
⊢ f (i, i') = f ((i, i').fst, (i, i').snd)
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inl.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
⊢ f (i, j') ≤ (fun i' => Finset.sup s fun i => f (i, i')) (i, j').snd
[PROOFSTEP]
convert le_sup (α := α) hj.1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
⊢ f (i, j') = f ((i, j').fst, (i, j').snd)
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
hij : i ≠ j
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
refine' (hs.pairwiseDisjoint hi.1 hj.1 hij).mono _ _
[GOAL]
case mk.mk.inr.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => Finset.sup t fun i' => f (i, i')) (i, i').fst
[PROOFSTEP]
convert le_sup (α := α) hi.2
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
hij : i ≠ j
⊢ f (i, i') = f ((i, i').fst, (i, i').snd)
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => Finset.sup t fun i' => f (i, i')) (j, j').fst
[PROOFSTEP]
convert le_sup (α := α) hj.2
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : SupIndep s fun i => Finset.sup t fun i' => f (i, i')
ht : SupIndep t fun i' => Finset.sup s fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
hiu : ¬(i, i') ∈ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
hij : i ≠ j
⊢ f (j, j') = f ((j, j').fst, (j, j').snd)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ SupIndep (Finset.product s t) f ↔
    (SupIndep s fun i => sup t fun i' => f (i, i')) ∧ SupIndep t fun i' => sup s fun i => f (i, i')
[PROOFSTEP]
refine' ⟨_, fun h => h.1.product h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ SupIndep (Finset.product s t) f →
    (SupIndep s fun i => sup t fun i' => f (i, i')) ∧ SupIndep t fun i' => sup s fun i => f (i, i')
[PROOFSTEP]
simp_rw [supIndep_iff_pairwiseDisjoint]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ Set.PairwiseDisjoint (↑(Finset.product s t)) f →
    (Set.PairwiseDisjoint ↑s fun i => sup t fun i' => f (i, i')) ∧
      Set.PairwiseDisjoint ↑t fun i' => sup s fun i => f (i, i')
[PROOFSTEP]
refine' fun h => ⟨fun i hi j hj hij => _, fun i hi j hj hij => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : Set.PairwiseDisjoint (↑(Finset.product s t)) f
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i => sup t fun i' => f (i, i')) i j
[PROOFSTEP]
simp_rw [Function.onFun, Finset.disjoint_sup_left, Finset.disjoint_sup_right]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : Set.PairwiseDisjoint (↑(Finset.product s t)) f
i : ι'
hi : i ∈ ↑t
j : ι'
hj : j ∈ ↑t
hij : i ≠ j
⊢ (Disjoint on fun i' => sup s fun i => f (i, i')) i j
[PROOFSTEP]
simp_rw [Function.onFun, Finset.disjoint_sup_left, Finset.disjoint_sup_right]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : Set.PairwiseDisjoint (↑(Finset.product s t)) f
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃i_1 : ι'⦄, i_1 ∈ t → ∀ ⦃i_2 : ι'⦄, i_2 ∈ t → Disjoint (f (i, i_1)) (f (j, i_2))
[PROOFSTEP]
intro i' hi' j' hj'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : Set.PairwiseDisjoint (↑(Finset.product s t)) f
i : ι'
hi : i ∈ ↑t
j : ι'
hj : j ∈ ↑t
hij : i ≠ j
⊢ ∀ ⦃i_1 : ι⦄, i_1 ∈ s → ∀ ⦃i_2 : ι⦄, i_2 ∈ s → Disjoint (f (i_1, i)) (f (i_2, j))
[PROOFSTEP]
intro i' hi' j' hj'
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : Set.PairwiseDisjoint (↑(Finset.product s t)) f
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne Prod.fst hij)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
f✝ : ι → α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : Set.PairwiseDisjoint (↑(Finset.product s t)) f
i : ι'
hi : i ∈ ↑t
j : ι'
hj : j ∈ ↑t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))
[PROOFSTEP]
exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne Prod.snd hij)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ SetIndependent {a, b} ↔ Disjoint a b
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ SetIndependent {a, b} → Disjoint a b
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
h : SetIndependent {a, b}
⊢ Disjoint a b
[PROOFSTEP]
exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab
[GOAL]
case mpr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ Disjoint a b → SetIndependent {a, b}
[PROOFSTEP]
rintro h c ((rfl : c = a) | (rfl : c = b))
[GOAL]
case mpr.inl
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b
[PROOFSTEP]
simp [hab, sSup_singleton]
[GOAL]
case mpr.inr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))
[PROOFSTEP]
convert h.symm using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a
[PROOFSTEP]
simp [hab, sSup_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : ¬x ∈ y
⊢ Disjoint x (sSup y)
[PROOFSTEP]
have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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)
[PROOFSTEP]
rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
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)
[PROOFSTEP]
exact this
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ SetIndependent s ↔ Independent Subtype.val
[PROOFSTEP]
simp_rw [Independent, SetIndependent, SetCoe.forall, sSup_eq_iSup]
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ (a_2 : α) (_ : a_2 ∈ s \ {a}), a_2)) ↔
    ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := x, property := h }), ↑j)
[PROOFSTEP]
refine' forall₂_congr fun a ha => _
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ (a_1 : α) (_ : a_1 ∈ s \ {a}), a_1) ↔
    Disjoint a (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := ha }), ↑j)
[PROOFSTEP]
simp [iSup_subtype, iSup_and]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))
[PROOFSTEP]
simp_rw [sSup_image]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (a : ι) (_ : a ∈ {j | j ≠ i}), t a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j x, t j = a})
[PROOFSTEP]
rw [independent_def']
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
⊢ (∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j x, t j = a})
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι'✝ : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : Independent t
hf : Injective f
i : ι'
⊢ ⨆ (j : ι') (_ : j ≠ i), (t ∘ f) j ≤ ⨆ (j : ι) (_ : j ≠ f i), t j
[PROOFSTEP]
refine' (iSup_mono fun i => _).trans (iSup_comp_le _ f)
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι'✝ : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : Independent t
hf : Injective f
i✝ i : ι'
⊢ ⨆ (_ : i ≠ i✝), (t ∘ f) i ≤ ⨆ (_ : f i ≠ f i✝), t (f i)
[PROOFSTEP]
exact iSup_const_mono hf.ne
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι'✝ : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
⊢ Independent t
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι'✝ : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ (j : ι) (_ : j ≠ i), t j)
[PROOFSTEP]
obtain ⟨i', rfl⟩ := hf i
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι'✝ : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (j : ι) (_ : j ≠ f i'), t j)
[PROOFSTEP]
rw [← hf.iSup_comp]
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι'✝ : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : Independent (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (x : ι') (_ : f x ≠ f i'), t (f x))
[PROOFSTEP]
exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
⊢ SetIndependent (range t)
[PROOFSTEP]
rw [setIndependent_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
⊢ Independent Subtype.val
[PROOFSTEP]
rw [← coe_comp_rangeFactorization t] at ht
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ : Independent t
ht : Independent (Subtype.val ∘ rangeFactorization t)
⊢ Independent Subtype.val
[PROOFSTEP]
exact ht.comp' surjective_onto_range
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Injective t
[PROOFSTEP]
intro i j h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
⊢ i = j
[PROOFSTEP]
by_contra' contra
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : i ≠ j
⊢ False
[PROOFSTEP]
apply h_ne_bot j
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : i ≠ j
⊢ t j = ⊥
[PROOFSTEP]
suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
  replace ht := (ht i).mono_right this
  rwa [h, disjoint_self] at ht
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι) (_ : k ≠ i), t k
⊢ t j = ⊥
[PROOFSTEP]
replace ht := (ht i).mono_right this
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι) (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
⊢ t j = ⊥
[PROOFSTEP]
rwa [h, disjoint_self] at ht
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : i ≠ j
⊢ t j ≤ ⨆ (k : ι) (_ : k ≠ i), t k
[PROOFSTEP]
replace contra : j ≠ i
[GOAL]
case contra
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : i ≠ j
⊢ j ≠ i
[PROOFSTEP]
exact Ne.symm contra
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
i j : ι
h : t i = t j
contra : j ≠ i
⊢ t j ≤ ⨆ (k : ι) (_ : k ≠ i), t k
[PROOFSTEP]
exact @le_iSup₂ _ _ _ _ (fun x _ => t x) j contra
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Independent t ↔ Disjoint (t i) (t j)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Independent t → Disjoint (t i) (t j)
[PROOFSTEP]
exact fun h => h.pairwiseDisjoint hij
[GOAL]
case mpr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → Independent t
[PROOFSTEP]
rintro h k
[GOAL]
case mpr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
h : Disjoint (t i) (t j)
k : ι
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
[PROOFSTEP]
obtain rfl | rfl := huniv k
[GOAL]
case mpr.inl
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
[PROOFSTEP]
refine' h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le _)
[GOAL]
case mpr.inl
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t i = t j
[PROOFSTEP]
rw [(huniv i).resolve_left hi]
[GOAL]
case mpr.inr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
[PROOFSTEP]
refine' h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le _)
[GOAL]
case mpr.inr
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
j : ι
hj : j ≠ k
⊢ t j = t i
[PROOFSTEP]
rw [(huniv j).resolve_right hj]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ Finset.SupIndep s f
[PROOFSTEP]
classical
rw [Finset.supIndep_iff_disjoint_erase]
refine' Subtype.forall.trans (forall₂_congr fun a b => _)
rw [Finset.sup_eq_iSup]
congr! 1
refine' iSup_subtype.trans _
congr! 1
simp [iSup_and, @iSup_comm _ (_ ∈ s)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ Finset.SupIndep s f
[PROOFSTEP]
rw [Finset.supIndep_iff_disjoint_erase]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (Finset.sup (Finset.erase s i) f)
[PROOFSTEP]
refine' Subtype.forall.trans (forall₂_congr fun a b => _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) { val := a, property := b })
      (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (Finset.sup (Finset.erase s a) f)
[PROOFSTEP]
rw [Finset.sup_eq_iSup]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) { val := a, property := b })
      (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1)
[PROOFSTEP]
congr! 1
[GOAL]
case a.h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j =
    ⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1
[PROOFSTEP]
refine' iSup_subtype.trans _
[GOAL]
case a.h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ (i : ι) (h : i ∈ s) (_ : { val := i, property := h } ≠ { val := a, property := b }),
      (f ∘ Subtype.val) { val := i, property := h } =
    ⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1
[PROOFSTEP]
congr! 1
[GOAL]
case a.h.e'_5.h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (fun i =>
      ⨆ (h : i ∈ s) (_ : { val := i, property := h } ≠ { val := a, property := b }),
        (f ∘ Subtype.val) { val := i, property := h }) =
    fun a_1 => ⨆ (_ : a_1 ∈ Finset.erase s a), f a_1
[PROOFSTEP]
simp [iSup_and, @iSup_comm _ (_ ∈ s)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ Independent f ↔ Finset.SupIndep Finset.univ f
[PROOFSTEP]
classical simp [Finset.supIndep_iff_disjoint_erase, CompleteLattice.Independent, Finset.sup_eq_iSup]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ Independent f ↔ Finset.SupIndep Finset.univ f
[PROOFSTEP]
simp [Finset.supIndep_iff_disjoint_erase, CompleteLattice.Independent, Finset.sup_eq_iSup]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a✝ b : α
s : Finset β
hs : Finset.Nonempty s
f : β → α
a : α
⊢ sup' s hs f ≤ a ↔ sSup (f '' ↑s) ≤ a
[PROOFSTEP]
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (hs.to_set.image f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
s : Finset α
hs : Finset.Nonempty s
⊢ sup' s hs id = sSup ↑s
[PROOFSTEP]
rw [hs.sup'_eq_cSup_image, Set.image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ sSup ↑s ∈ s
[PROOFSTEP]
rw [h.cSup_eq_max']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
s✝ t : Set α
a b : α
s : Finset α
h : Finset.Nonempty s
⊢ max' s h ∈ s
[PROOFSTEP]
exact s.max'_mem _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
h : Set.Nonempty s
hs : Set.Finite s
⊢ sSup s ∈ s
[PROOFSTEP]
lift s to Finset α using hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
a b : α
s : Finset α
h : Set.Nonempty ↑s
⊢ sSup ↑s ∈ ↑s
[PROOFSTEP]
exact Finset.Nonempty.cSup_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f = sSup (f '' ↑s)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sup' s H f ≤ sSup (f '' ↑s)
[PROOFSTEP]
refine' Finset.sup'_le _ _ fun a ha => _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ f a ≤ sSup (f '' ↑s)
[PROOFSTEP]
refine' le_csSup ⟨s.sup' H f, _⟩ ⟨a, ha, rfl⟩
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
⊢ sup' s H f ∈ upperBounds (f '' ↑s)
[PROOFSTEP]
rintro i ⟨j, hj, rfl⟩
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ s
j : α
hj : j ∈ ↑s
⊢ f j ≤ sup' s H f
[PROOFSTEP]
exact Finset.le_sup' _ hj
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ sSup (f '' ↑s) ≤ sup' s H f
[PROOFSTEP]
apply csSup_le ((coe_nonempty.mpr H).image _)
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
⊢ ∀ (b : β), b ∈ f '' ↑s → b ≤ sup' s H f
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice β
s : Finset α
H : Finset.Nonempty s
f : α → β
a : α
ha : a ∈ ↑s
⊢ f a ≤ sup' s H f
[PROOFSTEP]
exact Finset.le_sup' _ ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
s : Finset α
H : Finset.Nonempty s
⊢ sup' s H id = sSup ↑s
[PROOFSTEP]
rw [sup'_eq_csSup_image s H, Set.image_id]