awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
⊢ (f '' closure[inst] S).Subsingleton
have H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
Tactic: have H₄ : IsClosed (f '' (S ∩ closedPoints X)) := by
    obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))
    · simp [h]
    · rw [H₃.eq_singleton_of_mem hx]; exact H₂ hx
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
⊢ (f '' closure[inst] S).Subsingleton
have this : f '' closure[inst] (S ∩ closedPoints X) ⊆ closure[inst_1] (f '' (S ∩ closedPoints X))
Tactic: have := image_closure_subset_closure_image (s := S ∩ closedPoints X) hf₁
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst_1] (f '' (S ∩ closedPoints X))
this : f '' closure[inst] (S ∩ closedPoints X) ⊆ closure[inst_1] (f '' (S ∩ closedPoints X))
⊢ (f '' closure[inst] S).Subsingleton
have this₁ : f '' closure[inst] S ⊆ f '' (S ∩ closedPoints X)
Tactic: rw [JacobsonSpace.closure_inter_closedPoints_eq_closure hS, H₄.closure_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ topologicalKrullDim X ≤ 0
have refine : ∀ (Z Y : IrreducibleCloseds X) (h : Z ≤ Y) (x : X) (hx : x ∈ Y), x ∈ Z
Tactic: refine krullDim_nonpos_iff_forall_isMax.mpr fun Z Y h ↦ (h.antisymm' fun x hx ↦ ?_).le
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
⊢ x ∈ Z
have obtain : ∀ (z : X) (hz : z ∈ Z.carrier), x ∈ Z
Tactic: obtain ⟨z, hz⟩ := Z.2.nonempty
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
z : X
hz : z ∈ Z.carrier
⊢ x ∈ Z
have rwa : z ∈ Z
Tactic: rwa [DiscreteTopology.isDiscrete.subsingleton_of_isPreirreducible Y.2.isPreirreducible hx (h hz)]
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ coheight (map f ⋯ Z) = coheight Z
have rw : coheight (map f sorry Z) =
  coheight.{u_2} (α := (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
    ((orderIsoOfIsOpenEmbedding f hf :
          (a : IrreducibleCloseds X) → (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
        Z :
      (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
Tactic: rw [← coheight_orderIso (orderIsoOfIsOpenEmbedding f hf) Z]
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ coheight (map f ⋯ Z) =
    coheight.{u_2} (α := (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
      ((orderIsoOfIsOpenEmbedding f hf :
            (a : IrreducibleCloseds X) → (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
          Z :
        (↑{V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} : Type u_2))
have refine : ∀
  (a :
    { x : IrreducibleCloseds Y //
      Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty} x })
  (b : IrreducibleCloseds Y),
  (↑a : IrreducibleCloseds Y) < b →
    ∃ (a' :
      { x : IrreducibleCloseds Y //
        Membership.mem (γ := Set (IrreducibleCloseds Y)) {V : IrreducibleCloseds Y | (f ⁻¹' (↑V : Set Y)).Nonempty}
          x }),
      a < a' ∧ (↑a' : IrreducibleCloseds Y) = b
Tactic: refine .symm (coheight_eq_of_strictMono Subtype.val (Subtype.strictMono_coe _) ?_ _)
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (f x) = coheight x
have rw : coheight (α := IrreducibleCloseds Y)
    ((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) =
  coheight (map f sorry ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x))
Tactic: rw [← coheight_orderIso (irreducibleSetEquivPoints (α := Y)).symm (f x),
    ← coheight_orderIso (irreducibleSetEquivPoints (α := X)).symm x,
    ← Topology.IsOpenEmbedding.coheight_map hf]
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (α := IrreducibleCloseds Y)
      ((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) =
    coheight (map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x))
have e_a : (OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) =
  map f sorry ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.KrullDimension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : QuasiSober Y
inst_3 : T0Space Y
inst_4 : QuasiSober X
inst_5 : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ (OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) =
    map f ⋯ ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)
have e_a : (↑((OrderIso.symm irreducibleSetEquivPoints : (a : Y) → IrreducibleCloseds Y) (f x) : IrreducibleCloseds Y) : Set Y) =
  (↑(map f sorry ((OrderIso.symm irreducibleSetEquivPoints : (a : X) → IrreducibleCloseds X) x)) : Set Y)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
⊢ 𝓝 as = traverse 𝓝 as
have refine_1 : LE.le.{u_1} (α := List α → Filter (List α)) pure (traverse 𝓝)
Tactic: refine nhds_mkOfNhds _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
refine_1 : LE.le.{u_1} (α := List α → Filter (List α)) pure (traverse 𝓝)
⊢ 𝓝 as = traverse 𝓝 as
have refine_2 : ∀ (a : List α), ∀ s ∈ traverse 𝓝 a, ∀ᶠ (y : List α) in traverse 𝓝 a, s ∈ traverse 𝓝 y
Tactic: refine nhds_mkOfNhds _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)
have refine_1 : List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l
Tactic: suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using this
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
as l : List α
⊢ pure l ≤ traverse 𝓝 l
have refine_1 : LE.le.{u_1} (α := (fun (a : List α) ↦ Filter.{u_1} (List α)) []) (pure []) (traverse 𝓝 [])
Tactic: induction l with
    | nil => exact le_rfl
    | cons a l ih =>
      suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using this
      exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
as l : List α
refine_1 : LE.le.{u_1} (α := (fun (a : List α) ↦ Filter.{u_1} (List α)) []) (pure []) (traverse 𝓝 [])
⊢ pure l ≤ traverse 𝓝 l
have refine_1₁ : ∀ (a : α) (l : List α) (ih : pure l ≤ traverse 𝓝 l), pure (a :: l) ≤ traverse 𝓝 (a :: l)
Tactic: induction l with
    | nil => exact le_rfl
    | cons a l ih =>
      suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using this
      exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
have refine_2 : ∀ (u : List (Set α)) (hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u) (hus : sequence u ⊆ s),
  ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
Tactic: rcases (mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s
have nil : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s
Tactic: exists []
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] [] ∧ sequence [] ⊆ s
have nil : True ∧ sequence [] ⊆ s
Tactic: simp only [List.forall₂_nil_left_iff]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u : List (Set α)
a : α
b : Set α
l₁ : List α
l₂ : List (Set α)
ht : b ∈ 𝓝 a
h : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂
ih :
  ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b :: l₂) ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
have cons : ∀ (u : Set α) (hut : u ⊆ b) (hu : IsOpen[inst] u ∧ a ∈ u),
  ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
Tactic: rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
u_1 : List (Set α)
a : α
b : Set α
l₁ : List α
l₂ : List (Set α)
ht : b ∈ 𝓝 a
h : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂
ih :
  ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b :: l₂) ⊆ s
u : Set α
hut : u ⊆ b
hu : IsOpen[inst] u ∧ a ∈ u
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
have cons : ∀ (v : List (Set α)) (hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v)
  (hvss : sequence v ⊆ sequence l₂),
  ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
Tactic: rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
have nil : ∀ (s : Set (List α)) (hus : sequence [] ⊆ s),
  ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s
Tactic: induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons ht _ ih =>
        rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
        rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
        exact
          ⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩
Cleared hypotheses: s, hu, hus
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
nil :
  ∀ (s : Set (List α)) (hus : sequence [] ⊆ s),
    ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s
⊢ ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
have cons : ∀ {a : α} {b : Set α} {l₁ : List α} {l₂ : List (Set α)} (ht : b ∈ 𝓝 a),
  List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l₁ l₂ →
    ∀
      (ih :
        ∀ (s : Set (List α)) (hus : sequence l₂ ⊆ s),
          ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l₁ v ∧ sequence v ⊆ s)
      (s : Set (List α)) (hus : sequence (b :: l₂) ⊆ s),
      ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) (a :: l₁) v ∧ sequence v ⊆ s
Tactic: induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons ht _ ih =>
        rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
        rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
        exact
          ⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩
Cleared hypotheses: s, hu, hus
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
have this : ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
Tactic: have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s := by
      induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons ht _ ih =>
        rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
        rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
        exact
          ⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ (v : List (Set α)), List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
have refine_2 : ∀ (v : List (Set α)) (hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v) (hvs : sequence v ⊆ s),
  ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
Tactic: rcases this with ⟨v, hv, hvs⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
have this : sequence v ∈ traverse 𝓝 l
Tactic: have : sequence v ∈ traverse 𝓝 l :=
      mem_traverse _ _ <| hv.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
have refine_2 : ∀ (u : List α) (hu : u ∈ sequence v),
  Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ s ∈ traverse 𝓝 y) x} u
Tactic: refine mem_of_superset this fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu : u ∈ sequence v
⊢ Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ s ∈ traverse 𝓝 y) x} u
have hu₁ : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
Tactic: have hu := (List.mem_traverse _ _).1 hu
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
⊢ List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v
have refine : List.Forall₂ (flip fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) v u
Tactic: refine List.Forall₂.flip ?_
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
⊢ List.Forall₂ (flip fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) v u
have hv₁ : List.Forall₂ (fun (s : Set α) (a : α) ↦ IsOpen[inst] s ∧ a ∈ s) v l
Tactic: replace hv := hv.flip
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
hv : List.Forall₂ (fun (s : Set α) (a : α) ↦ IsOpen[inst] s ∧ a ∈ s) v l
⊢ List.Forall₂ (flip fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) v u
have simp : ∀ (hv : (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v l),
  (∀ a ∈ v, IsOpen[inst] a) ∧ List.Forall₂ Membership.mem v u
Tactic: simp only [List.forall₂_and_left, Function.flip_def] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Topology.List (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
⊢ Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ s ∈ traverse 𝓝 y) x} u
have this₁ : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v
Tactic: have : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v := by
      refine List.Forall₂.flip ?_
      replace hv := hv.flip
      simp only [List.forall₂_and_left, Function.flip_def] at hv ⊢
      exact ⟨hv.1, hu.flip⟩
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
l : List α
s : Set (List α)
u_1 : List (Set α)
hu_1 : List.Forall₂ (fun (b : α) (s : Set α) ↦ s ∈ 𝓝 b) l u_1
hus : sequence u_1 ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this_1 : sequence v ∈ traverse 𝓝 l
u : List α
hu_2 : u ∈ sequence v
hu : List.Forall₂ (fun (b : α) (a : Set α) ↦ b ∈ id a) u v
this : List.Forall₂ (fun (a : α) (s : Set α) ↦ IsOpen[inst] s ∧ a ∈ s) u v
⊢ Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ s ∈ traverse 𝓝 y) x} u
have refine_2 : Membership.mem (γ := Set (List α)) {x : List α | (fun (y : List α) ↦ sequence v ∈ traverse 𝓝 y) x} u
Tactic: grw [← hvs]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])
have rw : Eq.{u_1 + 1} (α := Filter (List α)) (traverse 𝓝 []) (pure [])
Tactic: rw [nhds_list, List.traverse_nil _]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : Eq.{u_1 + 1} (α := Filter (List α)) (traverse 𝓝 []) (pure [])
⊢ Eq.{u_1 + 1} (α := Filter (List α)) (𝓝 []) (pure [])
have rw₁ : Eq.{u_1 + 1} (α := Filter (List α)) (pure []) (pure [])
Tactic: rw [nhds_list, List.traverse_nil _]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
have rw : traverse 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
Tactic: rw [nhds_list, List.traverse_cons _, ← nhds_list]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
rw : traverse 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
⊢ 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
have rw₁ : (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> 𝓝 a <*> traverse 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l
Tactic: rw [nhds_list, List.traverse_cons _, ← nhds_list]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
rw : traverse 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
rw₁ : (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> 𝓝 a <*> traverse 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l
⊢ 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l
have rw₂ : (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> 𝓝 a <*> 𝓝 l = List.cons <$> 𝓝 a <*> 𝓝 l
Tactic: rw [nhds_list, List.traverse_cons _, ← nhds_list]
-- Lean 4 proof step from Mathlib.Topology.List (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun (p : α × List α) ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))
have rw : Filter.seq (Filter.map (fun (a : α) (b : List α) ↦ (a, b).1 :: (a, b).2) (𝓝 a)) (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l
Tactic: rw [nhds_cons, Tendsto, Filter.map_prod]