Update Lemmas.lean

Author: CoolRmal

Mathlib/Topology/Baire/Lemmas.lean

@@ -53,19 +53,12 @@ theorem IsGδ.baireSpace_of_dense {s : Set X} (hG : IsGδ s) (hd : Dense s) : Ba
   constructor
   intro f hof hdf
   obtain ⟨V, hV⟩ : ∃ V : ℕ → Set X, (∀ n, IsOpen (V n)) ∧ s = ⋂ n, V n := eq_iInter_nat hG
-  obtain ⟨g, hg1, hg2, hg3⟩ : ∃ g : ℕ → Set X, (∀ n, IsOpen (g n)) ∧ (∀ n, Dense (g n)) ∧
-    ∀ n, f n = Subtype.val ⁻¹' g n := by
-    choose g hg1 hg2 hg3 using fun n => exists_open_dense_of_open_dense_subtype hd (hof n) (hdf n)
-    exact ⟨g, hg1, hg2, fun n => (hg3 n).symm⟩
-  have h_inter_dense : Dense (⋂ n, g n ∩ V n) :=
-    BaireSpace.baire_property (fun n ↦ g n ∩ V n) (fun n => (hg1 n).inter (hV.1 n))
-      (fun n => (hg2 n).inter_of_isOpen_left (hd.mono (by simp [hV.2, iInter_subset]))
-      (hg1 n))
-  have h_inter_eq : ⋂ n, g n ∩ V n = ⋂ n, f n := by
-    ext
-    simpa [hg3, hV] using ⟨fun h => ⟨fun i => (h i).1, fun i => (h i).2⟩, fun h n => ⟨h.1 n, h.2 n⟩⟩
-  rw [h_inter_eq] at h_inter_dense
-  exact Subtype.dense_iff.mpr fun a _ ↦ h_inter_dense a
+  choose g hg1 hg2 hg3 using fun n => exists_open_dense_of_open_dense_subtype hd (hof n) (hdf n)
+  have h_inter_dense : Dense (⋂ n, g n ∩ V n) := BaireSpace.baire_property (fun n ↦ g n ∩ V n)
+    (fun n => (hg1 n).inter (hV.1 n)) (fun n => (hg2 n).inter_of_isOpen_left
+    (hd.mono (by simp [hV.2, iInter_subset])) (hg1 n))
+  have h_inter_eq : ⋂ n, g n ∩ V n = ⋂ n, f n := by ext; simp_all; grind
+  exact Subtype.dense_iff.mpr fun a _ ↦ h_inter_eq ▸ h_inter_dense a
 
 /-- If `p : Y → X` is an open embedding and `X` is a Baire space, then `Y` is a Baire space. -/
 theorem Topology.IsOpenEmbedding.baireSpace {Y : Type*} [TopologicalSpace Y] {p : Y → X}