α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht✝ ht : Independent t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Injective t
intro i j h
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
by_contra' contra
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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 = ⊥
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
apply h_ne_bot j
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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 = ⊥
suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
  replace ht := (ht i).mono_right this
  rwa [h, disjoint_self] at ht
case contra
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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

α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
replace contra : j ≠ i
no goals
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
exact @le_iSup₂ _ _ _ _ (fun x _ => t x) j contra
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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 = ⊥
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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 = ⊥
replace ht := (ht i).mono_right this
no goals
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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 = ⊥
rwa [h, disjoint_self] at ht
no goals
case contra
α : Type u_2
β : Type ?u.53351
ι : Type u_1
ι' : Type ?u.53357
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
exact Ne.symm contra