-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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})
⊢ 𝓝 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}
have 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})
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]