α : 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)
intro t _ i _ hi
no goals
α : 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))
classical
  rw [← 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
α : 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))
rw [← 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
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 (image Subtype.val t) f)
refine' hs (image_subset_iff.2 fun (j : { x // x ∈ s }) _ => j.2) i.2 fun hi' => 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
hi' : ↑i ∈ image (fun j => ↑j) t
⊢ i ∈ t
rw [mem_image] at hi'
case intro.intro
α : 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
⊢ 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
obtain ⟨j, hj, hji⟩ := hi'
no goals
case intro.intro
α : 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
⊢ i ∈ t
rwa [Subtype.ext hji] at hj