-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
simp_rw :
  𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
simp_rw₁ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          {s : Set C(X, Y) |
            f ∈ s ∧
              Membership.mem (γ := Set (Set C(X, Y)))
                (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
                  {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
                s}
          s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₂ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        f ∈ s ∧
          Membership.mem (γ := Set (Set C(X, Y)))
            (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
              {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
            s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₃ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
            (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
              {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
            s ∧
          f ∈ s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₄ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
            {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
          s),
        ⨅ (_ : f ∈ s), 𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₅ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          ((fun (x : Prod.{u_2, u_3} (Set X) (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) x.1 x.2}) ''
            SProd.sprod (α := Set (Set X)) (β := Set (Set Y)) {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
          s),
        ⨅ (_ : f ∈ s), 𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₆ :
  Eq (α := Filter C(X, Y))
    (⨅ b ∈ SProd.sprod (α := Set (Set X)) (β := Set (Set Y)) {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t},
      ⨅ (_ : Membership.mem (γ := Set C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) b.1 b.2} f),
        𝓟 {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) b.1 b.2})
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₇ :
  Eq (α := Filter C(X, Y))
    (⨅ (a : Set X),
      ⨅ (_ : Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} a),
        ⨅ (b : Set Y),
          ⨅ (_ : Membership.mem (γ := Set (Set Y)) {t : Set Y | IsOpen[inst_1] t} b),
            ⨅ (_ : Membership.mem (γ := Set C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) a b} f),
              𝓟 {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) a b})
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
⊢ 𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}

Tactic:
simp_rw +instances [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]

Premises used: Set.image_prod, ContinuousMap.compactOpen_eq, TopologicalSpace.nhds_generateFrom, Set.mem_setOf_eq, and_comm, biInf_prod, iInf_image, iInf_and