awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
have false : uniformSpace α γ = bif false then uniformSpace α γ else uniformSpace α γ
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
i : Bool
false : uniformSpace α γ = bif Bool.false then uniformSpace α γ else uniformSpace α γ
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
have true : uniformSpace α γ = bif true then uniformSpace α γ else uniformSpace α γ
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (α := α →ᵤ γ) (β := α →ᵤ β)
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))
have refine : uniformSpace α γ ≤
  UniformSpace.comap
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))
    (uniformSpace α β)
Tactic: refine uniformContinuous_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ ≤
    UniformSpace.comap
      (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))
      (uniformSpace α β)
have _ : uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β)
Tactic: calc
      𝒰(α, γ, _) ≤ 𝒰(α, γ, ‹UniformSpace β›.comap f) :=
        UniformFun.mono (uniformContinuous_iff.mp hf)
      _ = 𝒰(α, β, _).comap (f ∘ ·) := by exact UniformFun.comap_eq
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
f : γ → α
⊢ UniformContinuous (β := γ →ᵤ β) fun (g : α →ᵤ β) ↦
    (ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) g ∘ f)
have rw : ∀ ib ∈ 𝓤 β,
  ∃ ia ∈ 𝓤 β,
    ∀ x ∈ UniformFun.gen α β ia,
      Membership.mem (α := (γ →ᵤ β) × (γ →ᵤ β)) (UniformFun.gen γ β ib)
        (((ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.1 ∘ f),
            (ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.2 ∘ f)) :
          (γ →ᵤ β) × (γ →ᵤ β))
Tactic: rw [UniformContinuous,
      (UniformFun.hasBasis_uniformity α β).tendsto_iff (UniformFun.hasBasis_uniformity γ β)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ UniformContinuous (α := α →ᵤ β) (β := α → β) (⇑toFun : (a : α →ᵤ β) → α → β)
have rw : ∀ (i : α), UniformContinuous (β := β) fun (x : α →ᵤ β) ↦ (toFun : (a : α →ᵤ β) → α → β) x i
Tactic: rw [uniformContinuous_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ Tendsto F p (𝓝 f) ↔
    TendstoUniformly.{u_1, u_2, u_4} (α := α) (β := β) ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ F)
      ((toFun : (a : α →ᵤ β) → α → β) f) p
have rw : (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, Membership.mem (γ := Set (α →ᵤ β)) {g : α →ᵤ β | (f, g) ∈ UniformFun.gen α β i} (F x)) ↔
  ∀ u ∈ 𝓤 β,
    ∀ᶠ (n : ι) in p,
      ∀ (x : α),
        Membership.mem (α := β × β) u
          (((toFun : (a : α →ᵤ β) → α → β) f x, ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ F) n x) : β × β)
Tactic: rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
⊢ IsUniformInducing (α := α →ᵤ β × γ) (β := (α →ᵤ β) × (α →ᵤ γ))
    (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) : (a : α →ᵤ β × γ) → (α →ᵤ β) × (α →ᵤ γ))
have comap_uniformity : Eq (α := Filter ((α →ᵤ β × γ) × (α →ᵤ β × γ)))
  (comap (β := ((α →ᵤ β) × (α →ᵤ γ)) × (α →ᵤ β) × (α →ᵤ γ))
    (fun (x : (α →ᵤ β × γ) × (α →ᵤ β × γ)) ↦
      ((Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ : (a : α →ᵤ β × γ) → (α →ᵤ β) × (α →ᵤ γ)) x.1,
        (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ : (a : α →ᵤ β × γ) → (α →ᵤ β) × (α →ᵤ γ))
          x.2))
    (𝓤 ((α →ᵤ β) × (α →ᵤ γ))))
  (𝓤 (α →ᵤ β × γ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
⊢ Eq (α := Filter (((i : α) → β × γ) × ((i : α) → β × γ))) (𝓤 ((i : α) → β × γ)) (𝓤 (α → β × γ))
have comap_uniformity : Eq (α := UniformSpace ((i : α) → β × γ))
  (UniformSpace.comap (β := ((i : α) → β) × ((i : α) → γ))
    (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
      (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ))
    instUniformSpaceProd)
  (uniformSpace α (β × γ))
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
⊢ Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
      (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
        (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ))
      (UniformSpace.comap Prod.fst (uniformSpace α β) ⊓ UniformSpace.comap Prod.snd (uniformSpace α γ)))
    (uniformSpace α (β × γ))
have comap_uniformity : Eq (α := UniformSpace ((i : α) → β × γ))
  (UniformSpace.comap
      (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
        (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
          (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
      (uniformSpace α β) ⊓
    UniformSpace.comap
      (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
        (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
          (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
      (uniformSpace α γ))
  (uniformSpace α (β × γ))
Tactic: rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
⊢ Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))
have this : Eq (α := UniformSpace (α →ᵤ β × γ)) (uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ)) (uniformSpace α (β × γ))
Tactic: have := (@UniformFun.inf_eq α (β × γ)
      (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
this : Eq (α := UniformSpace (α →ᵤ β × γ)) (uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ)) (uniformSpace α (β × γ))
⊢ Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))
have comap_uniformity : ∀
  (this :
    Eq (α := UniformSpace (α →ᵤ β × γ))
      (UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓ uniformSpace α (β × γ))
      (uniformSpace α (β × γ))),
  Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))
Tactic: rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
this : Eq (α := UniformSpace (α →ᵤ β × γ)) (uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ)) (uniformSpace α (β × γ))
comap_uniformity :
  ∀
    (this :
      Eq (α := UniformSpace (α →ᵤ β × γ))
        (UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓ uniformSpace α (β × γ))
        (uniformSpace α (β × γ))),
    Eq (α := UniformSpace ((i : α) → β × γ))
      (UniformSpace.comap
          (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
            (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
              (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
          (uniformSpace α β) ⊓
        UniformSpace.comap
          (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
            (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
              (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
          (uniformSpace α γ))
      (uniformSpace α (β × γ))
⊢ Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))
have comap_uniformity₁ : ∀
  (this :
    Eq (α := UniformSpace (α →ᵤ β × γ))
      (UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓
        UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.snd ∘ x) (uniformSpace α γ))
      (uniformSpace α (β × γ))),
  Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))
Tactic: rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing (α := α →ᵤ (i : ι) → δ i) (β := (i : ι) → (fun (i : ι) ↦ α → δ i) i)
    (⇑(Equiv.piComm fun (a : α) ↦ δ) : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i)
have refine : Eq (α := Filter ((α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)))
  (comap (β := ((i : ι) → (fun (i : ι) ↦ α → δ i) i) × ((i : ι) → (fun (i : ι) ↦ α → δ i) i))
    (fun (x : (α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)) ↦
      ((Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.1,
        (Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.2))
    (𝓤 ((i : ι) → (fun (i : ι) ↦ α → δ i) i)))
  (𝓤 (α →ᵤ (i : ι) → δ i))
Tactic: refine @IsUniformInducing.mk ?_ ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := Filter ((α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)))
    (comap (β := ((i : ι) → (fun (i : ι) ↦ α → δ i) i) × ((i : ι) → (fun (i : ι) ↦ α → δ i) i))
      (fun (x : (α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)) ↦
        ((Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.1,
          (Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.2))
      (𝓤 ((i : ι) → (fun (i : ι) ↦ α → δ i) i)))
    (𝓤 (α →ᵤ (i : ι) → δ i))
have change : Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y)))
  (comap (Prod.map (Function.swap (φ := fun (a : α) ↦ δ)) (Function.swap (φ := fun (a : α) ↦ δ)))
    (𝓤 ((i : ι) → (fun (i : ι) ↦ α → δ i) i)))
  (𝓤 (α →ᵤ (i : ι) → δ i))
Tactic: change comap (Prod.map Function.swap Function.swap) _ = _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y))) (𝓤 ((x : α) → (y : ι) → δ y))
    (𝓤 (α →ᵤ (i : ι) → δ i))
have h : Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
  (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ)) (Pi.uniformSpace fun (i : ι) ↦ α → δ i))
  (uniformSpace α ((i : ι) → δ i))
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.ofCoreEq
        (UniformSpace.toCore
          (⨅ (i : ι),
            UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
              ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
        (Pi.topologicalSpace (Y := fun (i : ι) ↦ α → δ i)) ⋯))
    (uniformSpace α ((i : ι) → δ i))
have h : Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
  (⨅ (i : ι),
    UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
        ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
  (⨅ (i : ι), uniformSpace α ((i : ι) → δ i))
Tactic: rw [UniformSpace.ofCoreEq_toCore, UniformSpace.ofCoreEq_toCore,
        UniformSpace.comap_iInf, UniformFun.iInf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
          ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i))
have h : ∀ (i : ι),
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
        ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (uniformSpace α ((i : ι) → δ i))
Tactic: refine iInf_congr fun i => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
i : ι
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
        ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (uniformSpace α ((i : ι) → δ i))
have h : Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
  (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i ∘ Function.swap (φ := fun (a : α) ↦ δ))
    ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i))
  (UniformSpace.comap (β := α → δ i) (fun (x : α → (i : ι) → δ i) ↦ Function.eval (β := δ) i ∘ x)
    (uniformSpace α (δ i)))
Tactic: rw [← UniformSpace.comap_comap, UniformFun.comap_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
⊢ IsClosed[topologicalSpace α β]
    {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}
have refine : ∀ (f : α →ᵤ β) (u : Filter (α →ᵤ β)),
  u.NeBot →
    ∀ (hu : u ≤ 𝓟 {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)})
      (huf : u ≤ 𝓝 f),
      Membership.mem (γ := Set (α →ᵤ β))
        {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)} f
Tactic: refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
h : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}
huf : u ≤ 𝓝 f
⊢ Membership.mem (γ := Set (α →ᵤ β))
    {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)} f
have huf₁ : TendstoUniformly (α := α) (β := β) ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ id) ((toFun : (a : α →ᵤ β) → α → β) f) u
Tactic: rw [← tendsto_id', UniformFun.tendsto_iff_tendstoUniformly] at huf
Cleared hypotheses: huf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ uniformSpace α β =
    UniformSpace.comap
        (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (uniformSpace δ₁ β) ⊓
      UniformSpace.comap
        (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (uniformSpace δ₂ β)
have h : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
have h : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
Tactic: refine le_antisymm (le_inf ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
h : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
have h₁ : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
Tactic: refine le_antisymm (le_inf ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
h : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
h₁ : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
have h₂ : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
Tactic: refine le_antisymm (le_inf ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
have h : ∀ (U : Set (β × β)) (hU : U ∈ 𝓤 β) (x : (α →ᵤ β) × (α →ᵤ β)) (x : α) (f g : α →ᵤ β)
  (hfg :
    Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
      ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
            (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
                ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
              Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
                ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
          UniformFun.gen δ₁ β (U, U).1 ∩
        (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
            (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
                ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
              Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
                ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
          UniformFun.gen δ₂ β (U, U).2)
      (f, g)),
  Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
Tactic: refine
      (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩