[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq β
⊢ sup (∅ ∪ s₂) f = sup ∅ f ⊔ sup s₂ f
[PROOFSTEP]
rw [empty_union, sup_empty, bot_sup_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a✝ : α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : sup (s ∪ s₂) f = sup s f ⊔ sup s₂ f
⊢ sup (insert a s ∪ s₂) f = sup (insert a s) f ⊔ sup s₂ f
[PROOFSTEP]
rw [insert_union, sup_insert, sup_insert, ih, sup_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ sup s (f ⊔ g) = sup s f ⊔ sup s g
[PROOFSTEP]
refine' Finset.cons_induction_on s _ fun b t _ h => _
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ sup ∅ (f ⊔ g) = sup ∅ f ⊔ sup ∅ g
[PROOFSTEP]
rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : sup t (f ⊔ g) = sup t f ⊔ sup t g
⊢ sup (cons b t x✝) (f ⊔ g) = sup (cons b t x✝) f ⊔ sup (cons b t x✝) g
[PROOFSTEP]
rw [sup_cons, sup_cons, sup_cons, h]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : sup t (f ⊔ g) = sup t f ⊔ sup t g
⊢ (f ⊔ g) b ⊔ (sup t f ⊔ sup t g) = f b ⊔ sup t f ⊔ (g b ⊔ sup t g)
[PROOFSTEP]
exact sup_sup_sup_comm _ _ _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ sup s₁ f = sup s₂ g
[PROOFSTEP]
subst hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ sup s₁ f = sup s₁ g
[PROOFSTEP]
exact Finset.fold_congr hfg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
s✝¹ s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : ↑f (sup s g) = sup s (↑f ∘ g)
⊢ ↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)
[PROOFSTEP]
rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a✝ a : α
⊢ sup s f ≤ a ↔ ∀ (b : β), b ∈ s → f b ≤ a
[PROOFSTEP]
apply Iff.trans Multiset.sup_le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a✝ a : α
⊢ (∀ (b : α), b ∈ Multiset.map f s.val → b ≤ a) ↔ ∀ (b : β), b ∈ s → f b ≤ a
[PROOFSTEP]
simp only [Multiset.mem_map, and_imp, exists_imp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a✝ a : α
⊢ (∀ (b : α) (x : β), x ∈ s.val → f x = b → b ≤ a) ↔ ∀ (b : β), b ∈ s → f b ≤ a
[PROOFSTEP]
exact ⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq β
s : Finset γ
t : γ → Finset β
c : α
⊢ sup (Finset.biUnion s t) f ≤ c ↔ (sup s fun x => sup (t x) f) ≤ c
[PROOFSTEP]
simp [@forall_swap _ β]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
s : Finset β
⊢ (sup s fun x => ⊥) = ⊥
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
⊢ (sup ∅ fun x => ⊥) = ⊥
[PROOFSTEP]
exact sup_empty
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
s : Finset β
hs : Finset.Nonempty s
⊢ (sup s fun x => ⊥) = ⊥
[PROOFSTEP]
exact sup_const hs _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β → γ → α
⊢ (sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b c
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun a => _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a✝ : α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (sup s fun b => sup t (f b)) ≤ a ↔ (sup t fun c => sup s fun b => f b c) ≤ a
[PROOFSTEP]
simp_rw [Finset.sup_le_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a✝ : α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f b b_1 ≤ a) ↔ ∀ (b : γ), b ∈ t → ∀ (b_1 : β), b_1 ∈ s → f b_1 b ≤ a
[PROOFSTEP]
exact ⟨fun h c hc b hb => h b hb c hc, fun h b hb c hc => h c hc b hb⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')
[PROOFSTEP]
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_product, and_imp, Prod.forall]
  -- Porting note: was one expression.
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (∀ (a : β) (b : γ), a ∈ s → b ∈ t → f (a, b) ≤ sup s fun i => sup t fun i' => f (i, i')) ∧
    ∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f (b, b_1) ≤ sup (s ×ˢ t) f
[PROOFSTEP]
refine ⟨fun b c hb hc => ?_, fun b hb c hc => ?_⟩
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
c : γ
hb : b ∈ s
hc : c ∈ t
⊢ f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')
[PROOFSTEP]
refine (le_sup hb).trans' ?_
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
c : γ
hb : b ∈ s
hc : c ∈ t
⊢ f (b, c) ≤ sup t fun i' => f (b, i')
[PROOFSTEP]
exact @le_sup _ _ _ _ _ (fun c => f (b, c)) c hc
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
⊢ f (b, c) ≤ sup (s ×ˢ t) f
[PROOFSTEP]
exact le_sup <| mem_product.2 ⟨hb, hc⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')
[PROOFSTEP]
rw [sup_product_left, Finset.sup_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
s : Finset α
⊢ sup (erase s ⊥) id = sup s id
[PROOFSTEP]
refine' (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a✝ : α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ id a ≤ sup (erase s ⊥) id
[PROOFSTEP]
obtain rfl | ha' := eq_or_ne a ⊥
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ sup (erase s ⊥) id
[PROOFSTEP]
exact bot_le
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a✝ : α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ sup (erase s ⊥) id
[PROOFSTEP]
exact le_sup (mem_erase.2 ⟨ha', ha⟩)
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α✝
inst✝¹ : OrderBot α✝
s✝ s₁ s₂ : Finset β✝
f✝ g : β✝ → α✝
a✝ : α✝
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
⊢ (sup s fun b => f b \ a) = sup s f \ a
[PROOFSTEP]
refine' Finset.cons_induction_on s _ fun b t _ h => _
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α✝
inst✝¹ : OrderBot α✝
s✝ s₁ s₂ : Finset β✝
f✝ g : β✝ → α✝
a✝ : α✝
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
⊢ (sup ∅ fun b => f b \ a) = sup ∅ f \ a
[PROOFSTEP]
rw [sup_empty, sup_empty, bot_sdiff]
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α✝
inst✝¹ : OrderBot α✝
s✝ s₁ s₂ : Finset β✝
f✝ g : β✝ → α✝
a✝ : α✝
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
x✝ : ¬b ∈ t
h : (sup t fun b => f b \ a) = sup t f \ a
⊢ (sup (cons b t x✝) fun b => f b \ a) = sup (cons b t x✝) f \ a
[PROOFSTEP]
rw [sup_cons, sup_cons, h, sup_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : ¬c ∈ t
ih : g (sup t f) = sup t (g ∘ f)
⊢ g (sup (cons c t hc) f) = sup (cons c t hc) (g ∘ f)
[PROOFSTEP]
rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
[PROOFSTEP]
letI := Subtype.semilatticeSup Psup
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
[PROOFSTEP]
letI := Subtype.orderBot Pbot
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
[PROOFSTEP]
apply comp_sup_eq_sup_comp Subtype.val
[GOAL]
case g_sup
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ∀ (x y : { x // P x }), ↑(x ⊔ y) = ↑x ⊔ ↑y
[PROOFSTEP]
intros
[GOAL]
case bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑⊥ = ⊥
[PROOFSTEP]
intros
[GOAL]
case g_sup
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
x✝ y✝ : { x // P x }
⊢ ↑(x✝ ⊔ y✝) = ↑x✝ ⊔ ↑y✝
[PROOFSTEP]
rfl
[GOAL]
case bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑⊥ = ⊥
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l = sup (List.toFinset l) id
[PROOFSTEP]
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val, Multiset.map_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x x_1 => x ⊔ x_1) ⊥ (dedup ↑l) = Multiset.sup (dedup ↑l)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ p (sup s f)
[PROOFSTEP]
induction' s using Finset.cons_induction with c s hc ih
[GOAL]
case empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s → p (f b)
hs : ∀ (b : β), b ∈ ∅ → p (f b)
⊢ p (sup ∅ f)
[PROOFSTEP]
exact hb
[GOAL]
case cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (sup (cons c s hc) f)
[PROOFSTEP]
rw [sup_cons]
[GOAL]
case cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (f c ⊔ sup s f)
[PROOFSTEP]
apply hp
[GOAL]
case cons.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (f c)
[PROOFSTEP]
exact hs c (mem_cons.2 (Or.inl rfl))
[GOAL]
case cons.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f g : β → α
a : α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs✝ : ∀ (b : β), b ∈ s✝ → p (f b)
c : β
s : Finset β
hc : ¬c ∈ s
ih : (∀ (b : β), b ∈ s → p (f b)) → p (sup s f)
hs : ∀ (b : β), b ∈ cons c s hc → p (f b)
⊢ p (sup s f)
[PROOFSTEP]
exact ih fun b h => hs b (mem_cons.2 (Or.inr h))
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
t : Finset α
⊢ (∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup t id ≤ x
[PROOFSTEP]
classical
induction' t using Finset.induction_on with a r _ ih h
·
  simpa only [forall_prop_of_true, and_true_iff, forall_prop_of_false, bot_le, not_false_iff, sup_empty,
    forall_true_iff, not_mem_empty]
· intro h
  have incs : (r : Set α) ⊆ ↑(insert a r) := by
    rw [Finset.coe_subset]
    apply Finset.subset_insert
  obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
  obtain ⟨y, hys, hay⟩ :=
    h a
      (Finset.mem_insert_self a r)
        -- z ∈ s is above x and y
  obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
  use z, hzs
  rw [sup_insert, id.def, sup_le_iff]
  exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
t : Finset α
⊢ (∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup t id ≤ x
[PROOFSTEP]
induction' t using Finset.induction_on with a r _ ih h
[GOAL]
case empty
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ (∀ (x : α), x ∈ ∅ → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup ∅ id ≤ x
[PROOFSTEP]
simpa only [forall_prop_of_true, and_true_iff, forall_prop_of_false, bot_le, not_false_iff, sup_empty, forall_true_iff,
  not_mem_empty]
[GOAL]
case insert
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
⊢ (∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
[PROOFSTEP]
intro h
[GOAL]
case insert
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
[PROOFSTEP]
have incs : (r : Set α) ⊆ ↑(insert a r) := by
  rw [Finset.coe_subset]
  apply Finset.subset_insert
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ ↑r ⊆ ↑(insert a r)
[PROOFSTEP]
rw [Finset.coe_subset]
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ r ⊆ insert a r
[PROOFSTEP]
apply Finset.subset_insert
[GOAL]
case insert
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
[PROOFSTEP]
obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
[GOAL]
case insert.intro.intro
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
[PROOFSTEP]
obtain ⟨y, hys, hay⟩ :=
  h a
    (Finset.mem_insert_self a r)
      -- z ∈ s is above x and y
[GOAL]
case insert.intro.intro.intro.intro
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
[PROOFSTEP]
obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
[PROOFSTEP]
use z, hzs
[GOAL]
case right
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ sup (insert a r) id ≤ z
[PROOFSTEP]
rw [sup_insert, id.def, sup_le_iff]
[GOAL]
case right
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ sup r id ≤ z
[PROOFSTEP]
exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
f : β → α
S : Finset β
⊢ sup S f = ⊥ ↔ ∀ (s : β), s ∈ S → f s = ⊥
[PROOFSTEP]
classical induction' S using Finset.induction with a S _ hi <;> simp [*]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
f : β → α
S : Finset β
⊢ sup S f = ⊥ ↔ ∀ (s : β), s ∈ S → f s = ⊥
[PROOFSTEP]
induction' S using Finset.induction with a S _ hi
[GOAL]
case empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
f : β → α
⊢ sup ∅ f = ⊥ ↔ ∀ (s : β), s ∈ ∅ → f s = ⊥
[PROOFSTEP]
simp [*]
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a✝¹ : α
f : β → α
a : β
S : Finset β
a✝ : ¬a ∈ S
hi : sup S f = ⊥ ↔ ∀ (s : β), s ∈ S → f s = ⊥
⊢ sup (insert a S) f = ⊥ ↔ ∀ (s : β), s ∈ insert a S → f s = ⊥
[PROOFSTEP]
simp [*]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : CompleteLattice α
s : Finset α
⊢ sup s id = sSup ↑s
[PROOFSTEP]
simp [sSup_eq_iSup, sup_eq_iSup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ sup s f = sSup (f '' ↑s)
[PROOFSTEP]
classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.comp.left_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ sup s f = sSup (f '' ↑s)
[PROOFSTEP]
rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.comp.left_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hs : s₁ = s₂
hfg : ∀ (a : β), a ∈ s₂ → f a = g a
⊢ inf s₁ f = inf s₂ g
[PROOFSTEP]
subst hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s s₁ : Finset β
f✝ g✝ : β → α
a : α
f g : β → α
hfg : ∀ (a : β), a ∈ s₁ → f a = g a
⊢ inf s₁ f = inf s₁ g
[PROOFSTEP]
exact Finset.fold_congr hfg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁴ : SemilatticeInf α
inst✝³ : OrderTop α
s✝¹ s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
inst✝² : SemilatticeInf β
inst✝¹ : OrderTop β
inst✝ : InfTopHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : ↑f (inf s g) = inf s (↑f ∘ g)
⊢ ↑f (inf (cons i s x✝) g) = inf (cons i s x✝) (↑f ∘ g)
[PROOFSTEP]
rw [inf_cons, inf_cons, map_inf, h, Function.comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l = inf (List.toFinset l) id
[PROOFSTEP]
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, inf_def, ← List.toFinset_coe, toFinset_val, Multiset.map_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
s s₁ s₂ : Finset β
f g : β → α
a : α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x x_1 => x ⊓ x_1) ⊤ (dedup ↑l) = Multiset.inf (dedup ↑l)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ sup s f = sup s fun i => a ⊓ f i
[PROOFSTEP]
induction' s using Finset.cons_induction with i s hi h
[GOAL]
case empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
f : ι → α
a : α
⊢ a ⊓ sup ∅ f = sup ∅ fun i => a ⊓ f i
[PROOFSTEP]
simp_rw [Finset.sup_empty, inf_bot_eq]
[GOAL]
case cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
f : ι → α
a : α
i : ι
s : Finset ι
hi : ¬i ∈ s
h : a ⊓ sup s f = sup s fun i => a ⊓ f i
⊢ a ⊓ sup (cons i s hi) f = sup (cons i s hi) fun i => a ⊓ f i
[PROOFSTEP]
rw [sup_cons, sup_cons, inf_sup_left, h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ sup s f ⊓ a = sup s fun i => f i ⊓ a
[PROOFSTEP]
rw [_root_.inf_comm, s.sup_inf_distrib_left]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t : Finset κ
f✝ : ι → α
g : κ → α
a✝ : α
s : Finset ι
f : ι → α
a : α
⊢ (sup s fun i => a ⊓ f i) = sup s fun i => f i ⊓ a
[PROOFSTEP]
simp_rw [_root_.inf_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
a : α
⊢ _root_.Disjoint a (sup s f) ↔ ∀ ⦃i : ι⦄, i ∈ s → _root_.Disjoint a (f i)
[PROOFSTEP]
simp only [disjoint_iff, sup_inf_distrib_left, Finset.sup_eq_bot_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
a : α
⊢ _root_.Disjoint (sup s f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → _root_.Disjoint (f i) a
[PROOFSTEP]
simp only [disjoint_iff, sup_inf_distrib_right, Finset.sup_eq_bot_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s✝ : Finset ι
t✝ : Finset κ
f✝ : ι → α
g✝ : κ → α
a : α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
⊢ sup s f ⊓ sup t g = sup (s ×ˢ t) fun i => f i.fst ⊓ g i.snd
[PROOFSTEP]
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
[PROOFSTEP]
induction' s using Finset.induction with i s hi ih
[GOAL]
case empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ (inf ∅ fun i => sup (t i) (f i)) = sup (pi ∅ t) fun g => inf (attach ∅) fun i => f (↑i) (g ↑i (_ : ↑i ∈ ∅))
[PROOFSTEP]
simp
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
⊢ (inf (insert i s) fun i => sup (t i) (f i)) =
    sup (pi (insert i s) t) fun g => inf (attach (insert i s)) fun i_1 => f (↑i_1) (g ↑i_1 (_ : ↑i_1 ∈ insert i s))
[PROOFSTEP]
rw [inf_insert, ih, attach_insert, sup_inf_sup]
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
⊢ (sup (t i ×ˢ pi s t) fun i_1 => f i i_1.fst ⊓ inf (attach s) fun i_2 => f (↑i_2) (Prod.snd i_1 ↑i_2 (_ : ↑i_2 ∈ s))) =
    sup (pi (insert i s) t) fun g =>
      inf
        (insert { val := i, property := (_ : i ∈ insert i s) }
          (image (fun x => { val := ↑x, property := (_ : ↑x ∈ insert i s) }) (attach s)))
        fun i_1 => f (↑i_1) (g ↑i_1 (_ : ↑i_1 ∈ insert i s))
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun c => _
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
⊢ (sup (t i ×ˢ pi s t) fun i_1 => f i i_1.fst ⊓ inf (attach s) fun i_2 => f (↑i_2) (Prod.snd i_1 ↑i_2 (_ : ↑i_2 ∈ s))) ≤
      c ↔
    (sup (pi (insert i s) t) fun g =>
        inf
          (insert { val := i, property := (_ : i ∈ insert i s) }
            (image (fun x => { val := ↑x, property := (_ : ↑x ∈ insert i s) }) (attach s)))
          fun i_1 => f (↑i_1) (g ↑i_1 (_ : ↑i_1 ∈ insert i s))) ≤
      c
[PROOFSTEP]
simp only [Finset.sup_le_iff, mem_product, mem_pi, and_imp, Prod.forall, inf_insert, inf_image]
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
⊢ (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i →
        (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ inf (attach s) fun i => f (↑i) (b ↑i (_ : ↑i ∈ s))) ≤ c) ↔
    ∀ (b : (a : ι) → a ∈ insert i s → κ a),
      (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
        f i
              (b ↑{ val := i, property := (_ : i ∈ insert i s) }
                (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
            inf (attach s)
              ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
                { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
          c
[PROOFSTEP]
refine'
  ⟨fun h g hg =>
    h (g i <| mem_insert_self _ _) (fun j hj => g j <| mem_insert_of_mem hj) (hg _ <| mem_insert_self _ _) fun j hj =>
      hg _ <| mem_insert_of_mem hj,
    fun h a g ha hg => _⟩
    -- TODO: This `have` must be named to prevent it being shadowed by the internal `this` in `simpa`
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
⊢ (f i a ⊓ inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))) ≤ c
[PROOFSTEP]
have aux : ∀ j : { x // x ∈ s }, ↑j ≠ i := fun j : s => ne_of_mem_of_not_mem j.2 hi
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
⊢ (f i a ⊓ inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))) ≤ c
[PROOFSTEP]
have :=
  h (fun j hj => if hji : j = i then cast (congr_arg κ hji.symm) a else g _ <| mem_of_mem_insert_of_ne hj hji)
    (fun j hj => ?_)
[GOAL]
case insert.refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
this :
  f i
        ((fun j hj => if hji : j = i then cast (_ : κ i = κ j) a else g j (_ : j ∈ s))
          ↑{ val := i, property := (_ : i ∈ insert i s) }
          (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
      inf (attach s)
        ((fun i_1 =>
            f (↑i_1)
              ((fun j hj => if hji : j = i then cast (_ : κ i = κ j) a else g j (_ : j ∈ s)) ↑i_1
                (_ : ↑i_1 ∈ insert i s))) ∘
          fun x => { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
    c
⊢ (f i a ⊓ inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))) ≤ c
case insert.refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
j : ι
hj : j ∈ insert i s
⊢ (fun j hj => if hji : j = i then cast (_ : κ i = κ j) a else g j (_ : j ∈ s)) j hj ∈ t j
[PROOFSTEP]
simpa only [cast_eq, dif_pos, Function.comp, Subtype.coe_mk, dif_neg, aux] using this
[GOAL]
case insert.refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
j : ι
hj : j ∈ insert i s
⊢ (fun j hj => if hji : j = i then cast (_ : κ i = κ j) a else g j (_ : j ∈ s)) j hj ∈ t j
[PROOFSTEP]
rw [mem_insert] at hj
[GOAL]
case insert.refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j = i ∨ j ∈ s
⊢ (fun j hj => if hji : j = i then cast (_ : κ i = κ j) a else g j (_ : j ∈ s)) j hj✝ ∈ t j
[PROOFSTEP]
obtain (rfl | hj) := hj
[GOAL]
case insert.refine_1.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
s : Finset ι
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
g : (a : ι) → a ∈ s → κ a
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
j : ι
hi : ¬j ∈ s
h :
  ∀ (b : (a : ι) → a ∈ insert j s → κ a),
    (∀ (a : ι) (h : a ∈ insert j s), b a h ∈ t a) →
      f j
            (b ↑{ val := j, property := (_ : j ∈ insert j s) }
              (_ : ↑{ val := j, property := (_ : j ∈ insert j s) } ∈ insert j s)) ⊓
          inf (attach s)
            ((fun i => f (↑i) (b ↑i (_ : ↑i ∈ insert j s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert j s) }) ≤
        c
a : κ j
ha : a ∈ t j
aux : ∀ (j_1 : { x // x ∈ s }), ↑j_1 ≠ j
hj : j ∈ insert j s
⊢ (fun j_1 hj => if hji : j_1 = j then cast (_ : κ j = κ j_1) a else g j_1 (_ : j_1 ∈ s)) j hj ∈ t j
[PROOFSTEP]
simpa
[GOAL]
case insert.refine_1.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ✝ : Type u_6
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_7
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih : (inf s fun i => sup (t i) (f i)) = sup (pi s t) fun g => inf (attach s) fun i => f (↑i) (g ↑i (_ : ↑i ∈ s))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i
            (b ↑{ val := i, property := (_ : i ∈ insert i s) }
              (_ : ↑{ val := i, property := (_ : i ∈ insert i s) } ∈ insert i s)) ⊓
          inf (attach s)
            ((fun i_1 => f (↑i_1) (b ↑i_1 (_ : ↑i_1 ∈ insert i s))) ∘ fun x =>
              { val := ↑x, property := (_ : ↑x ∈ insert i s) }) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j ∈ s
⊢ (fun j hj => if hji : j = i then cast (_ : κ i = κ j) a else g j (_ : j ∈ s)) j hj✝ ∈ t j
[PROOFSTEP]
simpa [ne_of_mem_of_not_mem hj hi] using hg _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
⊢ (sup s fun b => a \ f b) = a \ inf s f
[PROOFSTEP]
refine' Finset.cons_induction_on s _ fun b t _ h => _
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
⊢ (sup ∅ fun b => a \ f b) = a \ inf ∅ f
[PROOFSTEP]
rw [sup_empty, inf_empty, sdiff_top]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s✝ s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
x✝ : ¬b ∈ t
h : (sup t fun b => a \ f b) = a \ inf t f
⊢ (sup (cons b t x✝) fun b => a \ f b) = a \ inf (cons b t x✝) f
[PROOFSTEP]
rw [sup_cons, inf_cons, h, sdiff_inf]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
a : α
⊢ (inf s fun b => a \ f b) = a \ sup s f
[PROOFSTEP]
induction' hs using Finset.Nonempty.cons_induction with b b t _ _ h
[GOAL]
case h₀
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
⊢ (inf {b} fun b => a \ f b) = a \ sup {b} f
[PROOFSTEP]
rw [sup_singleton, inf_singleton]
[GOAL]
case h₁
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
h✝ : ¬b ∈ t
hs✝ : Finset.Nonempty t
h : (inf t fun b => a \ f b) = a \ sup t f
⊢ (inf (cons b t h✝) fun b => a \ f b) = a \ sup (cons b t h✝) f
[PROOFSTEP]
rw [sup_cons, inf_cons, h, sdiff_sup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
a : α
⊢ (inf s fun b => f b \ a) = inf s f \ a
[PROOFSTEP]
induction' hs using Finset.Nonempty.cons_induction with b b t _ _ h
[GOAL]
case h₀
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
⊢ (inf {b} fun b => f b \ a) = inf {b} f \ a
[PROOFSTEP]
rw [inf_singleton, inf_singleton]
[GOAL]
case h₁
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
b : ι
t : Finset ι
h✝ : ¬b ∈ t
hs✝ : Finset.Nonempty t
h : (inf t fun b => f b \ a) = inf t f \ a
⊢ (inf (cons b t h✝) fun b => f b \ a) = inf (cons b t h✝) f \ a
[PROOFSTEP]
rw [inf_cons, inf_cons, h, inf_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup s f ↔ ∃ b, b ∈ s ∧ a ≤ f b
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup s f → ∃ b, b ∈ s ∧ a ≤ f b
[PROOFSTEP]
induction s using cons_induction with
| empty => exact (absurd · (not_le_of_lt ha))
| @cons c t hc ih =>
  rw [sup_cons, le_sup_iff]
  exact fun
    | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
    | Or.inr h =>
      let ⟨b, hb, hle⟩ := ih h;
      ⟨b, mem_cons.2 (Or.inr hb), hle⟩
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup s f → ∃ b, b ∈ s ∧ a ≤ f b
[PROOFSTEP]
induction s using cons_induction with
| empty => exact (absurd · (not_le_of_lt ha))
| @cons c t hc ih =>
  rw [sup_cons, le_sup_iff]
  exact fun
    | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
    | Or.inr h =>
      let ⟨b, hb, hle⟩ := ih h;
      ⟨b, mem_cons.2 (Or.inr hb), hle⟩
[GOAL]
case mp.empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup ∅ f → ∃ b, b ∈ ∅ ∧ a ≤ f b
[PROOFSTEP]

| empty => exact (absurd · (not_le_of_lt ha))
[GOAL]
case mp.empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup ∅ f → ∃ b, b ∈ ∅ ∧ a ≤ f b
[PROOFSTEP]
exact (absurd · (not_le_of_lt ha))
[GOAL]
case mp.cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a ≤ sup t f → ∃ b, b ∈ t ∧ a ≤ f b
⊢ a ≤ sup (cons c t hc) f → ∃ b, b ∈ cons c t hc ∧ a ≤ f b
[PROOFSTEP]

| @cons c t hc ih =>
  rw [sup_cons, le_sup_iff]
  exact fun
    | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
    | Or.inr h =>
      let ⟨b, hb, hle⟩ := ih h;
      ⟨b, mem_cons.2 (Or.inr hb), hle⟩
[GOAL]
case mp.cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a ≤ sup t f → ∃ b, b ∈ t ∧ a ≤ f b
⊢ a ≤ sup (cons c t hc) f → ∃ b, b ∈ cons c t hc ∧ a ≤ f b
[PROOFSTEP]
rw [sup_cons, le_sup_iff]
[GOAL]
case mp.cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a ≤ sup t f → ∃ b, b ∈ t ∧ a ≤ f b
⊢ a ≤ f c ∨ a ≤ sup t f → ∃ b, b ∈ cons c t hc ∧ a ≤ f b
[PROOFSTEP]
exact fun
  | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
  | Or.inr h =>
    let ⟨b, hb, hle⟩ := ih h;
    ⟨b, mem_cons.2 (Or.inr hb), hle⟩
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b, b ∈ s ∧ a ≤ f b) → a ≤ sup s f
[PROOFSTEP]
exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup s f ↔ ∃ b, b ∈ s ∧ a < f b
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup s f → ∃ b, b ∈ s ∧ a < f b
[PROOFSTEP]
induction s using cons_induction with
| empty => exact (absurd · not_lt_bot)
| @cons c t hc ih =>
  rw [sup_cons, lt_sup_iff]
  exact fun
    | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
    | Or.inr h =>
      let ⟨b, hb, hlt⟩ := ih h;
      ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup s f → ∃ b, b ∈ s ∧ a < f b
[PROOFSTEP]
induction s using cons_induction with
| empty => exact (absurd · not_lt_bot)
| @cons c t hc ih =>
  rw [sup_cons, lt_sup_iff]
  exact fun
    | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
    | Or.inr h =>
      let ⟨b, hb, hlt⟩ := ih h;
      ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
[GOAL]
case mp.empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup ∅ f → ∃ b, b ∈ ∅ ∧ a < f b
[PROOFSTEP]

| empty => exact (absurd · not_lt_bot)
[GOAL]
case mp.empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup ∅ f → ∃ b, b ∈ ∅ ∧ a < f b
[PROOFSTEP]
exact (absurd · not_lt_bot)
[GOAL]
case mp.cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a < sup t f → ∃ b, b ∈ t ∧ a < f b
⊢ a < sup (cons c t hc) f → ∃ b, b ∈ cons c t hc ∧ a < f b
[PROOFSTEP]

| @cons c t hc ih =>
  rw [sup_cons, lt_sup_iff]
  exact fun
    | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
    | Or.inr h =>
      let ⟨b, hb, hlt⟩ := ih h;
      ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
[GOAL]
case mp.cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a < sup t f → ∃ b, b ∈ t ∧ a < f b
⊢ a < sup (cons c t hc) f → ∃ b, b ∈ cons c t hc ∧ a < f b
[PROOFSTEP]
rw [sup_cons, lt_sup_iff]
[GOAL]
case mp.cons
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a < sup t f → ∃ b, b ∈ t ∧ a < f b
⊢ a < f c ∨ a < sup t f → ∃ b, b ∈ cons c t hc ∧ a < f b
[PROOFSTEP]
exact fun
  | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
  | Or.inr h =>
    let ⟨b, hb, hlt⟩ := ih h;
    ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ a < f b) → a < sup s f
[PROOFSTEP]
exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : ¬c ∈ t
⊢ ((∀ (b : ι), b ∈ t → f b < a) → sup t f < a) → (∀ (b : ι), b ∈ cons c t hc → f b < a) → sup (cons c t hc) f < a
[PROOFSTEP]
simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using And.imp_right
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
⊢ sup s (WithBot.some ∘ f) ≠ ⊥
[PROOFSTEP]
simpa using H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
⊢ ↑(sup' s H f) = sup s (WithBot.some ∘ f)
[PROOFSTEP]
rw [sup', WithBot.coe_unbot]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
hb : ¬b ∈ s
h : Finset.Nonempty (cons b s hb)
⊢ sup' (cons b s hb) h f = f b ⊔ sup' s H f
[PROOFSTEP]
rw [← WithBot.coe_eq_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
hb : ¬b ∈ s
h : Finset.Nonempty (cons b s hb)
⊢ ↑(sup' (cons b s hb) h f) = ↑(f b ⊔ sup' s H f)
[PROOFSTEP]
simp [WithBot.coe_sup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
inst✝ : DecidableEq β
b : β
h : Finset.Nonempty (insert b s)
⊢ sup' (insert b s) h f = f b ⊔ sup' s H f
[PROOFSTEP]
rw [← WithBot.coe_eq_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
inst✝ : DecidableEq β
b : β
h : Finset.Nonempty (insert b s)
⊢ ↑(sup' (insert b s) h f) = ↑(f b ⊔ sup' s H f)
[PROOFSTEP]
simp [WithBot.coe_sup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
hs : ∀ (b : β), b ∈ s → f b ≤ a
⊢ sup' s H f ≤ a
[PROOFSTEP]
rw [← WithBot.coe_le_coe, coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
hs : ∀ (b : β), b ∈ s → f b ≤ a
⊢ sup s (WithBot.some ∘ f) ≤ ↑a
[PROOFSTEP]
exact Finset.sup_le fun b h => WithBot.coe_le_coe.2 <| hs b h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
h : b ∈ s
⊢ f b ≤ sup' s (_ : ∃ x, x ∈ s) f
[PROOFSTEP]
rw [← WithBot.coe_le_coe, coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
b : β
h : b ∈ s
⊢ ↑(f b) ≤ sup s (WithBot.some ∘ f)
[PROOFSTEP]
exact le_sup (f := fun c => WithBot.some (f c)) h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ (sup' s H fun x => a) = a
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ (sup' s H fun x => a) ≤ a
[PROOFSTEP]
apply sup'_le
[GOAL]
case a.hs
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ ∀ (b : β), b ∈ s → a ≤ a
[PROOFSTEP]
intros
[GOAL]
case a.hs
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
b✝ : β
a✝ : b✝ ∈ s
⊢ a ≤ a
[PROOFSTEP]
exact le_rfl
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
a : α
⊢ a ≤ sup' s H fun x => a
[PROOFSTEP]
apply le_sup' (fun _ => a) H.choose_spec
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f : β → α
inst✝ : DecidableEq β
s : Finset γ
Hs : Finset.Nonempty s
t : γ → Finset β
Ht : ∀ (b : γ), Finset.Nonempty (t b)
c : α
⊢ sup' (Finset.biUnion s t) (_ : Finset.Nonempty (Finset.biUnion s t)) f ≤ c ↔
    (sup' s Hs fun b => sup' (t b) (_ : Finset.Nonempty (t b)) f) ≤ c
[PROOFSTEP]
simp [@forall_swap _ β]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (sup' s H f) = sup' s H (g ∘ f)
[PROOFSTEP]
rw [← WithBot.coe_eq_coe, coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ↑(g (sup' s H f)) = sup s (WithBot.some ∘ g ∘ f)
[PROOFSTEP]
let g' := WithBot.map g
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ ↑(g (sup' s H f)) = sup s (WithBot.some ∘ g ∘ f)
[PROOFSTEP]
show g' ↑(s.sup' H f) = s.sup fun a => g' ↑(f a)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ g' ↑(sup' s H f) = sup s fun a => g' ↑(f a)
[PROOFSTEP]
rw [coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ g' (sup s (WithBot.some ∘ f)) = sup s fun a => g' ↑(f a)
[PROOFSTEP]
refine' comp_sup_eq_sup_comp g' _ rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
⊢ ∀ (x y : WithBot α), g' (x ⊔ y) = g' x ⊔ g' y
[PROOFSTEP]
intro f₁ f₂
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : WithBot α
⊢ g' (f₁ ⊔ f₂) = g' f₁ ⊔ g' f₂
[PROOFSTEP]
cases f₁ using WithBot.recBotCoe with
| bot =>
  rw [bot_sup_eq]
  exact bot_sup_eq.symm
| coe f₁ =>
  cases f₂ using WithBot.recBotCoe with
  | bot => rfl
  | coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : WithBot α
⊢ g' (f₁ ⊔ f₂) = g' f₁ ⊔ g' f₂
[PROOFSTEP]
cases f₁ using WithBot.recBotCoe with
| bot =>
  rw [bot_sup_eq]
  exact bot_sup_eq.symm
| coe f₁ =>
  cases f₂ using WithBot.recBotCoe with
  | bot => rfl
  | coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
case bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
⊢ g' (⊥ ⊔ f₂) = g' ⊥ ⊔ g' f₂
[PROOFSTEP]

| bot =>
  rw [bot_sup_eq]
  exact bot_sup_eq.symm
[GOAL]
case bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
⊢ g' (⊥ ⊔ f₂) = g' ⊥ ⊔ g' f₂
[PROOFSTEP]
rw [bot_sup_eq]
[GOAL]
case bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
⊢ g' f₂ = g' ⊥ ⊔ g' f₂
[PROOFSTEP]
exact bot_sup_eq.symm
[GOAL]
case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
f₁ : α
⊢ g' (↑f₁ ⊔ f₂) = g' ↑f₁ ⊔ g' f₂
[PROOFSTEP]

| coe f₁ =>
  cases f₂ using WithBot.recBotCoe with
  | bot => rfl
  | coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
f₁ : α
⊢ g' (↑f₁ ⊔ f₂) = g' ↑f₁ ⊔ g' f₂
[PROOFSTEP]
cases f₂ using WithBot.recBotCoe with
| bot => rfl
| coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₂ : WithBot α
f₁ : α
⊢ g' (↑f₁ ⊔ f₂) = g' ↑f₁ ⊔ g' f₂
[PROOFSTEP]
cases f₂ using WithBot.recBotCoe with
| bot => rfl
| coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
case coe.bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ : α
⊢ g' (↑f₁ ⊔ ⊥) = g' ↑f₁ ⊔ g' ⊥
[PROOFSTEP]

| bot => rfl
[GOAL]
case coe.bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ : α
⊢ g' (↑f₁ ⊔ ⊥) = g' ↑f₁ ⊔ g' ⊥
[PROOFSTEP]
rfl
[GOAL]
case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : α
⊢ g' (↑f₁ ⊔ ↑f₂) = g' ↑f₁ ⊔ g' ↑f₂
[PROOFSTEP]

| coe f₂ => exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
s✝ : Finset β
H✝ : Finset.Nonempty s✝
f✝ : β → α
inst✝ : SemilatticeSup γ
s : Finset β
H : Finset.Nonempty s
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
g' : WithBot α → WithBot γ := WithBot.map g
f₁ f₂ : α
⊢ g' (↑f₁ ⊔ ↑f₂) = g' ↑f₁ ⊔ g' ↑f₂
[PROOFSTEP]
exact congr_arg _ (g_sup f₁ f₂)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ p (sup' s H f)
[PROOFSTEP]
show @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ WithBot.recBotCoe True p ↑(sup' s H f)
[PROOFSTEP]
rw [coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ WithBot.recBotCoe True p (sup s (WithBot.some ∘ f))
[PROOFSTEP]
refine' sup_induction trivial _ hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
⊢ ∀ (a₁ : WithBot α),
    WithBot.recBotCoe True p a₁ → ∀ (a₂ : WithBot α), WithBot.recBotCoe True p a₂ → WithBot.recBotCoe True p (a₁ ⊔ a₂)
[PROOFSTEP]
rintro (_ | a₁) h₁ a₂ h₂
[GOAL]
case none
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
h₁ : WithBot.recBotCoe True p none
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (none ⊔ a₂)
[PROOFSTEP]
rw [WithBot.none_eq_bot, bot_sup_eq]
[GOAL]
case none
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
h₁ : WithBot.recBotCoe True p none
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p a₂
[PROOFSTEP]
exact h₂
[GOAL]
case some
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ a₂)
[PROOFSTEP]
cases a₂ using WithBot.recBotCoe with
| bot => exact h₁
| coe a₂ => exact hp a₁ h₁ a₂ h₂
[GOAL]
case some
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : WithBot α
h₂ : WithBot.recBotCoe True p a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ a₂)
[PROOFSTEP]
cases a₂ using WithBot.recBotCoe with
| bot => exact h₁
| coe a₂ => exact hp a₁ h₁ a₂ h₂
[GOAL]
case some.bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
h₂ : WithBot.recBotCoe True p ⊥
⊢ WithBot.recBotCoe True p (some a₁ ⊔ ⊥)
[PROOFSTEP]

| bot => exact h₁
[GOAL]
case some.bot
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
h₂ : WithBot.recBotCoe True p ⊥
⊢ WithBot.recBotCoe True p (some a₁ ⊔ ⊥)
[PROOFSTEP]
exact h₁
[GOAL]
case some.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : α
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ ↑a₂)
[PROOFSTEP]

| coe a₂ => exact hp a₁ h₁ a₂ h₂
[GOAL]
case some.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ (b : β), b ∈ s → p (f b)
a₁ : α
h₁ : WithBot.recBotCoe True p (some a₁)
a₂ : α
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (some a₁ ⊔ ↑a₂)
[PROOFSTEP]
exact hp a₁ h₁ a₂ h₂
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f✝ : β → α
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ (x : β), x ∈ s → f x = g x
⊢ sup' s H f = sup' t (_ : Finset.Nonempty t) g
[PROOFSTEP]
subst s
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
f✝ : β → α
t : Finset β
f g : β → α
H : Finset.Nonempty t
h₂ : ∀ (x : β), x ∈ t → f x = g x
⊢ sup' t H f = sup' t (_ : Finset.Nonempty t) g
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun c => _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
f✝ : β → α
t : Finset β
f g : β → α
H : Finset.Nonempty t
h₂ : ∀ (x : β), x ∈ t → f x = g x
c : α
⊢ sup' t H f ≤ c ↔ sup' t (_ : Finset.Nonempty t) g ≤ c
[PROOFSTEP]
simp (config := { contextual := true }) only [sup'_le_iff, h₂]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f✝ : β → α
s : Finset γ
f : γ ↪ β
g : β → α
hs : Finset.Nonempty (map f s)
hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)
⊢ sup' (map f s) hs g = sup' s hs' (g ∘ ↑f)
[PROOFSTEP]
rw [← WithBot.coe_eq_coe, coe_sup', sup_map, coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeSup α
s✝ : Finset β
H : Finset.Nonempty s✝
f✝ : β → α
s : Finset γ
f : γ ↪ β
g : β → α
hs : Finset.Nonempty (map f s)
hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)
⊢ sup s ((WithBot.some ∘ g) ∘ ↑f) = sup s (WithBot.some ∘ g ∘ ↑f)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : SemilatticeInf α
s : Finset β
H : Finset.Nonempty s
f : β → α
⊢ inf s (WithTop.some ∘ f) ≠ ⊤
[PROOFSTEP]
simpa using H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
h : Finset.Nonempty s
f : β → α
⊢ ↑(sup s f) = sup s (WithBot.some ∘ f)
[PROOFSTEP]
simp only [← sup'_eq_sup h, coe_sup' h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ a ≤ sup' s H f ↔ ∃ b, b ∈ s ∧ a ≤ f b
[PROOFSTEP]
rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ ↑a ≤ (WithBot.some ∘ f) b) ↔ ∃ b, b ∈ s ∧ a ≤ f b
[PROOFSTEP]
exact exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ a < sup' s H f ↔ ∃ b, b ∈ s ∧ a < f b
[PROOFSTEP]
rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ ↑a < (WithBot.some ∘ f) b) ↔ ∃ b, b ∈ s ∧ a < f b
[PROOFSTEP]
exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ sup' s H f < a ↔ ∀ (i : ι), i ∈ s → f i < a
[PROOFSTEP]
rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f : ι → α
a : α
⊢ (∀ (b : ι), b ∈ s → (WithBot.some ∘ f) b < ↑a) ↔ ∀ (i : ι), i ∈ s → f i < a
[PROOFSTEP]
exact ball_congr (fun _ _ => WithBot.coe_lt_coe)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f✝ : ι → α
a : α
f : ι → α
⊢ ∃ i, i ∈ s ∧ sup' s H f = f i
[PROOFSTEP]
refine' H.cons_induction (fun c => _) fun c s hc hs ih => _
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f✝ : ι → α
a : α
f : ι → α
c : ι
⊢ ∃ i, i ∈ {c} ∧ sup' {c} (_ : Finset.Nonempty {c}) f = f i
[PROOFSTEP]
exact ⟨c, mem_singleton_self c, rfl⟩
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
ih : ∃ i, i ∈ s ∧ sup' s hs f = f i
⊢ ∃ i, i ∈ cons c s hc ∧ sup' (cons c s hc) (_ : Finset.Nonempty (cons c s hc)) f = f i
[PROOFSTEP]
rcases ih with ⟨b, hb, h'⟩
[GOAL]
case refine'_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
⊢ ∃ i, i ∈ cons c s hc ∧ sup' (cons c s hc) (_ : Finset.Nonempty (cons c s hc)) f = f i
[PROOFSTEP]
rw [sup'_cons hs, h']
[GOAL]
case refine'_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
[PROOFSTEP]
cases le_total (f b) (f c) with
| inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
| inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
[GOAL]
case refine'_2.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
x✝ : f b ≤ f c ∨ f c ≤ f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
[PROOFSTEP]
cases le_total (f b) (f c) with
| inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
| inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
[GOAL]
case refine'_2.intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
h : f b ≤ f c
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
[PROOFSTEP]

| inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
[GOAL]
case refine'_2.intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
h : f b ≤ f c
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
[PROOFSTEP]
exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
[GOAL]
case refine'_2.intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
h : f c ≤ f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
[PROOFSTEP]

| inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
[GOAL]
case refine'_2.intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
h : f c ≤ f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
[PROOFSTEP]
exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
a : α
⊢ Finset.max {a} = ↑a
[PROOFSTEP]
rw [← insert_emptyc_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
a : α
⊢ Finset.max (insert a ∅) = ↑a
[PROOFSTEP]
exact max_insert
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ b, Finset.max s = ↑b
[PROOFSTEP]
obtain ⟨b, h, _⟩ := le_sup (α := WithBot α) h _ rfl
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : b ∈ sup s some
right✝ : a ≤ b
⊢ ∃ b, Finset.max s = ↑b
[PROOFSTEP]
exact ⟨b, h⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
⊢ s = ∅
[PROOFSTEP]
obtain ⟨a, ha⟩ := max_of_nonempty H
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
a : α
ha : Finset.max s = ↑a
⊢ s = ∅
[PROOFSTEP]
rw [h] at ha
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
h : Finset.max s = ⊥
H : Finset.Nonempty s
a : α
ha : ⊥ = ↑a
⊢ s = ∅
[PROOFSTEP]
cases ha
[GOAL]

[PROOFSTEP]
done
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, Finset.max s = ↑a → a ∈ s
[PROOFSTEP]
induction' s using Finset.induction_on with b s _ ih
[GOAL]
case empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
⊢ ∀ {a : α}, Finset.max ∅ = ↑a → a ∈ ∅
[PROOFSTEP]
intro _ H
[GOAL]
case empty
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
a✝ : α
H : Finset.max ∅ = ↑a✝
⊢ a✝ ∈ ∅
[PROOFSTEP]
cases H
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
⊢ ∀ {a : α}, Finset.max (insert b s) = ↑a → a ∈ insert b s
[PROOFSTEP]
intro a h
[GOAL]
case insert
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
⊢ a ∈ insert b s
[PROOFSTEP]
by_cases p : b = a
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : b = a
⊢ a ∈ insert b s
[PROOFSTEP]
induction p
[GOAL]
case pos.refl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑b
⊢ b ∈ insert b s
[PROOFSTEP]
exact mem_insert_self b s
[GOAL]
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : ¬b = a
⊢ a ∈ insert b s
[PROOFSTEP]
cases' max_choice (↑b) s.max with q q
[GOAL]
case neg.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = ↑b
⊢ a ∈ insert b s
[PROOFSTEP]
rw [max_insert, q] at h
[GOAL]
case neg.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = Finset.max s
⊢ a ∈ insert b s
[PROOFSTEP]
rw [max_insert, q] at h
[GOAL]
case neg.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : ↑b = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = ↑b
⊢ a ∈ insert b s
[PROOFSTEP]
cases h
[GOAL]
case neg.inl.refl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
q : max (↑b) (Finset.max s) = ↑b
p : ¬b = b
⊢ b ∈ insert b s
[PROOFSTEP]
cases p rfl
[GOAL]
case neg.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max s = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = Finset.max s
⊢ a ∈ insert b s
[PROOFSTEP]
exact mem_insert_of_mem (ih h)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
a : α
⊢ Finset.min {a} = ↑a
[PROOFSTEP]
rw [← insert_emptyc_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
a : α
⊢ Finset.min (insert a ∅) = ↑a
[PROOFSTEP]
exact min_insert
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ b, Finset.min s = ↑b
[PROOFSTEP]
obtain ⟨b, h, _⟩ := inf_le (α := WithTop α) h _ rfl
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : b ∈ inf s some
right✝ : b ≤ a
⊢ ∃ b, Finset.min s = ↑b
[PROOFSTEP]
exact ⟨b, h⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
h : Finset.min s = ⊤
H : Finset.Nonempty s
⊢ s = ∅
[PROOFSTEP]
let ⟨a, ha⟩ := min_of_nonempty H
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
h : Finset.min s = ⊤
H : Finset.Nonempty s
a : α
ha : Finset.min s = ↑a
⊢ s = ∅
[PROOFSTEP]
rw [h] at ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
h : Finset.min s = ⊤
H : Finset.Nonempty s
a : α
ha : ⊤ = ↑a
⊢ s = ∅
[PROOFSTEP]
cases ha
[GOAL]

[PROOFSTEP]
done
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ Finset.min s = ↑(min' s H)
[PROOFSTEP]
simp only [Finset.min, min', id_eq, coe_inf']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ inf s WithTop.some = inf s (WithTop.some ∘ fun x => x)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x a : α
⊢ min' {a} (_ : Finset.Nonempty {a}) = a
[PROOFSTEP]
simp [min']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ Finset.max s = ↑(max' s H)
[PROOFSTEP]
simp only [max', Finset.max, id_eq, coe_sup']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ sup s WithBot.some = sup s (WithBot.some ∘ fun x => x)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x a : α
⊢ max' {a} (_ : Finset.Nonempty {a}) = a
[PROOFSTEP]
simp [max']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
h₂ : 1 < card s
⊢ min' s (_ : Finset.Nonempty s) < max' s (_ : Finset.Nonempty s)
[PROOFSTEP]
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
h₂ : 1 < card s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ min' s (_ : Finset.Nonempty s) < max' s (_ : Finset.Nonempty s)
[PROOFSTEP]
exact s.min'_lt_max' ha hb hab
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
⊢ WithTop.map (↑ofDual) (Finset.min s) = Finset.max (image (↑ofDual) s)
[PROOFSTEP]
rw [max_eq_sup_withBot, sup_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
⊢ WithTop.map (↑ofDual) (Finset.min s) = sup s (WithBot.some ∘ ↑ofDual)
[PROOFSTEP]
exact congr_fun Option.map_id _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
⊢ WithBot.map (↑ofDual) (Finset.max s) = Finset.min (image (↑ofDual) s)
[PROOFSTEP]
rw [min_eq_inf_withTop, inf_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
⊢ WithBot.map (↑ofDual) (Finset.max s) = inf s (WithTop.some ∘ ↑ofDual)
[PROOFSTEP]
exact congr_fun Option.map_id _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithTop.map (↑toDual) (Finset.min s) = Finset.max (image (↑toDual) s)
[PROOFSTEP]
rw [max_eq_sup_withBot, sup_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithTop.map (↑toDual) (Finset.min s) = sup s (WithBot.some ∘ ↑toDual)
[PROOFSTEP]
exact congr_fun Option.map_id _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithBot.map (↑toDual) (Finset.max s) = Finset.min (image (↑toDual) s)
[PROOFSTEP]
rw [min_eq_inf_withTop, inf_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ WithBot.map (↑toDual) (Finset.max s) = inf s (WithTop.some ∘ ↑toDual)
[PROOFSTEP]
exact congr_fun Option.map_id _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑ofDual (min' s hs) = max' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s))
[PROOFSTEP]
rw [← WithBot.coe_eq_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑(↑ofDual (min' s hs)) = ↑(max' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s)))
[PROOFSTEP]
simp only [min'_eq_inf', id_eq, ofDual_inf', Function.comp_apply, coe_sup', max'_eq_sup', sup_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ sup s (WithBot.some ∘ fun x => ↑ofDual x) = sup s ((WithBot.some ∘ fun x => x) ∘ ↑ofDual)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑ofDual (max' s hs) = min' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s))
[PROOFSTEP]
rw [← WithTop.coe_eq_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ ↑(↑ofDual (max' s hs)) = ↑(min' (image (↑ofDual) s) (_ : Finset.Nonempty (image (↑ofDual) s)))
[PROOFSTEP]
simp only [max'_eq_sup', id_eq, ofDual_sup', Function.comp_apply, coe_inf', min'_eq_inf', inf_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset αᵒᵈ
hs : Finset.Nonempty s
⊢ inf s (WithTop.some ∘ fun x => ↑ofDual x) = inf s ((WithTop.some ∘ fun x => x) ∘ ↑ofDual)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑toDual (min' s hs) = max' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s))
[PROOFSTEP]
rw [← WithBot.coe_eq_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(↑toDual (min' s hs)) = ↑(max' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s)))
[PROOFSTEP]
simp only [min'_eq_inf', id_eq, toDual_inf', Function.comp_apply, coe_sup', max'_eq_sup', sup_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ sup s (WithBot.some ∘ fun x => ↑toDual x) = sup s ((WithBot.some ∘ fun x => x) ∘ ↑toDual)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑toDual (max' s hs) = min' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s))
[PROOFSTEP]
rw [← WithTop.coe_eq_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(↑toDual (max' s hs)) = ↑(min' (image (↑toDual) s) (_ : Finset.Nonempty (image (↑toDual) s)))
[PROOFSTEP]
simp only [max'_eq_sup', id_eq, toDual_sup', Function.comp_apply, coe_inf', min'_eq_inf', inf_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
hs : Finset.Nonempty s
⊢ inf s (WithTop.some ∘ fun x => ↑toDual x) = inf s ((WithTop.some ∘ fun x => x) ∘ ↑toDual)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsGreatest (↑(insert a s)) (max (max' s H) a)
[PROOFSTEP]
rw [coe_insert, max_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsGreatest (insert a ↑s) (max a (max' s H))
[PROOFSTEP]
exact (isGreatest_max' _ _).insert _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsLeast (↑(insert a s)) (min (min' s H) a)
[PROOFSTEP]
rw [coe_insert, min_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsLeast (insert a ↑s) (min a (min' s H))
[PROOFSTEP]
exact (isLeast_min' _ _).insert _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
⊢ max' (image f s) h = f (max' s (_ : Finset.Nonempty s))
[PROOFSTEP]
refine' le_antisymm (max'_le _ _ _ fun y hy => _) (le_max' _ _ (mem_image.mpr ⟨_, max'_mem _ _, rfl⟩))
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
y : β
hy : y ∈ image f s
⊢ y ≤ f (max' s (_ : Finset.Nonempty s))
[PROOFSTEP]
obtain ⟨x, hx, rfl⟩ := mem_image.mp hy
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
x : α
hx : x ∈ s
hy : f x ∈ image f s
⊢ f x ≤ f (max' s (_ : Finset.Nonempty s))
[PROOFSTEP]
exact hf (le_max' _ _ hx)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
⊢ min' (image f s) h = f (min' s (_ : Finset.Nonempty s))
[PROOFSTEP]
refine' le_antisymm (min'_le _ _ (mem_image.mpr ⟨_, min'_mem _ _, rfl⟩)) (le_min' _ _ _ fun y hy => _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
y : β
hy : y ∈ image f s
⊢ f (min' s (_ : Finset.Nonempty s)) ≤ y
[PROOFSTEP]
obtain ⟨x, hx, rfl⟩ := mem_image.mp hy
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : Finset.Nonempty (image f s)
x : α
hx : x ∈ s
hy : f x ∈ image f s
⊢ f (min' s (_ : Finset.Nonempty s)) ≤ f x
[PROOFSTEP]
exact hf (min'_le _ _ hx)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ Finset.max (erase s x) ≠ ↑x
[PROOFSTEP]
by_cases s0 : (s.erase x).Nonempty
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : Finset.Nonempty (erase s x)
⊢ Finset.max (erase s x) ≠ ↑x
[PROOFSTEP]
refine' ne_of_eq_of_ne (coe_max' s0).symm _
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : Finset.Nonempty (erase s x)
⊢ ↑(max' (erase s x) s0) ≠ ↑x
[PROOFSTEP]
exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
[GOAL]
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : ¬Finset.Nonempty (erase s x)
⊢ Finset.max (erase s x) ≠ ↑x
[PROOFSTEP]
rw [not_nonempty_iff_eq_empty.mp s0, max_empty]
[GOAL]
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
s0 : ¬Finset.Nonempty (erase s x)
⊢ ⊥ ≠ ↑x
[PROOFSTEP]
exact WithBot.bot_ne_coe
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
⊢ Finset.min (erase s x) ≠ ↑x
[PROOFSTEP]
convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding) using 1
[GOAL]
case h.e'_2.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ Finset.min (erase s x) = Finset.max (erase (map (Equiv.toEmbedding toDual) s) (↑toDual x))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.e'_2.h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ erase s x = erase (map (Equiv.toEmbedding toDual) s) (↑toDual x)
[PROOFSTEP]
congr!
[GOAL]
case h.e'_2.h.h.h.e'_3.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ s = map (Equiv.toEmbedding toDual) s
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.h.h.e'_3.h.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ map (Equiv.toEmbedding toDual) s
[PROOFSTEP]
simp only [mem_map_equiv]
[GOAL]
case h.e'_2.h.h.h.e'_3.h.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ ↑toDual.symm a✝ ∈ s
[PROOFSTEP]
exact Iff.rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ x : α
s : Finset α
h : ∃ y, y ∈ s ∧ x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ (fun x x_1 => x < x_1) x y
[PROOFSTEP]
simpa
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ x : α
s : Finset α
h : ∃ y, y ∈ s ∧ x < y
Hne : Finset.Nonempty (filter ((fun x x_1 => x < x_1) x) s)
aux :
  min' (filter ((fun x x_1 => x < x_1) x) s) Hne ∈ s ∧
    (fun x x_1 => x < x_1) x (min' (filter ((fun x x_1 => x < x_1) x) s) Hne)
⊢ x < min' (filter ((fun x x_1 => x < x_1) x) s) Hne
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ x : α
s : Finset α
h : ∃ y, y ∈ s ∧ x < y
Hne : Finset.Nonempty (filter ((fun x x_1 => x < x_1) x) s)
aux :
  min' (filter ((fun x x_1 => x < x_1) x) s) Hne ∈ s ∧
    (fun x x_1 => x < x_1) x (min' (filter ((fun x x_1 => x < x_1) x) s) Hne)
z : α
hzs : z ∈ s
hz : x < z
⊢ (fun x x_1 => x < x_1) x z
[PROOFSTEP]
simpa
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ card s ≤ card t + 1
[PROOFSTEP]
replace h : ∀ (x) (_ : x ∈ s) (y) (_ : y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
[PROOFSTEP]
rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
[GOAL]
case h.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ (z : α), z ∈ s → x < z → a ≤ z
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
[PROOFSTEP]
rcases h x hx a has hxa fun z hzs hz => hz.2.not_le <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → ¬z ∈ Set.Ioo x y) → ∃ z, z ∈ t ∧ x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ (z : α), z ∈ s → x < z → a ≤ z
b : α
hbt : b ∈ t
hxb : x < b
hba : b < a
⊢ ∃ z, z ∈ t ∧ x < z ∧ z < y
[PROOFSTEP]
exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
⊢ card s ≤ card t + 1
[PROOFSTEP]
set f : α → WithTop α := fun x => (t.filter fun y => x < y).min
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
⊢ card s ≤ card t + 1
[PROOFSTEP]
have f_mono : StrictMonoOn f s := by
  intro x hx y hy hxy
  rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
  calc
    f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
    _ < f y :=
      (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
        WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
⊢ StrictMonoOn f ↑s
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
⊢ f x < f y
[PROOFSTEP]
rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ f x < f y
[PROOFSTEP]
calc
  f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
  _ < f y :=
    (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
      WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a
[PROOFSTEP]
simpa
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ filter (fun y_1 => y < y_1) t
⊢ y < b
[PROOFSTEP]
simpa using (mem_filter.1 hb).2
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
s t : Finset α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → ∃ z, z ∈ t ∧ x < z ∧ z < y
f : α → WithTop α := fun x => Finset.min (filter (fun y => x < y) t)
f_mono : StrictMonoOn f ↑s
⊢ card s ≤ card t + 1
[PROOFSTEP]
calc
  s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
  _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
    (card_mono <|
      image_subset_iff.2 fun x _ =>
        insert_subset_insert _ (image_subset_image <| filter_subset _ _) (min_mem_insert_top_image_coe _))
  _ ≤ t.card + 1 := (card_insert_le _ _).trans (add_le_add_right card_image_le _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
s : Finset α
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
⊢ p s
[PROOFSTEP]
induction' s using Finset.strongInductionOn with s ihs
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
⊢ p s
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hne)
[GOAL]
case a.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
ihs : ∀ (t : Finset α), t ⊂ ∅ → p t
⊢ p ∅
[PROOFSTEP]
exact h0
[GOAL]
case a.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
⊢ p s
[PROOFSTEP]
have H : s.max' hne ∈ s := max'_mem s hne
[GOAL]
case a.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
H : max' s hne ∈ s
⊢ p s
[PROOFSTEP]
rw [← insert_erase H]
[GOAL]
case a.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
H : max' s hne ∈ s
⊢ p (insert (max' s hne) (erase s (max' s hne)))
[PROOFSTEP]
exact step _ _ (fun x => s.lt_max'_of_mem_erase_max' hne) (ihs _ <| erase_ssubset H)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
s : Finset ι
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
⊢ p s
[PROOFSTEP]
induction' s using Finset.strongInductionOn with s ihs
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
⊢ p s
[PROOFSTEP]
rcases(s.image f).eq_empty_or_nonempty with (hne | hne)
[GOAL]
case a.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : image f s = ∅
⊢ p s
[PROOFSTEP]
simp only [image_eq_empty] at hne
[GOAL]
case a.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : s = ∅
⊢ p s
[PROOFSTEP]
simp only [hne, h0]
[GOAL]
case a.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
⊢ p s
[PROOFSTEP]
have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
[GOAL]
case a.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
H : max' (image f s) hne ∈ image f s
⊢ p s
[PROOFSTEP]
simp only [mem_image, exists_prop] at H
[GOAL]
case a.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
H : ∃ a, a ∈ s ∧ f a = max' (image f s) hne
⊢ p s
[PROOFSTEP]
rcases H with ⟨a, has, hfa⟩
[GOAL]
case a.inr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
⊢ p s
[PROOFSTEP]
rw [← insert_erase has]
[GOAL]
case a.inr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
⊢ p (insert a (erase s a))
[PROOFSTEP]
refine' step _ _ (not_mem_erase a s) (fun x hx => _) (ihs _ <| erase_ssubset has)
[GOAL]
case a.inr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
x : ι
hx : x ∈ erase s a
⊢ f x ≤ f a
[PROOFSTEP]
rw [hfa]
[GOAL]
case a.inr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
x : ι
hx : x ∈ erase s a
⊢ f x ≤ max' (image f s) hne
[PROOFSTEP]
exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
[PROOFSTEP]
cases' max_of_nonempty (h.image f) with y hy
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
y : α
hy : Finset.max (image f s) = ↑y
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
[PROOFSTEP]
rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : Finset.Nonempty s
x : β
hx : x ∈ s
hy : Finset.max (image f s) = ↑(f x)
⊢ ∃ x, x ∈ s ∧ ∀ (x' : β), x' ∈ s → f x' ≤ f x
[PROOFSTEP]
exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
⊢ IsGLB (↑s) i ↔ IsLeast (↑s) i
[PROOFSTEP]
refine' ⟨fun his => _, IsLeast.isGLB⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i
[PROOFSTEP]
suffices i = min' s hs by
  rw [this]
  exact isLeast_min' s hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
this : i = min' s hs
⊢ IsLeast (↑s) i
[PROOFSTEP]
rw [this]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
this : i = min' s hs
⊢ IsLeast (↑s) (min' s hs)
[PROOFSTEP]
exact isLeast_min' s hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : IsGLB (↑s) i
⊢ i = min' s hs
[PROOFSTEP]
rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
hs : Finset.Nonempty s
his : (∀ (x : α), x ∈ ↑s → i ≤ x) ∧ ∀ (x : α), x ∈ lowerBounds ↑s → x ≤ i
⊢ i = min' s hs
[PROOFSTEP]
exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : Finset.Nonempty s
⊢ i ∈ s
[PROOFSTEP]
rw [← mem_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : Finset.Nonempty s
⊢ i ∈ ↑s
[PROOFSTEP]
exact ((isGLB_iff_isLeast i s hs).mp his).1
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
⊢ count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
[PROOFSTEP]
refine' s.induction _ _
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup ∅ f) = Finset.sup ∅ fun a => count b (f a)
[PROOFSTEP]
exact count_zero _
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)) →
        count b (Finset.sup (insert a s) f) = Finset.sup (insert a s) fun a => count b (f a)
[PROOFSTEP]
intro i s _ ih
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : ¬i ∈ s
ih : count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
⊢ count b (Finset.sup (insert i s) f) = Finset.sup (insert i s) fun a => count b (f a)
[PROOFSTEP]
rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : ¬i ∈ s
ih : count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
⊢ max (count b (f i)) (Finset.sup s fun a => count b (f a)) = count b (f i) ⊔ Finset.sup s fun a => count b (f a)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s has hxs
· simp
· rw [Finset.sup_insert, Multiset.sup_eq_union, Multiset.mem_union]
  constructor
  · intro hxi
    cases' hxi with hf hf
    · refine' ⟨a, _, hf⟩
      simp only [true_or_iff, eq_self_iff_true, Finset.mem_insert]
    · rcases hxs.mp hf with ⟨v, hv, hfv⟩
      refine' ⟨v, _, hfv⟩
      simp only [hv, or_true_iff, Finset.mem_insert]
  · rintro ⟨v, hv, hfv⟩
    rw [Finset.mem_insert] at hv
    rcases hv with (rfl | hv)
    · exact Or.inl hfv
    · refine' Or.inr (hxs.mpr ⟨v, hv, hfv⟩)
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
[PROOFSTEP]
induction' s using Finset.induction_on with a s has hxs
[GOAL]
case empty
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup ∅ f ↔ ∃ v, v ∈ ∅ ∧ x ∈ f v
[PROOFSTEP]
simp
[GOAL]
case insert
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ Finset.sup (insert a s) f ↔ ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
rw [Finset.sup_insert, Multiset.sup_eq_union, Multiset.mem_union]
[GOAL]
case insert
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f ↔ ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f → ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
intro hxi
[GOAL]
case insert.mp
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hxi : x ∈ f a ∨ x ∈ Finset.sup s f
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
cases' hxi with hf hf
[GOAL]
case insert.mp.inl
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ f a
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
refine' ⟨a, _, hf⟩
[GOAL]
case insert.mp.inl
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ f a
⊢ a ∈ insert a s
[PROOFSTEP]
simp only [true_or_iff, eq_self_iff_true, Finset.mem_insert]
[GOAL]
case insert.mp.inr
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
rcases hxs.mp hf with ⟨v, hv, hfv⟩
[GOAL]
case insert.mp.inr.intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
v : α
hv : v ∈ s
hfv : x ∈ f v
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
[PROOFSTEP]
refine' ⟨v, _, hfv⟩
[GOAL]
case insert.mp.inr.intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
v : α
hv : v ∈ s
hfv : x ∈ f v
⊢ v ∈ insert a s
[PROOFSTEP]
simp only [hv, or_true_iff, Finset.mem_insert]
[GOAL]
case insert.mpr
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ (∃ v, v ∈ insert a s ∧ x ∈ f v) → x ∈ f a ∨ x ∈ Finset.sup s f
[PROOFSTEP]
rintro ⟨v, hv, hfv⟩
[GOAL]
case insert.mpr.intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hv : v ∈ insert a s
hfv : x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
[PROOFSTEP]
rw [Finset.mem_insert] at hv
[GOAL]
case insert.mpr.intro.intro
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hv : v = a ∨ v ∈ s
hfv : x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
[PROOFSTEP]
rcases hv with (rfl | hv)
[GOAL]
case insert.mpr.intro.intro.inl
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
s : Finset α
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hfv : x ∈ f v
has : ¬v ∈ s
⊢ x ∈ f v ∨ x ∈ Finset.sup s f
[PROOFSTEP]
exact Or.inl hfv
[GOAL]
case insert.mpr.intro.intro.inr
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hfv : x ∈ f v
hv : v ∈ s
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
[PROOFSTEP]
refine' Or.inr (hxs.mpr ⟨v, hv, hfv⟩)
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
[PROOFSTEP]
change _ ↔ ∃ v ∈ s, x ∈ (f v).val
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ ∃ v, v ∈ s ∧ x ∈ (f v).val
[PROOFSTEP]
rw [← Multiset.mem_sup, ← Multiset.mem_toFinset, sup_toFinset]
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
x : β
⊢ x ∈ sup s f ↔ x ∈ sup s fun x => Multiset.toFinset (f x).val
[PROOFSTEP]
simp_rw [val_toFinset]
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
⊢ sup s t = Finset.biUnion s t
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ a✝ ∈ sup s t ↔ a✝ ∈ Finset.biUnion s t
[PROOFSTEP]
rw [mem_sup, mem_biUnion]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq α
s : Finset β
f : β → α
⊢ (sup s fun b => {f b}) = image f s
[PROOFSTEP]
ext a
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ sup s fun b => {f b}) ↔ a ∈ image f s
[PROOFSTEP]
rw [mem_sup, mem_image]
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ v, v ∈ s ∧ a ∈ {f v}) ↔ ∃ a_1, a_1 ∈ s ∧ f a_1 = a
[PROOFSTEP]
simp only [mem_singleton, eq_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ (i : ι), s i = ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
classical
refine le_antisymm ?_ ?_
· exact iSup_le fun b => le_iSup_of_le { b } <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
· exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ (i : ι), s i = ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
refine le_antisymm ?_ ?_
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ (i : ι), s i ≤ ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
exact iSup_le fun b => le_iSup_of_le { b } <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι → α
b : ι
⊢ b ∈ {b}
[PROOFSTEP]
simp
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ (t : Finset ι) (i : ι) (_ : i ∈ t), s i ≤ ⨆ (i : ι), s i
[PROOFSTEP]
exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ (i : ι'), s i = ⨆ (t : Finset (PLift ι')) (i : PLift ι') (_ : i ∈ t), s i.down
[PROOFSTEP]
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ (x : PLift ι'), s (↑Equiv.plift x) = ⨆ (i : PLift ι'), s i.down
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨆ (x : α) (_ : x ∈ {a}), s x = s a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨅ (x : α) (_ : x ∈ {a}), s x = s a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : CompleteLattice β
o : Option α
f : α → β
⊢ ⨆ (x : α) (_ : x ∈ Option.toFinset o), f x = ⨆ (x : α) (_ : x ∈ o), f x
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
⊢ ⨆ (x : α) (_ : x ∈ s ∪ t), f x = (⨆ (x : α) (_ : x ∈ s), f x) ⊔ ⨆ (x : α) (_ : x ∈ t), f x
[PROOFSTEP]
simp [iSup_or, iSup_sup_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ (x : α) (_ : x ∈ insert a s), t x = t a ⊔ ⨆ (x : α) (_ : x ∈ s), t x
[PROOFSTEP]
rw [insert_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
a : α
s : Finset α
t : α → β
⊢ ⨆ (x : α) (_ : x ∈ {a} ∪ s), t x = t a ⊔ ⨆ (x : α) (_ : x ∈ s), t x
[PROOFSTEP]
simp only [iSup_union, Finset.iSup_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ ⨆ (x : α) (_ : x ∈ image f s), g x = ⨆ (y : γ) (_ : y ∈ s), g (f y)
[PROOFSTEP]
rw [← iSup_coe, coe_image, iSup_image, iSup_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ ⨅ (x : α) (_ : x ∈ image f s), g x = ⨅ (y : γ) (_ : y ∈ s), g (f y)
[PROOFSTEP]
rw [← iInf_coe, coe_image, iInf_image, iInf_coe]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
⊢ ⨆ (i : α) (_ : i ∈ insert x t), update f x s i = s ⊔ ⨆ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
simp only [Finset.iSup_insert, update_same]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
⊢ s ⊔ ⨆ (x_1 : α) (_ : x_1 ∈ t), update f x s x_1 = s ⊔ ⨆ (i : α) (_ : i ∈ t), f i
[PROOFSTEP]
rcongr (i hi)
[GOAL]
case e_a.e_s.h.e_s.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
i : α
hi : i ∈ t
⊢ update f x s i = f i
[PROOFSTEP]
apply update_noteq
[GOAL]
case e_a.e_s.h.e_s.h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : ¬x ∈ t
i : α
hi : i ∈ t
⊢ i ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
case e_a.e_s.h.e_s.h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
t : Finset α
f : α → β
s : β
i : α
hi : i ∈ t
hx : ¬i ∈ t
⊢ False
[PROOFSTEP]
exact hx hi
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → β
⊢ ⨆ (y : α) (_ : y ∈ Finset.biUnion s t), f y = ⨆ (x : γ) (_ : x ∈ s) (y : α) (_ : y ∈ t x), f y
[PROOFSTEP]
simp [@iSup_comm _ α, iSup_and]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
s : Finset α
f : α → Set β
x : α
h : x ∈ s
⊢ f x ≤ ⨆ (_ : x ∈ s), f x
[PROOFSTEP]
simp only [h, iSup_pos, le_refl]