awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
e_f :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-k * j) : ℂ)
e_f₂ :
  HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(k * j)) : ℂ)
e_f₃ :
  HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
      ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ)
      ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
e_f₄ e_f₅ :
  HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
      ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑((toCircle : (a : ZMod N) → Circle) (-(k * j))) : ℂ) : ℂ)
      ((χ : (a : ZMod N) → ℂ) j : ℂ)
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((stdAddChar : (a : ZMod N) → ℂ) (-(j * k)) : ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) j : ℂ) ((mulShift stdAddChar (-k) : (a : ZMod N) → ℂ) j : ℂ)

Tactic:
rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]

Premises used: AddChar.mulShift_apply, mul_comm, neg_mul, DFunLike.coe, ZMod.stdAddChar_apply
-- Module: Mathlib.Analysis.Fourier.ZMod
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
rw :
  gaussSum χ (mulShift stdAddChar (-k)) = HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
rw₁ rw₂ :
  HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar) =
    HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)
⊢ (𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ) k =
    HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-k) : ℂ) (gaussSum χ stdAddChar)

Tactic:
rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]

Premises used: gaussSum_mulShift_of_isPrimitive, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ ball x r =
    preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.ball
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.ball, Euclidean.dist, Set.preimage, Euclidean.ball, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ closedBall x r =
    preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))

Tactic:
rfl

Premises used: Set.Mem, setOf, Euclidean.dist, Set.preimage, Euclidean.closedBall, Metric.closedBall, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ ball x r ⊆ closedBall x r

Tactic:
fun _ (hy : _ < r) =>
  le_of_lt hy

Premises used: Set.Mem, setOf, le_of_lt, Set.Subset, Euclidean.closedBall, Euclidean.ball
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsOpen[inst_1] (ball x r)

Tactic:
Metric.isOpen_ball.preimage toEuclidean.continuous

Premises used: Set.Mem, setOf, Metric.ball, Euclidean.dist, Metric.isOpen_ball, Set.preimage, ContinuousLinearEquiv.continuous, Euclidean.ball, IsOpen.preimage, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
hr : 0 < r
⊢ x ∈ ball x r

Tactic:
Metric.mem_ball_self hr

Premises used: Set.Mem, setOf, Metric.mem_ball_self, Metric.ball, Euclidean.dist, Euclidean.ball
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
rw :
  closedBall x r =
    preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Set E)
    (preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
⊢ closedBall x r =
    image (α := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.symm toEuclidean) : (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) :
        (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E)
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))

Tactic:
rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]

Premises used: ContinuousLinearEquiv.image_symm_eq_preimage, Euclidean.closedBall_eq_preimage, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
rw :
  IsCompact.{u_1} (X := E)
    (image (α := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.symm toEuclidean) : (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) :
        (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E)
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_eq_image]

Premises used: Euclidean.closedBall_eq_image
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact.{u_1} (X := E)
    (image (α := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.symm toEuclidean) : (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) :
        (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E)
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))

Tactic:
(isCompact_closedBall _ _).image toEuclidean.symm.continuous

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.continuous, ProperSpace.isCompact_closedBall, IsCompact.image, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact.{u_1} (X := E)
    (image (α := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.symm toEuclidean) : (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E) :
        (a : EuclideanSpace ℝ (Fin (finrank ℝ E))) → E)
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))

Tactic:
exact (isCompact_closedBall _ _).image toEuclidean.symm.continuous
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsClosed[inst_1] (closedBall x r)

Tactic:
isCompact_closedBall.isClosed

Premises used: Euclidean.isCompact_closedBall, IsCompact.isClosed
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
h : r ≠ 0
rw :
  closure[inst_1]
      (preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
        ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
          (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
        (Metric.ball
            (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
                (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
              x)
            r :
          Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))) =
    closedBall x r
rw₁ :
  preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (closure
          (Metric.ball
            (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
                (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
              x)
            r) :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    closedBall x r
rw₂ :
  preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))) =
    closedBall x r
rw₃ rw₄ :
  Eq.{u_1 + 1} (α := Set E)
    (preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (preimage (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (Metric.closedBall
          (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x)
          r :
        Set (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
⊢ closure[inst_1] (ball x r) = closedBall x r

Tactic:
rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h,
    closedBall_eq_preimage]

Premises used: Euclidean.closedBall_eq_preimage, Euclidean.ball_eq_preimage, ContinuousLinearEquiv.preimage_closure, DFunLike.coe, Euclidean.closure_ball, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed[inst_1] s
h : s ⊆ ball x R
⊢ Subset (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) '' s : Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (Metric.ball
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        R :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))

Tactic:
rw [ball_eq_preimage, ← image_subset_iff] at h

Premises used: Euclidean.ball_eq_preimage, Set.image_subset_iff
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed[inst_1] s
h :
  Subset (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) '' s : Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (Metric.ball
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        R :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
r : ℝ
hr : r ∈ Ioo 0 R
hsr :
  Subset (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) '' s : Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (Metric.ball
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Tactic:
⟨r, hr, image_subset_iff.1 hsr⟩

Premises used: And.intro, Exists.intro, Iff.mp, Set.image_subset_iff
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed[inst_1] s
h :
  Subset (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) '' s : Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (Metric.ball
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        R :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
r : ℝ
hr : r ∈ Ioo 0 R
hsr :
  Subset (α := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    ((⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) '' s : Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (Metric.ball
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        r :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Tactic:
exact ⟨r, hr, image_subset_iff.1 hsr⟩
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
rw :
  Filter.HasBasis
    (Filter.comap (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.toHomeomorph toEuclidean) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
        (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (𝓝
          (((ContinuousLinearEquiv.toHomeomorph toEuclidean : E ≃ₜ EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x) :
        Filter (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (fun (r : ℝ) ↦ 0 < r) (closedBall x)
⊢ (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r) (closedBall x)

Tactic:
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]

Premises used: Homeomorph.nhds_eq_comap, ContinuousLinearEquiv.toHomeomorph, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis
    (Filter.comap (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.toHomeomorph toEuclidean) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
        (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (𝓝
          (((ContinuousLinearEquiv.toHomeomorph toEuclidean : E ≃ₜ EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x) :
        Filter (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (fun (r : ℝ) ↦ 0 < r) (closedBall x)

Tactic:
Metric.nhds_basis_closedBall.comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Euclidean.dist, Set.preimage, Euclidean.closedBall, Metric.nhds_basis_closedBall, Metric.closedBall
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis
    (Filter.comap (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.toHomeomorph toEuclidean) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
        (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (𝓝
          (((ContinuousLinearEquiv.toHomeomorph toEuclidean : E ≃ₜ EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x) :
        Filter (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (fun (r : ℝ) ↦ 0 < r) (closedBall x)

Tactic:
exact Metric.nhds_basis_closedBall.comap _

Premises used: Filter.HasBasis.comap, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
hr : 0 < r
⊢ closedBall x r ∈ 𝓝 x

Tactic:
nhds_basis_closedBall.mem_of_mem hr

Premises used: Euclidean.nhds_basis_closedBall, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
rw :
  Filter.HasBasis
    (Filter.comap (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.toHomeomorph toEuclidean) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
        (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (𝓝
          (((ContinuousLinearEquiv.toHomeomorph toEuclidean : E ≃ₜ EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x) :
        Filter (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (fun (r : ℝ) ↦ 0 < r) (ball x)
⊢ (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r) (ball x)

Tactic:
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]

Premises used: Homeomorph.nhds_eq_comap, ContinuousLinearEquiv.toHomeomorph, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis
    (Filter.comap (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.toHomeomorph toEuclidean) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
        (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (𝓝
          (((ContinuousLinearEquiv.toHomeomorph toEuclidean : E ≃ₜ EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x) :
        Filter (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (fun (r : ℝ) ↦ 0 < r) (ball x)

Tactic:
Metric.nhds_basis_ball.comap _

Premises used: Set.Mem, setOf, Metric.ball, Filter.HasBasis.comap, Euclidean.dist, Set.preimage, Metric.nhds_basis_ball, Euclidean.ball
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis
    (Filter.comap (β := EuclideanSpace ℝ (Fin (finrank ℝ E)))
      ((⇑(ContinuousLinearEquiv.toHomeomorph toEuclidean) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) :
        (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
      (𝓝
          (((ContinuousLinearEquiv.toHomeomorph toEuclidean : E ≃ₜ EuclideanSpace ℝ (Fin (finrank ℝ E))) :
              (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            x) :
        Filter (EuclideanSpace ℝ (Fin (finrank ℝ E)))))
    (fun (r : ℝ) ↦ 0 < r) (ball x)

Tactic:
exact Metric.nhds_basis_ball.comap _

Premises used: Filter.HasBasis.comap, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : T2Space E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : FiniteDimensional ℝ E
x : E
r : ℝ
hr : 0 < r
⊢ ball x r ∈ 𝓝 x

Tactic:
nhds_basis_ball.mem_of_mem hr

Premises used: Euclidean.nhds_basis_ball, Filter.HasBasis.mem_of_mem