[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
⊢ IsProperMap ↑e
[PROOFSTEP]
rw [isProperMap_iff_clusterPt]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
⊢ Continuous ↑e ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ ↑e → ∃ x, ↑e x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
refine ⟨e.continuous, fun ℱ y ↦ ?_⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
ℱ : Filter X
y : Y
⊢ MapClusterPt y ℱ ↑e → ∃ x, ↑e x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, e.comap_nhds_eq, ← e.coe_toEquiv, ←
  e.eq_symm_apply, exists_eq_left]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.666
W : Type ?u.669
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
e : X ≃ₜ Y
ℱ : Filter X
y : Y
⊢ NeBot (𝓝 (↑(Homeomorph.symm e) y) ⊓ ℱ) → NeBot (𝓝 (↑e.symm y) ⊓ ℱ)
[PROOFSTEP]
exact id
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.2964
W : Type ?u.2967
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
⊢ IsClosedMap f
[PROOFSTEP]
rw [isClosedMap_iff_clusterPt]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.2964
W : Type ?u.2967
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
[PROOFSTEP]
exact fun s y ↦ h.clusterPt_of_mapClusterPt (ℱ := 𝓟 s) (y := y)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rw [isProperMap_iff_clusterPt]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine and_congr_right (fun _ ↦ ?_)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) →
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
⊢ (∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x) →
    ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
intro H
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
⊢ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro 𝒰 y (hY : (Ultrafilter.map f 𝒰 : Filter Y) ≤ _)
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
simp_rw [← Ultrafilter.clusterPt_iff] at hY ⊢
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ClusterPt y ↑(Ultrafilter.map f 𝒰)
⊢ ∃ x, f x = y ∧ ClusterPt x ↑𝒰
[PROOFSTEP]
exact H hY
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, ← exists_ultrafilter_iff, forall_exists_index]
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄ (x : Ultrafilter X), ↑x ≤ comap f (𝓝 y) ⊓ ℱ → ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
[PROOFSTEP]
intro ℱ y 𝒰 hy
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ
⊢ ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
[PROOFSTEP]
rcases H (tendsto_iff_comap.mpr <| hy.trans inf_le_left) with ⟨x, hxy, hx⟩
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.3327
W : Type ?u.3330
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
x✝ : Continuous f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : ↑𝒰 ≤ comap f (𝓝 y) ⊓ ℱ
x : X
hxy : f x = y
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, f x = y ∧ ∃ u, ↑u ≤ 𝓝 x ⊓ ℱ
[PROOFSTEP]
exact ⟨x, hxy, 𝒰, le_inf hx (hy.trans inf_le_right)⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsProperMap f
hg : IsProperMap g
⊢ IsProperMap (Prod.map f g)
[PROOFSTEP]
simp_rw [isProperMap_iff_ultrafilter] at hf hg ⊢
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous (Prod.map f g) ∧
    ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄, Tendsto (Prod.map f g) (↑𝒰) (𝓝 y) → ∃ x, Prod.map f g x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
constructor
  -- Continuity is clear.
[GOAL]
case left
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous (Prod.map f g)
[PROOFSTEP]
exact
  hf.1.prod_map
    hg.1
      -- Let `𝒰 : Ultrafilter (X × Z)`, and assume that `f × g` tends to some `(y, w) : Y × W`
        -- along `𝒰`.
[GOAL]
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄, Tendsto (Prod.map f g) (↑𝒰) (𝓝 y) → ∃ x, Prod.map f g x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro 𝒰 ⟨y, w⟩ hyw
[GOAL]
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (Prod.map f g) (↑𝒰) (𝓝 (y, w))
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
simp_rw [nhds_prod_eq, tendsto_prod_iff'] at hyw
[GOAL]
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases hf.2 (show Tendsto f (Ultrafilter.map fst 𝒰) (𝓝 y) by simpa using hyw.1) with ⟨x, hxy, hx⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
⊢ Tendsto f (↑(Ultrafilter.map fst 𝒰)) (𝓝 y)
[PROOFSTEP]
simpa using hyw.1
[GOAL]
case right.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using hyw.2) with
  ⟨z, hzw, hz⟩
    -- By the properties of the product topology, that means that `𝒰` tends to `(x, z)`,
      -- which completes the proof since `(f × g)(x, z) = (y, w)`.
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
⊢ Tendsto g (↑(Ultrafilter.map snd 𝒰)) (𝓝 w)
[PROOFSTEP]
simpa using hyw.2
[GOAL]
case right.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩
[GOAL]
case right.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ↑𝒰 ≤ 𝓝 (x, z)
[PROOFSTEP]
rw [nhds_prod_eq, le_prod]
[GOAL]
case right.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n => (Prod.map f g n).fst) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n => (Prod.map f g n).snd) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ Tendsto fst (↑𝒰) (𝓝 x) ∧ Tendsto snd (↑𝒰) (𝓝 z)
[PROOFSTEP]
exact ⟨hx, hz⟩
[GOAL]
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h : ∀ (i : ι), IsProperMap (f i)
⊢ IsProperMap fun x i => f i (x i)
[PROOFSTEP]
simp_rw [isProperMap_iff_ultrafilter] at h ⊢
[GOAL]
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ (Continuous fun x i => f i (x i)) ∧
    ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
      Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
constructor
  -- Continuity is clear.
[GOAL]
case left
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous fun x i => f i (x i)
[PROOFSTEP]
exact
  continuous_pi fun i ↦
    (h i).1.comp
      (continuous_apply i)
        -- Let `𝒰 : Ultrafilter (Π i, X i)`, and assume that `Π i, f i` tends to some `y : Π i, Y i`
          -- along `𝒰`.
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
intro 𝒰 y hy
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by simpa [tendsto_pi_nhds] using hy
[GOAL]
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
⊢ ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
[PROOFSTEP]
simpa [tendsto_pi_nhds] using hy
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
choose x hxy hx using fun i ↦
  (h i).2
    (this i)
      -- By the properties of the product topology, that means that `𝒰` tends to `x`,
        -- which completes the proof since `(Π i, f i) x = y`.
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨x, funext hxy, ?_⟩
[GOAL]
case right
X✝ : Type ?u.30436
Y✝ : Type ?u.30439
Z : Type ?u.30442
W : Type ?u.30445
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
ι : Type u_3
X : ι → Type u_1
Y : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval i) 𝒰)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), ↑(Ultrafilter.map (eval i) 𝒰) ≤ 𝓝 (x i)
⊢ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rwa [nhds_pi, le_pi]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
[PROOFSTEP]
rw [isCompact_iff_ultrafilter_le_nhds]
  -- Let `𝒰 ≤ 𝓟 (f ⁻¹' K)` an ultrafilter.
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ ∀ (f_1 : Ultrafilter X), ↑f_1 ≤ 𝓟 (f ⁻¹' K) → ∃ a, a ∈ f ⁻¹' K ∧ ↑f_1 ≤ 𝓝 a
[PROOFSTEP]
intro 𝒰 h𝒰
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] at h𝒰
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
rcases hK.ultrafilter_le_nhds _ h𝒰 with
  ⟨y, hyK, hy⟩
    -- Then, by properness of `f`, that means that `𝒰` tends to some `x ∈ f ⁻¹' {y} ⊆ f ⁻¹' K`,
      -- which completes the proof.
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
y : Y
hyK : y ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36187
W : Type ?u.36190
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
x : X
hx : ↑𝒰 ≤ 𝓝 x
hyK : f x ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 (f x)
⊢ ∃ a, a ∈ f ⁻¹' K ∧ ↑𝒰 ≤ 𝓝 a
[PROOFSTEP]
exact ⟨x, hyK, hx⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
⊢ (Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
[PROOFSTEP]
exact ⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_singleton⟩
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_clusterPt]
  -- Let `ℱ : Filter X` and `y` some cluster point of `map f ℱ`.
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
refine
  ⟨H.1, fun ℱ y hy ↦ ?_⟩
    -- That means that the singleton `pure y` meets the "closure" of `map f ℱ`, by which we mean
      -- `Filter.lift' (map f ℱ) closure`. But `f` is closed, so
      -- `closure (map f ℱ) = map f (closure ℱ)` (see `IsClosedMap.lift'_closure_map_eq`).
      -- Thus `map f (closure ℱ ⊓ 𝓟 (f ⁻¹' {y})) = map f (closure ℱ) ⊓ 𝓟 {y} ≠ ⊥`, hence
      -- `closure ℱ ⊓ 𝓟 (f ⁻¹' {y}) ≠ ⊥`.
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' { y })) inf_le_right with ⟨x, hxy, hx⟩
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
[PROOFSTEP]
refine
  ⟨x, hxy, ?_⟩
    -- In particular `x` is a cluster point of `closure ℱ`. Since cluster points of `closure ℱ`
      -- are exactly cluster points of `ℱ` (see `clusterPt_lift'_closure_iff`), this completes
      -- the proof.
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x ℱ
[PROOFSTEP]
rw [← clusterPt_lift'_closure_iff]
[GOAL]
case mpr.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.36806
W : Type ?u.36809
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : NeBot (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (Filter.lift' ℱ closure)
[PROOFSTEP]
exact hx.mono inf_le_left
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite
[PROOFSTEP]
simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto, le_cofinite_iff_compl_singleton_mem, mem_map,
  preimage_compl]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
[PROOFSTEP]
refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦ ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})
[PROOFSTEP]
rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩
[GOAL]
case intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.37764
W : Type ?u.37767
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace W
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})
[PROOFSTEP]
exact isCompact_of_isClosed_subset hK (isClosed_singleton.preimage f_cont) (compl_le_compl_iff_le.mp hKy)
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ IsProperMap f → Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
[PROOFSTEP]
exact ⟨H.continuous, fun K hK ↦ H.isCompact_preimage hK⟩
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_ultrafilter]
  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine
  ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
    -- Pick `K` some compact neighborhood of `y`, which exists by local compactness.
[GOAL]
case mpr
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases exists_compact_mem_nhds y with
  ⟨K, hK, hKy⟩
    -- Then `map f 𝒰 ≤ 𝓝 y ≤ 𝓟 K`, hence `𝒰 ≤ 𝓟 (f ⁻¹' K)`
[GOAL]
case mpr.intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : 𝒰 ≤ 𝓟 (f ⁻¹' K) := by
  simpa only [← comap_principal, ← tendsto_iff_comap] using
    hy.mono_right
      (le_principal_iff.mpr hKy)
        -- By compactness of `f ⁻¹' K`, `𝒰` converges to some `x ∈ f ⁻¹' K`.
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
⊢ ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
[PROOFSTEP]
simpa only [← comap_principal, ← tendsto_iff_comap] using
  hy.mono_right
    (le_principal_iff.mpr hKy)
      -- By compactness of `f ⁻¹' K`, `𝒰` converges to some `x ∈ f ⁻¹' K`.
[GOAL]
case mpr.intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
this : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases(H.2 hK).ultrafilter_le_nhds _ this with
  ⟨x, -, hx⟩
    -- Finally, `f` tends to `f x` along `𝒰` by continuity, thus `f x = y`.
[GOAL]
case mpr.intro.intro.intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.39226
W : Type ?u.39229
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
H : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
K : Set Y
hK : IsCompact K
hKy : K ∈ 𝓝 y
this : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
x : X
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨x, tendsto_nhds_unique ((H.1.tendsto _).comp hx) hy, hx⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)
[PROOFSTEP]
simp_rw [isProperMap_iff_isCompact_preimage, hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set,
  preimage_compl]
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
[PROOFSTEP]
refine and_congr_right fun f_cont ↦ ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩
[GOAL]
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
[PROOFSTEP]
rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩
[GOAL]
case intro.intro
X : Type u_2
Y : Type u_1
Z : Type ?u.49990
W : Type ?u.49993
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f : X → Y
inst✝¹ : T2Space Y
inst✝ : LocallyCompactSpace Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ
⊢ IsCompact (f ⁻¹' K)
[PROOFSTEP]
exact isCompact_of_isClosed_subset hK' (hK.isClosed.preimage f_cont) (compl_le_compl_iff_le.mp hK'y)
[GOAL]
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.continuous, H.universally_closed _⟩
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_ultrafilter]
  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine
  ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
    -- In `X × Filter X`, consider the closed set `F := closure {(x, ℱ) | ℱ = pure x}`
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
let F : Set (X × Filter X) :=
  closure
    {xℱ | xℱ.2 = pure xℱ.1}
      -- Since `f × id` is closed, the set `(f × id) '' F` is also closed.
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have := H.2 F isClosed_closure
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
  -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
    -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
    -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
    -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
    -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.this.mem_of_tendsto
    (hy.prod_mk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
    (eventually_of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
      -- The above shows that `(y, 𝒰) = (f x, 𝒰)`, for some `x : X` such that `(x, 𝒰) ∈ F`.
[GOAL]
case mpr
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, ↑𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases this with
  ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
    -- We already know that `f x = y`, so to finish the proof we just have to check that `𝒰` tends
      -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is a ultrafilter,
      -- it is enough to show that `Uᶜ` is not in `𝒰`.
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : (x, 𝒰.1) ∈ F
⊢ ∃ x_1, f x_1 = f x ∧ ↑𝒰 ≤ 𝓝 x_1
[PROOFSTEP]
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_not_mem_iff.mp fun hUc ↦ ?_⟩
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : (x, 𝒰.1) ∈ F
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ 𝒰
⊢ False
[PROOFSTEP]
rw [mem_closure_iff_nhds] at hx
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : ∀ (t : Set (X × Filter X)), t ∈ 𝓝 (x, 𝒰.1) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ 𝒰
⊢ False
[PROOFSTEP]
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOf_mem.mem_nhds hUc)) with
  ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩
[GOAL]
case mpr.intro.mk.intro.refl.intro.mk.intro.intro
X✝ : Type ?u.52247
Y✝ : Type ?u.52250
Z : Type ?u.52253
W : Type ?u.52256
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰) (𝓝 (f x))
hx : ∀ (t : Set (X × Filter X)), t ∈ 𝓝 (x, 𝒰.1) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ 𝒰
z : X
hz : z ∈ U
hz' : Uᶜ ∈ pure z
⊢ False
[PROOFSTEP]
exact hz' hz
[GOAL]
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.continuous, H.universally_closed _⟩
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_ultrafilter]
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
let F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have := H.2 F isClosed_closure
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
have : (y, 𝒰) ∈ Prod.map f id '' F :=
  this.mem_of_tendsto (hy.prod_mk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
    (eventually_of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
[GOAL]
case mpr
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (𝓝 y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
[PROOFSTEP]
rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (𝓝 (f x))
⊢ ∃ x_1, f x_1 = f x ∧ ↑(id snd✝) ≤ 𝓝 x_1
[PROOFSTEP]
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_not_mem_iff.mp fun hUc ↦ ?_⟩
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (𝓝 (f x))
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ id snd✝
⊢ False
[PROOFSTEP]
rw [mem_closure_iff_nhds] at hx
[GOAL]
case mpr.intro.mk.intro.refl
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ (t : Set (X × Ultrafilter X)), t ∈ 𝓝 (x, snd✝) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
hy : Tendsto f (↑(id snd✝)) (𝓝 (f x))
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ id snd✝
⊢ False
[PROOFSTEP]
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc)) with
  ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩
[GOAL]
case mpr.intro.mk.intro.refl.intro.mk.intro.intro
X✝ : Type ?u.54240
Y✝ : Type ?u.54243
Z : Type ?u.54246
W : Type ?u.54249
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.snd = pure xℱ.fst}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ (t : Set (X × Ultrafilter X)), t ∈ 𝓝 (x, snd✝) → Set.Nonempty (t ∩ {xℱ | xℱ.snd = pure xℱ.fst})
hy✝ : Tendsto f (↑(id snd✝)) (𝓝 (f x))
U : Set X
hU : U ∈ 𝓝 x
hUc : Uᶜ ∈ id snd✝
y : X
hy : y ∈ U
hy' : Uᶜ ∈ pure y
⊢ False
[PROOFSTEP]
exact hy' hy
[GOAL]
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
[PROOFSTEP]
intro H
[GOAL]
case mpr
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)) → IsProperMap f
[PROOFSTEP]
intro H
[GOAL]
case mp
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.continuous, fun Z ↦ H.universally_closed _⟩
[GOAL]
case mpr
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ IsProperMap f
[PROOFSTEP]
rw [isProperMap_iff_isClosedMap_ultrafilter]
[GOAL]
case mpr
X✝ : Type ?u.56079
Y✝ : Type ?u.56082
Z : Type ?u.56085
W : Type ?u.56088
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
f✝ : X✝ → Y✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
[PROOFSTEP]
exact ⟨H.1, H.2 _⟩


[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ det (adjugate ↑A) = 1
[PROOFSTEP]
rw [det_adjugate, A.prop, one_pow]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : SpecialLinearGroup n R
⊢ det (↑A * ↑B) = 1
[PROOFSTEP]
rw [det_mul, A.prop, B.prop, one_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
A B : SpecialLinearGroup n R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ det ↑g ≠ 0
[PROOFSTEP]
rw [g.det_coe]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
A B : SpecialLinearGroup n R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
A B : SpecialLinearGroup n R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
i : n
h : ↑g i = 0
⊢ ∀ (j : n), ↑g i j = 0
[PROOFSTEP]
simp [h]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
src✝¹ : Monoid (SpecialLinearGroup n R) := monoid
src✝ : Inv (SpecialLinearGroup n R) := hasInv
A : SpecialLinearGroup n R
⊢ A⁻¹ * A = 1
[PROOFSTEP]
ext1
[GOAL]
case a
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
src✝¹ : Monoid (SpecialLinearGroup n R) := monoid
src✝ : Inv (SpecialLinearGroup n R) := hasInv
A : SpecialLinearGroup n R
i✝ j✝ : n
⊢ ↑(A⁻¹ * A) i✝ j✝ = ↑1 i✝ j✝
[PROOFSTEP]
simp [adjugate_mul]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ comp (↑Matrix.toLin' ↑A) (↑Matrix.toLin' ↑A⁻¹) = LinearMap.id
[PROOFSTEP]
rw [← toLin'_mul, ← coe_mul, mul_right_inv, coe_one, toLin'_one]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ comp (↑Matrix.toLin' ↑A⁻¹) (↑Matrix.toLin' ↑A) = LinearMap.id
[PROOFSTEP]
rw [← toLin'_mul, ← coe_mul, mul_left_inv, coe_one, toLin'_one]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : SpecialLinearGroup n R
⊢ det (↑(RingHom.mapMatrix f) ↑g) = 1
[PROOFSTEP]
rw [← f.map_det]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : SpecialLinearGroup n R
⊢ ↑f (det ↑g) = 1
[PROOFSTEP]
simp [g.prop]
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ det (-↑g) = 1
[PROOFSTEP]
simpa [(@Fact.out <| Even <| Fintype.card n).neg_one_pow, g.det_coe] using det_smul (↑ₘg) (-1)
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1
[PROOFSTEP]
rw [Matrix.det_fin_two, mul_comm]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 0 -
      vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 0 =
    1
[PROOFSTEP]
simp only [cons_val_zero, cons_val_one, head_cons, mul_neg, neg_mul, neg_neg]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
[PROOFSTEP]
have := A.2
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
this : det ↑A = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
[PROOFSTEP]
rw [Matrix.det_fin_two] at this
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
[PROOFSTEP]
convert this
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ A⁻¹ =
    { val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
      property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
[PROOFSTEP]
ext
[GOAL]
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
i✝ j✝ : Fin 2
⊢ ↑A⁻¹ i✝ j✝ =
    ↑{ val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
          property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
      i✝ j✝
[PROOFSTEP]
have := Matrix.adjugate_fin_two A.1
[GOAL]
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
i✝ j✝ : Fin 2
this : adjugate ↑A = ↑of ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]]
⊢ ↑A⁻¹ i✝ j✝ =
    ↑{ val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
          property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
      i✝ j✝
[PROOFSTEP]
rw [coe_inv, this]
[GOAL]
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
i✝ j✝ : Fin 2
this : adjugate ↑A = ↑of ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]]
⊢ ↑of ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] i✝ j✝ =
    ↑{ val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
          property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
      i✝ j✝
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
a b c d : R
hdet : a * d - b * c = 1
⊢ det (↑of ![![a, b], ![c, d]]) = 1
[PROOFSTEP]
rwa [det_fin_two_of]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
g : SL(2, R)
⊢ P g
[PROOFSTEP]
obtain ⟨m, hm⟩ := g
[GOAL]
case mk
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ P { val := m, property := hm }
[PROOFSTEP]
convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm )
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1
[PROOFSTEP]
rwa [det_fin_two] at hm
[GOAL]
case h.e'_1.h.e'_3
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]]
[PROOFSTEP]
ext i j
[GOAL]
case h.e'_1.h.e'_3.a.h
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
i j : Fin 2
⊢ m i j = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e'_1.h.e'_3.a.h.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
j : Fin 2
⊢ m { val := 0, isLt := (_ : 0 < 2) } j = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.e'_1.h.e'_3.a.h.tail.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
j : Fin 2
⊢ m { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.e'_1.h.e'_3.a.h.head.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_3.a.h.head.tail.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_3.a.h.tail.head.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_3.a.h.tail.head.tail.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
a b : R
h : a ≠ 0
⊢ det (↑of ![![a, b], ![0, a⁻¹]]) = 1
[PROOFSTEP]
simp [h]
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
⊢ ∃ a b h, g = { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
[PROOFSTEP]
induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h_det
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : ↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 = 0
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
[PROOFSTEP]
replace hg : c = 0 := by simpa using hg
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : ↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 = 0
⊢ c = 0
[PROOFSTEP]
simpa using hg
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
[PROOFSTEP]
have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ a * d = 1
[PROOFSTEP]
rwa [hg, mul_zero, sub_zero] at h_det
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
[PROOFSTEP]
refine' ⟨a, b, left_ne_zero_of_mul_eq_one had, _⟩
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
    { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
[PROOFSTEP]
simp_rw [eq_inv_of_mul_eq_one_right had, hg]
[GOAL]
⊢ det (↑of ![![0, -1], ![1, 0]]) = 1
[PROOFSTEP]
norm_num [Matrix.det_fin_two_of]
[GOAL]
⊢ det (↑of ![![1, 1], ![0, 1]]) = 1
[PROOFSTEP]
norm_num [Matrix.det_fin_two_of]
[GOAL]
⊢ ↑T⁻¹ = ↑of ![![1, -1], ![0, 1]]
[PROOFSTEP]
simp [coe_inv, coe_T, adjugate_fin_two]
[GOAL]
n : ℤ
⊢ ↑(T ^ n) = ↑of ![![1, n], ![0, 1]]
[PROOFSTEP]
induction' n using Int.induction_on with n h n h
[GOAL]
case hz
⊢ ↑(T ^ 0) = ↑of ![![1, 0], ![0, 1]]
[PROOFSTEP]
rw [zpow_zero, coe_one, Matrix.one_fin_two]
[GOAL]
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑(T ^ (↑n + 1)) = ↑of ![![1, ↑n + 1], ![0, 1]]
[PROOFSTEP]
simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
  -- Porting note: was congrm !![_, _; _, _]
[GOAL]
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1], ![0 * 1 + 1 * 0, 0 * 1 + 1 * 1]] = ↑of ![![1, ↑n + 1], ![0, 1]]
[PROOFSTEP]
ring_nf
[GOAL]
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑(T ^ (-↑n - 1)) = ↑of ![![1, -↑n - 1], ![0, 1]]
[PROOFSTEP]
simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
  -- Porting note: was congrm !![_, _; _, _]
[GOAL]
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + -↑n * 0, 1 * -1 + -↑n * 1], ![0 * 1 + 1 * 0, 0 * -1 + 1 * 1]] = ↑of ![![1, -↑n - 1], ![0, 1]]
[PROOFSTEP]
ring_nf
[GOAL]
n : ℤ
g : SL(2, ℤ)
⊢ ↑(T ^ n * g) 1 = ↑g 1
[PROOFSTEP]
ext j
[GOAL]
case h
n : ℤ
g : SL(2, ℤ)
j : Fin 2
⊢ ↑(T ^ n * g) 1 j = ↑g 1 j
[PROOFSTEP]
simp [coe_T_zpow, Matrix.vecMul, Matrix.dotProduct, Fin.sum_univ_succ, vecTail]
[GOAL]
g : SL(2, ℤ)
⊢ ↑(T * g) 1 = ↑g 1
[PROOFSTEP]
simpa using T_pow_mul_apply_one 1 g
[GOAL]
g : SL(2, ℤ)
⊢ ↑(T⁻¹ * g) 1 = ↑g 1
[PROOFSTEP]
simpa using T_pow_mul_apply_one (-1) g