awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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 =
    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))))
have 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))))
Tactic: rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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))))
⊢ 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))))
have 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)))))
Tactic: rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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 (closedBall x r)
have 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)))))
Tactic: rw [closedBall_eq_image]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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
⊢ closure[inst_1] (ball x r) = closedBall x r
have 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
Tactic: rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h,
    closedBall_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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
⊢ closure[inst_1] (ball x r) = closedBall x r
have 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
Tactic: rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h,
    closedBall_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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
⊢ closure[inst_1] (ball x r) = closedBall x r
have 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
Tactic: rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h,
    closedBall_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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
⊢ closure[inst_1] (ball x r) = closedBall x r
have 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)))))
Tactic: rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h,
    closedBall_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (hypothesis)
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
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r
have 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))))
Tactic: rw [ball_eq_preimage, ← image_subset_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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
⊢ (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r) (closedBall x)
have 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)
Tactic: rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
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
⊢ (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r) (ball x)
have 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)
Tactic: rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
G : Type u_3
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n : ℕ∞ω) f
hg : ContDiff ℝ (↑n : ℕ∞ω) g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : F) ↦
    Dist.dist (α := EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
          (f x) :
        EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
          (g x) :
        EuclideanSpace ℝ (Fin (finrank ℝ G)))
have hf₁ : ContDiff ℝ (F := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
  ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G))) (f y)
Tactic: apply ContDiff.dist ℝ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
G : Type u_3
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n : ℕ∞ω) f
hg : ContDiff ℝ (↑n : ℕ∞ω) g
h : ∀ (x : F), f x ≠ g x
hf₁ :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
    ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (f y)
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : F) ↦
    Dist.dist (α := EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
          (f x) :
        EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
          (g x) :
        EuclideanSpace ℝ (Fin (finrank ℝ G)))
have hg₁ : ContDiff ℝ (F := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
  ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G))) (g y)
Tactic: apply ContDiff.dist ℝ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.EuclideanDist (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
G : Type u_3
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ (↑n : ℕ∞ω) f
hg : ContDiff ℝ (↑n : ℕ∞ω) g
h : ∀ (x : F), f x ≠ g x
hf₁ :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
    ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (f y)
hg₁ :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
    ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (g y)
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : F) ↦
    Dist.dist (α := EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
          (f x) :
        EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
          (g x) :
        EuclideanSpace ℝ (Fin (finrank ℝ G)))
have hne : ∀ (x : F),
  Ne (α := EuclideanSpace ℝ (Fin (finrank ℝ G)))
    (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
        (f x) :
      EuclideanSpace ℝ (Fin (finrank ℝ G)))
    (((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
        (g x) :
      EuclideanSpace ℝ (Fin (finrank ℝ G)))
Tactic: apply ContDiff.dist ℝ
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
f : F →ₗ[𝕜] 𝕜
g : E →ₗ[𝕜] F
⊢ f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm
have h : ∀ (x : E), Eq (α := ℝ) ((f.toSeminorm.comp g : (a : E) → ℝ) x : ℝ) (((f ∘ₗ g).toSeminorm : (a : E) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
have mp : Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ →
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
mp :
  Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ →
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
have mpr : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜) →
  Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ
have mpr : ∀ (x : E) (hx : Membership.mem (γ := Submodule 𝕜 E) (⨅ (i : ι), (f i).ker) x), x ∈ φ.ker
Tactic: refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x_1 : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
x : E
hx : Membership.mem (γ := Submodule 𝕜 E) (⨅ (i : ι), (f i).ker) x
⊢ x ∈ φ.ker
have hx₁ : ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
Tactic: simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x_1 : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
x : E
hx : ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ Inseparable x 0
have simp_rw : 𝓝 x = 𝓝 0
Tactic: simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x_1 : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
x : E
hx : ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
simp_rw : 𝓝 x = 𝓝 0
⊢ Inseparable x 0
have simp_rw₁ : Eq.{u_6 + 1} (α := Filter E) (⨅ (i : ι), 𝓝 x) (⨅ (i : ι), 𝓝 0)
Tactic: simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x_1 : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
x : E
hx : ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
simp_rw : 𝓝 x = 𝓝 0
simp_rw₁ : Eq.{u_6 + 1} (α := Filter E) (⨅ (i : ι), 𝓝 x) (⨅ (i : ι), 𝓝 0)
⊢ Inseparable x 0
have simp_rw₂ : Eq.{u_6 + 1} (α := Filter E)
  (⨅ (i : ι),
    Filter.comap.{u_6, u_5} (β := 𝕜) ((⇑(f i) : (a : E) → 𝕜) : (a : E) → 𝕜) (𝓝 ((f i : (a : E) → 𝕜) x) : Filter 𝕜))
  (⨅ (i : ι),
    Filter.comap.{u_6, u_5} (β := 𝕜) ((⇑(f i) : (a : E) → 𝕜) : (a : E) → 𝕜) (𝓝 ((f i : (a : E) → 𝕜) 0) : Filter 𝕜))
Tactic: simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]