no goals
α : 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
no goals
α : 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
α : 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} f
rw [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)
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)
⊢ ∀ (i_1 : ι), i_1 ∈ {i, j} → Disjoint (f i_1) (sup (erase {i, j} i_1) f)
intro k 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)
k : ι
hk : k ∈ {i, j}
⊢ Disjoint (f k) (sup (erase {i, j} k) f)
rw [Finset.mem_insert, Finset.mem_singleton] at hk
case inl
α : 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)
⊢ Disjoint (f k) (sup (erase {k, j} k) f)

case inr
α : 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)
⊢ Disjoint (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)
k : ι
hk : k = i ∨ k = j
⊢ Disjoint (f k) (sup (erase {i, j} k) f)
obtain rfl | rfl := hk
case h.e'_5
α : 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)
⊢ sup (erase {k, j} k) f = f j
case inl
α : 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)
⊢ Disjoint (f k) (sup (erase {k, j} k) f)
convert h using 1
case h.e'_5
α : 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)
⊢ ¬k ∈ {j}
case h.e'_5
α : 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)
⊢ sup (erase {k, j} k) f = f j
rw [Finset.erase_insert, Finset.sup_singleton]
no goals
case h.e'_5
α : 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)
⊢ ¬k ∈ {j}
simpa using hij
case h.e'_5
α : 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)
⊢ sup (erase {i, k} k) f = f i
case inr
α : 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)
⊢ Disjoint (f k) (sup (erase {i, k} k) f)
convert h.symm using 1
case h.e'_5
α : 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}
⊢ sup (erase {i, k} k) f = f i
case h.e'_5
α : 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)
⊢ sup (erase {i, k} k) f = f i
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
no goals
case h.e'_5
α : 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}
⊢ sup (erase {i, k} k) f = f i
rw [this, Finset.sup_singleton]
case a
α : 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✝ ∈ 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}
ext
case a
α : 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✝ = i → ¬a✝ = k
case a
α : 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✝ ∈ erase {i, k} k ↔ a✝ ∈ {i}
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]
case a
α : 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✝ = k
case a
α : 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✝ = i → ¬a✝ = k
rintro rfl
no goals
case a
α : 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✝ = k
exact hij