Theorem: Finset.sup_filter_eq_sup_univ_subtype_coe (ForML/PiEquiv.lean)

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup univ fun i => f ↑i
Tactic:
rw [← Finset.subtype_univ]
State after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (Finset.subtype (fun a => p a) univ) fun i => f ↑i

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (Finset.subtype (fun a => p a) univ) fun i => f ↑i
Tactic:
rw [Finset.subtype]
State after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup
      (map
        { toFun := fun x => { val := ↑x, property := (_ : p ↑x) },
          inj' :=
            (_ :
              ∀ (x y : { x // x ∈ filter (fun a => p a) univ }),
                (fun x => { val := ↑x, property := (_ : p ↑x) }) x =
                    (fun x => { val := ↑x, property := (_ : p ↑x) }) y →
                  x = y) }
        (attach (filter (fun a => p a) univ)))
      fun i => f ↑i

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup
      (map
        { toFun := fun x => { val := ↑x, property := (_ : p ↑x) },
          inj' :=
            (_ :
              ∀ (x y : { x // x ∈ filter (fun a => p a) univ }),
                (fun x => { val := ↑x, property := (_ : p ↑x) }) x =
                    (fun x => { val := ↑x, property := (_ : p ↑x) }) y →
                  x = y) }
        (attach (filter (fun a => p a) univ)))
      fun i => f ↑i
Tactic:
simp
State after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup (attach (filter (fun a => p a) univ)) ((fun i => f ↑i) ∘ fun x => { val := ↑x, property := (_ : p ↑x) })

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup (attach (filter (fun a => p a) univ)) ((fun i => f ↑i) ∘ fun x => { val := ↑x, property := (_ : p ↑x) })
Tactic:
conv => rhs; arg 2; intro x; simp
State after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (attach (filter (fun a => p a) univ)) fun x => f ↑x

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (attach (filter (fun a => p a) univ)) fun x => f ↑x
Tactic:
rw [sup_attach]
State after:
no goals