awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
He₁ : x ∈ e.baseSet
He'₁ : x ∈ e'.baseSet
Heq₁ : ∀ (p : Z), proj p = x → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet
have hx₁ : x ∈ frontier (Iic x)
Tactic: obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)
Cleared hypotheses: a, He, He', Heq, hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ (↑e : Z → B × F) p = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p
have fst : ((↑e : Z → B × F) p).1 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).1
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
fst : ((↑e : Z → B × F) p).1 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).1
⊢ (↑e : Z → B × F) p = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p
have snd : ((↑e : Z → B × F) p).2 = ((↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) : Z → B × F) p).2
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint e.source e'.source
have rw : Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)
Tactic: rw [e.source_eq, e'.source_eq]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint e.target e'.target
have rw : SProd.sprod (β := Set F) e.baseSet univ ⊓ SProd.sprod (β := Set F) e'.baseSet univ ≤ ⊥
Tactic: rw [e.target_eq, e'.target_eq, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ ((↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) : Z → B × F) p).1 = proj p
have inl : (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p
Tactic: change (e.source.piecewise e e' p).1 = proj p
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
⊢ ((↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) : Z → B × F) p).1 = proj p
have inr : (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p
Tactic: change (e.source.piecewise e e' p).1 = proj p
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
⊢ (e.source.piecewise (β := fun (a : Z) ↦ B × F) (↑e : Z → B × F) (↑e' : Z → B × F) p).1 = proj p
have inr : p ∉ e.source
Tactic: rw [piecewise_eq_of_notMem, e'.coe_fst hp']
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
⊢ p ∉ e.source
have inr : ∀ (hp' : p ∈ proj ⁻¹' e'.baseSet), p ∉ proj ⁻¹' e.baseSet
Tactic: simp only [source_eq] at hp' ⊢
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceSubtype]
    fun (ex : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
    Subtype.mk (p := fun (x : Z) ↦ x ∈ T.source) (T.lift (↑ex.1 : Z) (↑ex.2 : B)) ⋯
have h : Continuous[instTopologicalSpaceProd, inst_2] fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
  T.lift (↑x.1 : Z) (↑x.2 : B)
Tactic: apply Continuous.subtype_mk
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ T.lift (↑x.1 : Z) (↑x.2 : B)
have h : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
  fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
  ((↑x.2 : B), ((↑T : Z → B × F) (↑x.1 : Z)).2)
Tactic: refine T.continuousOn_invFun.comp_continuous ?_ (by simp [mem_target])
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
    fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦
    ((↑x.2 : B), ((↑T : Z → B × F) (↑x.1 : Z)).2)
have h : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
  fun (x : Prod.{u_4, u_1} (↑T.source : Type u_4) (↑T.baseSet : Type u_1)) ↦ (↑T : Z → B × F) (↑x.1 : Z)
Tactic: refine .prodMk (by fun_prop) (.snd ?_)
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
T_1 : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst_4 : TopologicalSpace ι
inst_5 : LocallyCompactPair.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T_1.baseSet : Type u_1)
i : ι
e : (↑T_1.source : Type u_4)
T : Trivialization F proj
inst_6 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
Ψ : C(((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι,
  ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1) × ι) :=
  {
    toFun := fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
      (eγt.1.2, eγt.2),
    continuous_toFun := ⋯ }
⊢ C((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1),
    ContinuousMap.{u_5, u_4} ι (↑T.source : Type u_4))
have refine : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd]
  fun (eγt : ((↑T.source : Type u_4) × ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)) × ι) ↦
  (eγt.1.1, (eγt.1.2 : (a : ι) → (↑T.baseSet : Type u_1)) eγt.2)
Tactic: refine ContinuousMap.curry <| T.liftCM.comp <| ⟨fun eγt => ⟨eγt.1.1, eγt.1.2 eγt.2⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst_3 : TopologicalSpace ι
inst_4 : LocallyCompactPair.{u_5, u_1} ι (↑T.baseSet : Type u_1)
γ : ContinuousMap.{u_5, u_1} ι (↑T.baseSet : Type u_1)
i : ι
e : (↑T.source : Type u_4)
h : proj (↑e : Z) = (↑((γ : (a : ι) → (↑T.baseSet : Type u_1)) i) : B)
⊢ (((T.clift : (a : (↑T.source : Type u_4) × C(ι, (↑T.baseSet : Type u_1))) → C(ι, (↑T.source : Type u_4))) (e, γ) :
          ContinuousMap.{u_5, u_4} ι (↑T.source : Type u_4)) :
        (a : ι) → (↑T.source : Type u_4))
      i =
    e
have this : proj (↑e : Z) ∈ T.baseSet
Tactic: have : proj e ∈ T.baseSet := by simp [h]
-- Lean 4 proof step from Mathlib.Topology.FiberPartition (hypothesis)
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
⊢ (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) ∈
    (↑(Fiber.mk f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)) :
      Set S)
have this : (↑x : (↑(↑a : Set S) : Type u_1)) ∈ (↑b : Set (↑(↑a : Set S) : Type u_1))
Tactic: have := x.prop
-- Lean 4 proof step from Mathlib.Topology.FiberPartition (hypothesis)
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
this : (↑x : (↑(↑a : Set S) : Type u_1)) ∈ (↑b : Set (↑(↑a : Set S) : Type u_1))
⊢ (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) ∈
    (↑(Fiber.mk f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)) :
      Set S)
have this₁ : f (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) = Fiber.image (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b
Tactic: simp only [sigmaIncl, ContinuousMap.coe_mk, Fiber.mem_iff_eq_image, comp_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.FiberPartition (goal)
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (Y := (↑(↑a : Set S) : Type u_1)) (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S))
x : (↑(↑b : Set (↑(↑a : Set S) : Type u_1)) : Type u_1)
this : f (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) = Fiber.image (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b
⊢ (↑(↑x : (↑(↑a : Set S) : Type u_1)) : S) ∈
    (↑(Fiber.mk f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)) :
      Set S)
have rw : (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S))
    (Fiber.preimage (f ∘ fun (x : (↑(↑a : Set S) : Type u_1)) ↦ (↑x : S)) b) =
  f (↑(Fiber.preimage (f ∘ (⇑(sigmaIncl (g ∘ f) a) : (a : (↑(↑a : Set S) : Type u_1)) → S)) b) : S)
Tactic: rw [Fiber.mem_iff_eq_image, Fiber.mk_image, this, ← Fiber.map_preimage_eq_image]
-- Lean 4 proof step from Mathlib.Topology.FiberPartition (goal)
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
x : Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y)
⊢ CompactSpace.{u_1} (↑(↑x : Set S) : Type u_1)
have obtain : ∀ (y : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2))
  (hy :
    (fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
          (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
        y =
      (↑x : Set S)),
  CompactSpace.{u_1} (↑(↑x : Set S) : Type u_1)
Tactic: obtain ⟨y, hy⟩ := x.prop
-- Lean 4 proof step from Mathlib.Topology.FiberPartition (goal)
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
l : LocallyConstant S Y
inst_1 : CompactSpace S
x : Fiber.{u_1, u_2} (Y := S) (Z := Y) (⇑l : (a : S) → Y)
y : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)
hy :
  (fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
        (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
      y =
    (↑x : Set S)
⊢ CompactSpace.{u_1} (↑(↑x : Set S) : Type u_1)
have rw : IsCompact.{u_1} (X := S)
  ((fun (x : (↑(Set.range.{u_2, u_1 + 1} (ι := S) (⇑l : (a : S) → Y)) : Type u_2)) ↦
      (Set.preimage (β := Y) (⇑l : (a : S) → Y) {(↑x : Y)} : Set S))
    y)
Tactic: rw [← isCompact_iff_compactSpace, ← hy]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun (i : ι) ↦ Iic (𝓟 (s i))
have rw : (l.lift' (Iic ∘ 𝓟)).HasBasis p fun (i : ι) ↦ Iic (𝓟 (s i))
Tactic: rw [nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
X : Type u_4
l : Filter X
⊢ Tendsto pure l (𝓝 l)
have rw : ∀ s ∈ l, ∀ᶠ (a : X) in l, Membership.mem (γ := Filter X) (pure a) s
Tactic: rw [Filter.tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
x : α
⊢ Eq (α := Filter (Filter α)) (𝓝 (pure x)) (𝓟 {⊥, pure x})
have rw : Eq (α := Filter (Filter α)) (𝓝 (𝓟 {x})) (𝓟 {⊥, 𝓟 {x}})
Tactic: rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
x : α
rw : Eq (α := Filter (Filter α)) (𝓝 (𝓟 {x})) (𝓟 {⊥, 𝓟 {x}})
⊢ Eq (α := Filter (Filter α)) (𝓝 (pure x)) (𝓟 {⊥, pure x})
have rw₁ : Eq (α := Filter (Filter α)) (𝓟 (Iic (𝓟 {x}))) (𝓟 {⊥, 𝓟 {x}})
Tactic: rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
x : α
rw : Eq (α := Filter (Filter α)) (𝓝 (𝓟 {x})) (𝓟 {⊥, 𝓟 {x}})
rw₁ : Eq (α := Filter (Filter α)) (𝓟 (Iic (𝓟 {x}))) (𝓟 {⊥, 𝓟 {x}})
⊢ Eq (α := Filter (Filter α)) (𝓝 (pure x)) (𝓟 {⊥, pure x})
have rw₂ : Eq (α := Filter (Filter α)) (𝓟 (Iic (pure x))) (𝓟 {⊥, pure x})
Tactic: rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
x : α
rw : Eq (α := Filter (Filter α)) (𝓝 (𝓟 {x})) (𝓟 {⊥, 𝓟 {x}})
rw₁ : Eq (α := Filter (Filter α)) (𝓟 (Iic (𝓟 {x}))) (𝓟 {⊥, 𝓟 {x}})
rw₂ : Eq (α := Filter (Filter α)) (𝓟 (Iic (pure x))) (𝓟 {⊥, pure x})
⊢ Eq (α := Filter (Filter α)) (𝓝 (pure x)) (𝓟 {⊥, pure x})
have rw₃ : Eq (α := Filter (Filter α)) (𝓟 {⊥, pure x}) (𝓟 {⊥, pure x})
Tactic: rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (𝓝 (⨅ (i : ι), f i)) (⨅ (i : ι), 𝓝 (f i))
have simp : Eq.{u_2 + 1} (α := Filter (Filter α)) (Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟)) (⨅ (i : ι), (f i).lift' (Iic ∘ 𝓟))
Tactic: simp only [nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟)) (⨅ (i : ι), (f i).lift' (Iic ∘ 𝓟))
have hg : ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
Tactic: apply lift'_iInf_of_map_univ
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
hg : ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ Eq.{u_2 + 1} (α := Filter (Filter α)) (Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟)) (⨅ (i : ι), (f i).lift' (Iic ∘ 𝓟))
have hg' : Eq.{u_2 + 1} (α := Set (Filter α)) ((Iic ∘ 𝓟) univ) univ
Tactic: apply lift'_iInf_of_map_univ
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l
have simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
Tactic: simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l
have simp_rw₁ : ⋂₀ {s : Set (Filter α) | Membership.mem (γ := Filter (Filter α)) (l.lift' fun (x : Set α) ↦ Iic (𝓟 x)) s} = Iic l
Tactic: simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
simp_rw₁ :
  ⋂₀ {s : Set (Filter α) | Membership.mem (γ := Filter (Filter α)) (l.lift' fun (x : Set α) ↦ Iic (𝓟 x)) s} = Iic l
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l
have simp_rw₂ : ⋂ s ∈ l, Iic (𝓟 s) = Iic l
Tactic: simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
simp_rw₁ :
  ⋂₀ {s : Set (Filter α) | Membership.mem (γ := Filter (Filter α)) (l.lift' fun (x : Set α) ↦ Iic (𝓟 x)) s} = Iic l
simp_rw₂ : ⋂ s ∈ l, Iic (𝓟 s) = Iic l
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l
have simp_rw₃ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | x ≤ 𝓟 s}) {x : Filter α | x ≤ l}
Tactic: simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
simp_rw₁ :
  ⋂₀ {s : Set (Filter α) | Membership.mem (γ := Filter (Filter α)) (l.lift' fun (x : Set α) ↦ Iic (𝓟 x)) s} = Iic l
simp_rw₂ : ⋂ s ∈ l, Iic (𝓟 s) = Iic l
simp_rw₃ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | x ≤ 𝓟 s}) {x : Filter α | x ≤ l}
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l
have simp_rw₄ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | s ∈ x}) {x : Filter α | x ≤ l}
Tactic: simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
simp_rw : ⋂₀ {s : Set (Filter α) | s ∈ l.lift' (Iic ∘ 𝓟)} = Iic l
simp_rw₁ :
  ⋂₀ {s : Set (Filter α) | Membership.mem (γ := Filter (Filter α)) (l.lift' fun (x : Set α) ↦ Iic (𝓟 x)) s} = Iic l
simp_rw₂ : ⋂ s ∈ l, Iic (𝓟 s) = Iic l
simp_rw₃ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | x ≤ 𝓟 s}) {x : Filter α | x ≤ l}
simp_rw₄ : Eq.{u_2 + 1} (α := Set (Filter α)) (⋂ s ∈ l, {x : Filter α | s ∈ x}) {x : Filter α | x ≤ l}
⊢ ⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l} = Iic l
have simp_rw₅ : Eq.{u_2 + 1} (α := Set (Filter α)) {x : Filter α | ∀ (i : Set α) (i_1 : i ∈ l), i ∈ x} {x : Filter α | x ≤ l}
Tactic: simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂
have refine : ∀ (h : 𝓝 l₁ ≤ 𝓝 l₂), l₁ ≤ l₂
Tactic: refine ⟨fun h => ?_, fun h => monotone_nhds h⟩
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂
have rw : Subset.{u_2} (α := Set (Filter α)) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₁}) (⋂₀ {s : Set (Filter α) | s ∈ 𝓝 l₂})
Tactic: rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
have rw : s ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
Tactic: rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
s : Set (Filter α)
l : Filter α
rw : s ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
have rw₁ : (∃ t ∈ l, Iic (𝓟 t) ⊆ s) ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
Tactic: rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Filter (goal)
Goal:
α : Type u_2
l : Filter α
⊢ closure {l} = Ici l
have h : ∀ (l' : Filter α), Membership.mem (γ := Set (Filter α)) (closure {l}) l' ↔ l' ∈ Ici l
Tactic: ext l'
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen[inst] (f i)
⊢ ⋂ i ∈ I, f i = ⋂₀ (f '' I)
have rw : Eq.{u_1 + 1} (α := Set X) (⋂ i ∈ I, f i) (⋂ a ∈ I, f a)
Tactic: rw [sInter_image]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst] (f i)
⊢ ⋂ (i : ι'), f i = ⋂₀ range f
have rw : Eq.{u_1 + 1} (α := Set X) (⋂ (i : ι'), f i) (⋂ (x : ι'), f x)
Tactic: rw [sInter_range]