[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
x✝ : Set C(α, β)
⊢ x✝ ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} ↔ x✝ ∈ image2 CompactOpen.gen {s | IsCompact s} {t | IsOpen t}
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
dsimp [mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ s_1 x u_1 x, CompactOpen.gen s u = CompactOpen.gen s_1 u_1
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
s : Set α
u : Set γ
⊢ comp g ⁻¹' CompactOpen.gen s u = CompactOpen.gen s (↑g ⁻¹' u)
[PROOFSTEP]
ext ⟨f, _⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
s : Set α
u : Set γ
f : α → β
continuous_toFun✝ : Continuous f
⊢ mk f ∈ comp g ⁻¹' CompactOpen.gen s u ↔ mk f ∈ CompactOpen.gen s (↑g ⁻¹' u)
[PROOFSTEP]
change g ∘ f '' s ⊆ u ↔ f '' s ⊆ g ⁻¹' u
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
s : Set α
u : Set γ
f : α → β
continuous_toFun✝ : Continuous f
⊢ ↑g ∘ f '' s ⊆ u ↔ f '' s ⊆ ↑g ⁻¹' u
[PROOFSTEP]
rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (comp g ⁻¹' m)
[PROOFSTEP]
rw [hm, preimage_gen g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (CompactOpen.gen s (↑g ⁻¹' u))
[PROOFSTEP]
exact ContinuousMap.isOpen_gen hs (hu.preimage g.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
hg : Inducing ↑g
⊢ compactOpen = TopologicalSpace.induced (comp g) compactOpen
[PROOFSTEP]
simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, preimage_gen, hg.setOf_isOpen, image2_image_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
⊢ (fun g => comp g f) ⁻¹' CompactOpen.gen s u = CompactOpen.gen (↑f '' s) u
[PROOFSTEP]
ext ⟨g, _⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ mk g ∈ (fun g => comp g f) ⁻¹' CompactOpen.gen s u ↔ mk g ∈ CompactOpen.gen (↑f '' s) u
[PROOFSTEP]
change g ∘ f '' s ⊆ u ↔ g '' (f '' s) ⊆ u
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ g ∘ ↑f '' s ⊆ u ↔ g '' (↑f '' s) ⊆ u
[PROOFSTEP]
rw [Set.image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen ((fun g => comp g f) ⁻¹' m)
[PROOFSTEP]
rw [hm, image_gen f hs hu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (CompactOpen.gen (↑f '' s) u)
[PROOFSTEP]
exact ContinuousMap.isOpen_gen (hs.image f.2) hu
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
⊢ ∀ (s : Set C(α, γ)), s ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} → IsOpen ((fun x => comp x.snd x.fst) ⁻¹' s)
[PROOFSTEP]
rintro M ⟨K, hK, U, hU, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
conv =>
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
    --congr
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
    --congr
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
    --congr
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
congr
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| (fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U
[PROOFSTEP]
rw [CompactOpen.gen, preimage_setOf_eq]
  --congr
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| {a | ↑(comp a.snd a.fst) '' K ⊆ U}
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
x✝ : C(α, β) × C(β, γ)
| setOf (fun a => ↑(comp a.snd a.fst) '' K ⊆ U) x✝
[PROOFSTEP]
dsimp [setOf]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
x✝ : C(α, β) × C(β, γ)
| ↑x✝.snd ∘ ↑x✝.fst '' K ⊆ U
[PROOFSTEP]
rw [image_comp, image_subset_iff]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
[PROOFSTEP]
rw [isOpen_iff_forall_mem_open]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ ∀ (x : C(α, β) × C(β, γ)),
    (x ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) → ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rintro ⟨φ₀, ψ₀⟩ H
[GOAL]
case intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
[PROOFSTEP]
obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between (hK.image φ₀.2) (hU.preimage ψ₀.2) H
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
[PROOFSTEP]
use{φ : C(α, β) | φ '' K ⊆ interior L} ×ˢ
    {ψ : C(β, γ) | ψ '' L ⊆ U}
      -- porting note: typing hint `: φ '' K ⊆ interior L` wasn't previously required
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U} ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧
    IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧
      (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
[PROOFSTEP]
use fun ⟨φ, ψ⟩ ⟨(hφ : φ '' K ⊆ interior L), hψ⟩ => subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
[PROOFSTEP]
use(ContinuousMap.isOpen_gen hK isOpen_interior).prod (ContinuousMap.isOpen_gen hL hU)
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
[PROOFSTEP]
exact mem_prod.mpr ⟨hKL, image_subset_iff.mpr hLU⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace α
x✝ : C(α, β) × α
n : Set β
f : C(α, β)
x : α
hn : n ∈ 𝓝 (↑(f, x).fst (f, x).snd)
v : Set β
vn : v ⊆ n
vo : IsOpen v
fxv : ↑(f, x).fst (f, x).snd ∈ v
this✝² : v ∈ 𝓝 (↑f x)
s : Set α
hs : s ∈ 𝓝 x
sv : s ⊆ ↑f ⁻¹' v
sc : IsCompact s
u : Set α
us : u ⊆ s
uo : IsOpen u
xu : x ∈ u
w : Set (C(α, β) × α) := CompactOpen.gen s v ×ˢ u
this✝¹ : w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
this✝ : IsOpen w
this : (f, x) ∈ w
⊢ w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace α
x✝ : C(α, β) × α
n : Set β
f : C(α, β)
x : α
hn : n ∈ 𝓝 (↑(f, x).fst (f, x).snd)
v : Set β
vn : v ⊆ n
vo : IsOpen v
fxv : ↑(f, x).fst (f, x).snd ∈ v
this✝² : v ∈ 𝓝 (↑f x)
s : Set α
hs : s ∈ 𝓝 x
sv : s ⊆ ↑f ⁻¹' v
sc : IsCompact s
u : Set α
us : u ⊆ s
uo : IsOpen u
xu : x ∈ u
w : Set (C(α, β) × α) := CompactOpen.gen s v ×ˢ u
this✝¹ : w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
this✝ : IsOpen w
this : (f, x) ∈ w
⊢ IsOpen w
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace α
x✝ : C(α, β) × α
n : Set β
f : C(α, β)
x : α
hn : n ∈ 𝓝 (↑(f, x).fst (f, x).snd)
v : Set β
vn : v ⊆ n
vo : IsOpen v
fxv : ↑(f, x).fst (f, x).snd ∈ v
this✝² : v ∈ 𝓝 (↑f x)
s : Set α
hs : s ∈ 𝓝 x
sv : s ⊆ ↑f ⁻¹' v
sc : IsCompact s
u : Set α
us : u ⊆ s
uo : IsOpen u
xu : x ∈ u
w : Set (C(α, β) × α) := CompactOpen.gen s v ×ˢ u
this✝¹ : w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
this✝ : IsOpen w
this : (f, x) ∈ w
⊢ (f, x) ∈ w
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
⊢ Continuous fun f => ↑f a
[PROOFSTEP]
refine continuous_def.2 fun U hU ↦ ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
U : Set ((fun x => β) a)
hU : IsOpen U
⊢ IsOpen ((fun f => ↑f a) ⁻¹' U)
[PROOFSTEP]
convert ContinuousMap.isOpen_gen (isCompact_singleton (a := a)) hU using 1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
U : Set ((fun x => β) a)
hU : IsOpen U
⊢ (fun f => ↑f a) ⁻¹' U = CompactOpen.gen {a} U
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
U : Set ((fun x => β) a)
hU : IsOpen U
x✝ : C(α, β)
⊢ x✝ ∈ (fun f => ↑f a) ⁻¹' U ↔ x✝ ∈ CompactOpen.gen {a} U
[PROOFSTEP]
simp [CompactOpen.gen]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ compactOpen ≤ TopologicalSpace.induced (restrict s) compactOpen
[PROOFSTEP]
simp only [induced_generateFrom_eq, ContinuousMap.compactOpen]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} ≤
    TopologicalSpace.generateFrom (preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u})
[PROOFSTEP]
apply TopologicalSpace.generateFrom_anti
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u} ⊆ {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
rintro b ⟨a, ⟨c, hc, u, hu, rfl⟩, rfl⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
refine' ⟨(↑) '' c, hc.image continuous_subtype_val, u, hu, _⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u = CompactOpen.gen (Subtype.val '' c) u
[PROOFSTEP]
ext f
[GOAL]
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen c u ↔ f ∈ CompactOpen.gen (Subtype.val '' c) u
[PROOFSTEP]
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
[GOAL]
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' c ⊆ u ↔ (fun a => ↑f a) '' (Subtype.val '' c) ⊆ u
[PROOFSTEP]
rw [image_comp f ((↑) : s → α)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen = ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen ≤ ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen
[PROOFSTEP]
refine' le_iInf₂ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (i : Set α), IsCompact i → compactOpen ≤ TopologicalSpace.induced (restrict i) compactOpen
[PROOFSTEP]
exact fun s _ => compactOpen_le_induced s
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen ≤ compactOpen
[PROOFSTEP]
simp only [← generateFrom_iUnion, induced_generateFrom_eq, ContinuousMap.compactOpen]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ TopologicalSpace.generateFrom
      (⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}) ≤
    TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
apply TopologicalSpace.generateFrom_anti
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ {m | ∃ s x u x, m = CompactOpen.gen s u} ⊆
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
rintro _ ⟨s, hs, u, hu, rfl⟩
[GOAL]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
rw [mem_iUnion₂]
[GOAL]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ i j, CompactOpen.gen s u ∈ preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
refine' ⟨s, hs, _, ⟨univ, isCompact_iff_isCompact_univ.mp hs, u, hu, rfl⟩, _⟩
[GOAL]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen univ u = CompactOpen.gen s u
[PROOFSTEP]
ext f
[GOAL]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen univ u ↔ f ∈ CompactOpen.gen s u
[PROOFSTEP]
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
[GOAL]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' univ ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
[PROOFSTEP]
rw [image_comp f ((↑) : s → α)]
[GOAL]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ ↑f '' (Subtype.val '' univ) ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ Continuous fun F => restrict s F
[PROOFSTEP]
rw [continuous_iff_le_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ compactOpen ≤ TopologicalSpace.induced (fun F => restrict s F) compactOpen
[PROOFSTEP]
exact compactOpen_le_induced s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
[PROOFSTEP]
rw [compactOpen_eq_sInf_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
[PROOFSTEP]
simp [nhds_iInf, nhds_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
[PROOFSTEP]
rw [compactOpen_eq_sInf_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
[PROOFSTEP]
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) ↔ ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) → ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
[PROOFSTEP]
rintro ⟨f, hf⟩ s _
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : C(α, β)
hf : Filter.Tendsto F l (𝓝 f)
s : Set α
hs✝ : IsCompact s
⊢ ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
[PROOFSTEP]
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)) → ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
h : ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
choose f hf using h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
have h :
  ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ :=
  by
  rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
  haveI := isCompact_iff_compactSpace.mp hs₁
  haveI := isCompact_iff_compactSpace.mp hs₂
  have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
  have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
  exact tendsto_nhds_unique h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
haveI := isCompact_iff_compactSpace.mp hs₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this : CompactSpace ↑s₁
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
haveI := isCompact_iff_compactSpace.mp hs₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
h₂ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₂ }) ∘ fun i => restrict s₂ (F i)) l
    (𝓝 (↑(f s₂ hs₂) { val := x, property := hxs₂ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
exact tendsto_nhds_unique h₁ h₂
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
have hs : ∀ x : α, ∃ (s : _), IsCompact s ∧ s ∈ 𝓝 x := by
  intro x
  obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x
  exact ⟨s, hs, hs'⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
[PROOFSTEP]
obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
s : Set α
hs : IsCompact s
hs' : s ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
[PROOFSTEP]
exact ⟨s, hs, hs'⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
refine ⟨liftCover' _ _ h hs, ?_⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ Filter.Tendsto F l
    (𝓝
      (liftCover'
        (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
        (fun s hs => f s hs) h hs))
[PROOFSTEP]
rw [tendsto_compactOpen_iff_forall]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∀ (s : Set α),
    IsCompact s →
      Filter.Tendsto (fun i => restrict s (F i)) l
        (𝓝
          (restrict s
            (liftCover'
              (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
              (fun s hs => f s hs) h hs)))
[PROOFSTEP]
intro s hs
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l
    (𝓝
      (restrict s
        (liftCover'
          (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
          (fun s hs => f s hs) h hs✝)))
[PROOFSTEP]
rw [liftCover_restrict']
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s ?m.52935))
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ s ∈ fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f
[PROOFSTEP]
exact hf s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
y : β
s : Set α
⊢ ↑(coev α β y) '' s = {y} ×ˢ s
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (s : Set C(α, β × α)), s ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} → IsOpen (coev α β ⁻¹' s)
[PROOFSTEP]
rintro _ ⟨s, sc, u, uo, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
⊢ IsOpen (coev α β ⁻¹' CompactOpen.gen s u)
[PROOFSTEP]
rw [isOpen_iff_forall_mem_open]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
⊢ ∀ (x : β), x ∈ coev α β ⁻¹' CompactOpen.gen s u → ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
intro y hy
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
have hy' : (↑(coev α β y) '' s ⊆ u) := hy
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : ↑(coev α β y) '' s ⊆ u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
rw [image_coev s] at hy'
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : {y} ×ˢ s ⊆ u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
rcases generalized_tube_lemma isCompact_singleton sc uo hy' with ⟨v, w, vo, _, yv, sw, vwu⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
refine' ⟨v, _, vo, singleton_subset_iff.mp yv⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
⊢ v ⊆ coev α β ⁻¹' CompactOpen.gen s u
[PROOFSTEP]
intro y' hy'
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy'✝ : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
y' : β
hy' : y' ∈ v
⊢ y' ∈ coev α β ⁻¹' CompactOpen.gen s u
[PROOFSTEP]
change coev α β y' '' s ⊆ u
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy'✝ : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
y' : β
hy' : y' ∈ v
⊢ ↑(coev α β y') '' s ⊆ u
[PROOFSTEP]
rw [image_coev s]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy'✝ : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
y' : β
hy' : y' ∈ v
⊢ {y'} ×ˢ s ⊆ u
[PROOFSTEP]
exact (prod_mono (singleton_subset_iff.mpr hy') sw).trans vwu
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
⊢ curry' f = comp f ∘ coev β α
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
x✝ : α
a✝ : β
⊢ ↑(curry' f x✝) a✝ = ↑((comp f ∘ coev β α) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous curry
[PROOFSTEP]
apply continuous_of_continuous_uncurry
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous (Function.uncurry fun x y => ↑(curry x) y)
[PROOFSTEP]
apply continuous_of_continuous_uncurry
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous (Function.uncurry fun x y => ↑(Function.uncurry (fun x y => ↑(curry x) y) x) y)
[PROOFSTEP]
rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous
    ((Function.uncurry fun x y => ↑(Function.uncurry (fun x y => ↑(curry x) y) x) y) ∘
      ↑(Homeomorph.symm (Homeomorph.prodAssoc C(α × β, γ) α β)))
[PROOFSTEP]
exact continuous_eval'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous uncurry
[PROOFSTEP]
apply continuous_of_continuous_uncurry
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous (Function.uncurry fun x y => ↑(uncurry x) y)
[PROOFSTEP]
rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous ((Function.uncurry fun x y => ↑(uncurry x) y) ∘ ↑(Homeomorph.prodAssoc C(α, C(β, γ)) α β))
[PROOFSTEP]
apply continuous_eval'.comp (continuous_eval'.prod_map continuous_id)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Function.LeftInverse uncurry ContinuousMap.curry
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α × β, γ)
⊢ uncurry (ContinuousMap.curry x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α × β, γ)
a✝ : α × β
⊢ ↑(uncurry (ContinuousMap.curry x✝)) a✝ = ↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Function.RightInverse uncurry ContinuousMap.curry
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α, C(β, γ))
⊢ ContinuousMap.curry (uncurry x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α, C(β, γ))
a✝¹ : α
a✝ : β
⊢ ↑(↑(ContinuousMap.curry (uncurry x✝)) a✝¹) a✝ = ↑(↑x✝ a✝¹) a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Unique α
f : C(α, β)
⊢ const α ((fun f => ↑f default) f) = f
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Unique α
f : C(α, β)
a : α
⊢ ↑(const α ((fun f => ↑f default) f)) a = ↑f a
[PROOFSTEP]
rw [Unique.eq_default a]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Unique α
f : C(α, β)
a : α
⊢ ↑(const α ((fun f => ↑f default) f)) default = ↑f default
[PROOFSTEP]
rfl
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
⊢ Continuous g
[PROOFSTEP]
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
⊢ Continuous g
[PROOFSTEP]
have h : ∀ x : X, Continuous fun y => g (x, y) := by
  intro x
  obtain ⟨x₀, rfl⟩ := hf.surjective x
  exact (Gf x₀).continuous
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
⊢ ∀ (x : X), Continuous fun y => g (x, y)
[PROOFSTEP]
intro x
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
x : X
⊢ Continuous fun y => g (x, y)
[PROOFSTEP]
obtain ⟨x₀, rfl⟩ := hf.surjective x
[GOAL]
case intro
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
x₀ : X₀
⊢ Continuous fun y => g (f x₀, y)
[PROOFSTEP]
exact (Gf x₀).continuous
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
⊢ Continuous g
[PROOFSTEP]
let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous g
[PROOFSTEP]
have : Continuous G := by
  rw [hf.continuous_iff]
  exact Gf.continuous
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous G
[PROOFSTEP]
rw [hf.continuous_iff]
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous (G ∘ f)
[PROOFSTEP]
exact Gf.continuous
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
this : Continuous G
⊢ Continuous g
[PROOFSTEP]
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
⊢ Continuous g
[PROOFSTEP]
have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) := hg.comp continuous_swap
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
this : Continuous fun p => g ((Prod.swap p).fst, f (Prod.swap p).snd)
⊢ Continuous g
[PROOFSTEP]
have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
[GOAL]
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
this✝ : Continuous fun p => g ((Prod.swap p).fst, f (Prod.swap p).snd)
this : Continuous fun p => (g ∘ Prod.swap) (f p.fst, p.snd)
⊢ Continuous g
[PROOFSTEP]
exact (hf.continuous_lift_prod_left this).comp continuous_swap


[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (Setoid.Rel toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (Setoid.Rel toSetoid✝ x))
x✝ :
  { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ }.toSetoid =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }.toSetoid
⊢ { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
⊢ IsOpen (setOf (Setoid.Rel { r := fun x y => x ∈ A ↔ y ∈ A, iseqv := (_ : Equivalence fun x y => x ∈ A ↔ y ∈ A) } x))
[PROOFSTEP]
by_cases hx : x ∈ A
[GOAL]
case pos
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
hx : x ∈ A
⊢ IsOpen (setOf (Setoid.Rel { r := fun x y => x ∈ A ↔ y ∈ A, iseqv := (_ : Equivalence fun x y => x ∈ A ↔ y ∈ A) } x))
[PROOFSTEP]
simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
[GOAL]
case neg
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
hx : ¬x ∈ A
⊢ IsOpen (setOf (Setoid.Rel { r := fun x y => x ∈ A ↔ y ∈ A, iseqv := (_ : Equivalence fun x y => x ∈ A ↔ y ∈ A) } x))
[PROOFSTEP]
simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen {proj S x}
[PROOFSTEP]
rw [← S.proj_quotientMap.isOpen_preimage, fiber_eq]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsOpen (setOf (Setoid.Rel S.toSetoid x))
[PROOFSTEP]
exact S.isOpen_setOf_rel _
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (setOf (Setoid.Rel S.toSetoid x))
[PROOFSTEP]
rw [← fiber_eq]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (proj S ⁻¹' {proj S x})
[PROOFSTEP]
apply isClopen_preimage
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S a : DiscreteQuotient X
⊢ a ≤ ⊤
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
⊢ ∀ (a b : Quotient ⊤.toSetoid), a = b
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
a✝² : Quotient ⊤.toSetoid
a✝¹ : X
b✝ : Quotient ⊤.toSetoid
a✝ : X
⊢ Quot.mk Setoid.r a✝¹ = Quot.mk Setoid.r a✝
[PROOFSTEP]
exact Quotient.sound trivial
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
g : C(Y, Z)
f : C(X, Y)
A B : DiscreteQuotient Y
h : A ≤ B
⊢ comap f A ≤ comap f B
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
⊢ ofLE (_ : A ≤ A) = id
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ ofLE (_ : A ≤ A) (Quot.mk Setoid.r a✝) = id (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
a : Quotient A.toSetoid
⊢ ofLE (_ : A ≤ A) a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE (_ : A ≤ C) x
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk Setoid.r a✝)) = ofLE (_ : A ≤ C) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x : X
⊢ IsOpen (setOf (Setoid.Rel (connectedComponentSetoid X) x))
[PROOFSTEP]
convert isOpen_connectedComponent (x := x)
[GOAL]
case h.e'_3
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x : X
⊢ setOf (Setoid.Rel (connectedComponentSetoid X) x) = connectedComponent x
[PROOFSTEP]
ext y
[GOAL]
case h.e'_3.h
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : LocallyConnectedSpace X
x y : X
⊢ y ∈ setOf (Setoid.Rel (connectedComponentSetoid X) x) ↔ y ∈ connectedComponent x
[PROOFSTEP]
simpa only [connectedComponentSetoid, ← connectedComponent_eq_iff_mem] using eq_comm
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : DiscreteTopology X
x y : X
⊢ proj ⊥ x = proj ⊥ y ↔ x = y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ LEComap g B C → LEComap f A B → LEComap (ContinuousMap.comp g f) A C
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) = id
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) (Quot.mk Setoid.r a✝) = id (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) = map g h1 ∘ map f h2
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) (Quot.mk Setoid.r a✝) =
    (map g h1 ∘ map f h2) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f (_ : LEComap f A B') a
[PROOFSTEP]
rcases a with ⟨⟩
[GOAL]
case mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A B') (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
⊢ map f cond (ofLE h c) = map f (_ : LEComap f A' B) c
[PROOFSTEP]
rcases c with ⟨⟩
[GOAL]
case mk
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A' B) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
S : DiscreteQuotient X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), proj Q x = proj Q y
⊢ x = y
[PROOFSTEP]
rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_clopen, mem_iInter]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
S : DiscreteQuotient X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), proj Q x = proj Q y
⊢ ∀ (i : { Z // IsClopen Z ∧ y ∈ Z }), x ∈ ↑i
[PROOFSTEP]
rintro ⟨U, hU1, hU2⟩
[GOAL]
case mk.intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
S : DiscreteQuotient X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), proj Q x = proj Q y
U : Set X
hU1 : IsClopen U
hU2 : y ∈ U
⊢ x ∈ ↑{ val := U, property := (_ : IsClopen U ∧ y ∈ U) }
[PROOFSTEP]
exact (Quotient.exact' (h (ofClopen hU1))).mpr hU2
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : Quotient A.toSetoid
⊢ proj A ⁻¹' {a} ⊆ proj B ⁻¹' {ofLE h a}
[PROOFSTEP]
rcases A.proj_surjective a with ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ proj A ⁻¹' {proj A a} ⊆ proj B ⁻¹' {ofLE h (proj A a)}
[PROOFSTEP]
rw [fiber_eq, ofLE_proj, fiber_eq]
[GOAL]
case intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B : DiscreteQuotient X
h : A ≤ B
a : X
⊢ setOf (Setoid.Rel A.toSetoid a) ⊆ setOf (Setoid.Rel B.toSetoid a)
[PROOFSTEP]
exact fun _ h' => h h'
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
[PROOFSTEP]
have H₁ : ∀ Q₁ Q₂, Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂} := fun _ _ h =>
  by
  rw [← compat _ _ h]
  exact fiber_subset_ofLE _ _
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {Qs x✝}
[PROOFSTEP]
rw [← compat _ _ h]
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ proj x✝¹ ⁻¹' {Qs x✝¹} ⊆ proj x✝ ⁻¹' {ofLE h (Qs x✝¹)}
[PROOFSTEP]
exact fiber_subset_ofLE _ _
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
[PROOFSTEP]
obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _})
    (directed_of_inf H₁) (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
    (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _
[GOAL]
case intro
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → proj Q₁ ⁻¹' {Qs Q₁} ⊆ proj Q₂ ⁻¹' {Qs Q₂}
x : X
hx : x ∈ ⋂ (Q : DiscreteQuotient X), proj Q ⁻¹' {Qs Q}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), proj Q x = Qs Q
[PROOFSTEP]
exact ⟨x, mem_iInter.1 hx⟩
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
⊢ Finite (Quotient S.toSetoid)
[PROOFSTEP]
have : CompactSpace S := Quotient.compactSpace
[GOAL]
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : CompactSpace X
this : CompactSpace (Quotient S.toSetoid)
⊢ Finite (Quotient S.toSetoid)
[PROOFSTEP]
rwa [← isCompact_univ_iff, isCompact_iff_finite, finite_univ_iff] at this


[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(TensorAlgebra.ι R) m ∈ LinearMap.range (TensorAlgebra.ι R) ^ 1
[PROOFSTEP]
simpa only [pow_one] using LinearMap.mem_range_self _ m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(TensorAlgebra.ι R) m ∈ LinearMap.range (TensorAlgebra.ι R) ^ 1
[PROOFSTEP]
simpa only [pow_one] using LinearMap.mem_range_self _ m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ AlgHom.comp (DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (↑(lift R) (GradedAlgebra.ι R M)) =
    AlgHom.id R (TensorAlgebra R M)
[PROOFSTEP]
ext m
[GOAL]
case w.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp (DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (↑(lift R) (GradedAlgebra.ι R M))))
          (ι R))
      m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M))) (ι R)) m
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply]
[GOAL]
case w.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (↑(↑(lift R) (GradedAlgebra.ι R M)) (↑(ι R) m)) = ↑(ι R) m
[PROOFSTEP]
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : { x // x ∈ LinearMap.range (ι R) ^ i }
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) ↑{ val := x, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
  -- porting note: use new `induction using` support that failed in Lean 3
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd x y i hx hy ihx ihy => rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
| hmul m hm i x hx ih =>
  obtain ⟨_, rfl⟩ := hm
  rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd x y i hx hy ihx ihy => rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
| hmul m hm i x hx ih =>
  obtain ⟨_, rfl⟩ := hm
  rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
case mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
r : R
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (↑(algebraMap R (TensorAlgebra R M)) r) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (TensorAlgebra R M)) r, property := (_ : ↑(algebraMap R (TensorAlgebra R M)) r ∈ 1) }
[PROOFSTEP]

| hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
[GOAL]
case mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
r : R
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (↑(algebraMap R (TensorAlgebra R M)) r) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (TensorAlgebra R M)) r, property := (_ : ↑(algebraMap R (TensorAlgebra R M)) r ∈ 1) }
[PROOFSTEP]
rw [AlgHom.commutes, DirectSum.algebraMap_apply]
[GOAL]
case mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
x : TensorAlgebra R M
r : R
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0) (↑DirectSum.GAlgebra.toFun r) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (TensorAlgebra R M)) r, property := (_ : ↑(algebraMap R (TensorAlgebra R M)) r ∈ 1) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ LinearMap.range (ι R) ^ i
hy : y ∈ LinearMap.range (ι R) ^ i
ihx :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
ihy :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) y =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := y, property := hy }
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (x + y) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i)
      { val := x + y, property := (_ : x + y ∈ LinearMap.range (ι R) ^ i) }
[PROOFSTEP]

| hadd x y i hx hy ihx ihy => rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ LinearMap.range (ι R) ^ i
hy : y ∈ LinearMap.range (ι R) ^ i
ihx :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
ihy :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) y =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := y, property := hy }
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (x + y) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i)
      { val := x + y, property := (_ : x + y ∈ LinearMap.range (ι R) ^ i) }
[PROOFSTEP]
rw [AlgHom.map_add, ihx, ihy, ← map_add]
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ LinearMap.range (ι R) ^ i
hy : y ∈ LinearMap.range (ι R) ^ i
ihx :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
ihy :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) y =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := y, property := hy }
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i)
      ({ val := x, property := hx } + { val := y, property := hy }) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i)
      { val := x + y, property := (_ : x + y ∈ LinearMap.range (ι R) ^ i) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hmul
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ m : TensorAlgebra R M
hm : m ∈ LinearMap.range (ι R)
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
ih :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (m * x) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i))
      { val := m * x, property := (_ : m * x ∈ LinearMap.range (ι R) * npowRec i (LinearMap.range (ι R))) }
[PROOFSTEP]

| hmul m hm i x hx ih =>
  obtain ⟨_, rfl⟩ := hm
  rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
case mk.hmul
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ m : TensorAlgebra R M
hm : m ∈ LinearMap.range (ι R)
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
ih :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (m * x) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i))
      { val := m * x, property := (_ : m * x ∈ LinearMap.range (ι R) * npowRec i (LinearMap.range (ι R))) }
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hm
[GOAL]
case mk.hmul.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ : TensorAlgebra R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
ih :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
w✝ : M
⊢ ↑(↑(lift R) (GradedAlgebra.ι R M)) (↑(ι R) w✝ * x) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i))
      { val := ↑(ι R) w✝ * x,
        property := (_ : ↑(ι R) w✝ * x ∈ LinearMap.range (ι R) * npowRec i (LinearMap.range (ι R))) }
[PROOFSTEP]
rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
[GOAL]
case mk.hmul.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ : TensorAlgebra R M
i : ℕ
x : TensorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
ih :
  ↑(↑(lift R) (GradedAlgebra.ι R M)) x =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
w✝ : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (1 + i))
      (GradedMonoid.GMul.mul { val := ↑(ι R) w✝, property := (_ : ↑(ι R) w✝ ∈ LinearMap.range (ι R) ^ 1) }
        { val := x, property := hx }) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i))
      { val := ↑(ι R) w✝ * x,
        property := (_ : ↑(ι R) w✝ * x ∈ LinearMap.range (ι R) * npowRec i (LinearMap.range (ι R))) }
[PROOFSTEP]
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)