awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
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)
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)))
⊢ 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)))

Tactic:
apply ContDiff.dist ℝ

Premises used: Real, ContDiff.dist
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
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 := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
    ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (f y)

Tactic:
(toEuclidean (E := G)).contDiff.comp hf

Premises used: ContDiff.comp, toEuclidean, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
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 := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
    ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (g y)

Tactic:
(toEuclidean (E := G)).contDiff.comp hg

Premises used: ContDiff.comp, toEuclidean, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
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
⊢ ∀ (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:
fun x => toEuclidean.injective.ne (h x)

Premises used: Function.Injective.ne, ContinuousLinearEquiv.injective, toEuclidean
-- Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist
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 := EuclideanSpace ℝ (Fin (finrank ℝ G))) (↑n : ℕ∞ω) fun (y : F) ↦
    ((toEuclidean : G ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ G))) : (a : G) → EuclideanSpace ℝ (Fin (finrank ℝ G)))
      (f y)

Tactic:
exacts [(toEuclidean (E := G)).contDiff.comp hf,
    (toEuclidean (E := G)).contDiff.comp hg, fun x => toEuclidean.injective.ne (h x)]

Premises used: Function.Injective.ne, ContinuousLinearEquiv.injective, ContDiff.comp, toEuclidean, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E →ₗ[𝕜] 𝕜
⊢ Eq (α := (a : E) → ℝ) (⇑f.toSeminorm : (a : E) → ℝ) fun (x : E) ↦ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E →ₗ[𝕜] 𝕜
x : E
⊢ (f.toSeminorm : (a : E) → ℝ) x = norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E →ₗ[𝕜] 𝕜
r : ℝ
⊢ f.toSeminorm.ball 0 r = {x : E | norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) < r}

Tactic:
simp only [Seminorm.ball_zero_eq, toSeminorm_apply]

Premises used: LinearMap.toSeminorm_apply, Seminorm.ball_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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
h : ∀ (x : E), Eq (α := ℝ) ((f.toSeminorm.comp g : (a : E) → ℝ) x : ℝ) (((f ∘ₗ g).toSeminorm : (a : E) → ℝ) x : ℝ)
⊢ f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm

Tactic:
ext
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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
x : E
⊢ Eq (α := ℝ) ((f.toSeminorm.comp g : (a : E) → ℝ) x : ℝ) (((f ∘ₗ g).toSeminorm : (a : E) → ℝ) x : ℝ)

Tactic:
simp only [Seminorm.comp_apply, toSeminorm_apply, coe_comp, Function.comp_apply]

Premises used: Seminorm.comp_apply, LinearMap.coe_comp, LinearMap.toSeminorm_apply, Function.comp_apply
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
x : E
y : F
⊢ (B.toSeminormFamily y : (a : E) → ℝ) x =
    norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hr : B.SeparatingRight
⊢ Function.Injective (α := F) (β := StrongDual.{u_1, u_2} 𝕜 (WeakBilin B))
    (⇑(WeakBilin.eval B) : (a : F) → StrongDual 𝕜 (WeakBilin B))

Tactic:
(injective_iff_map_eq_zero _).mpr (fun f hf ↦
    (separatingRight_iff_linear_flip_nontrivial.mp hr) f (ContinuousLinearMap.coe_inj.mpr hf))

Premises used: Iff.mpr, ContinuousLinearMap.coe_inj, injective_iff_map_eq_zero, Iff.mp, LinearMap.separatingRight_iff_linear_flip_nontrivial
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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) → 𝕜)
mpr :
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜) →
    Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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) → 𝕜)

Tactic:
Submodule.span_induction
      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)

Premises used: Submodule.span_induction
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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) → 𝕜)

Tactic:
exact Submodule.span_induction
      (Set.forall_mem_range.mpr fun i ↦ continuous_iInf_dom continuous_induced_dom) continuous_zero
      (fun _ _ _ _ ↦ .add) (fun c _ _ h ↦ h.const_smul c)
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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)) φ

Tactic:
mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_

Premises used: mem_span_of_iInf_ker_le_ker
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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) → 𝕜)
mpr : ∀ (x : E) (hx : Membership.mem (γ := Submodule 𝕜 E) (⨅ (i : ι), (f i).ker) x), x ∈ φ.ker
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ

Tactic:
refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_

Premises used: mem_span_of_iInf_ker_le_ker
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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
⊢ ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢

Premises used: Submodule.mem_iInf, LinearMap.mem_ker
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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)
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 𝕜))
simp_rw₃ :
  Eq.{u_6 + 1} (α := Filter E) (⨅ (i : ι), Filter.comap.{u_6, u_5} (β := 𝕜) (⇑(f i) : (a : E) → 𝕜) (𝓝 0))
    (⨅ (i : ι),
      Filter.comap.{u_6, u_5} (β := 𝕜) ((⇑(f i) : (a : E) → 𝕜) : (a : E) → 𝕜) (𝓝 ((f i : (a : E) → 𝕜) 0) : Filter 𝕜))
⊢ Inseparable x 0

Tactic:
simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]

Premises used: nhds_iInf, map_zero, nhds_induced, Inseparable
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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

Tactic:
have : Inseparable x 0 := by
      -- Maybe missing lemmas about `Inseparable`?
      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
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 : 𝕜)
this : Inseparable x 0
⊢ Eq.{u_5 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
simpa only [map_zero] using (this.map φ_cont).eq

Premises used: map_zero, Inseparable.eq, Inseparable.map
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
this : Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
simp_rw :
  Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ (i : ι), 𝕜 ∙ f i) φ ↔
    ∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)

Tactic:
simp_rw [this, ← mem_span_iff_continuous_of_finite, Submodule.span_range_eq_iSup,
      iSup_subtype]

Premises used: iSup_subtype, Submodule.span_range_eq_iSup, LinearMap.mem_span_iff_continuous_of_finite
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
this : Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
rw rw₁ :
  (∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ) ↔
    ∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ (i : ι), 𝕜 ∙ f i) φ ↔
    ∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ

Tactic:
rw [Submodule.mem_iSup_iff_exists_finset]

Premises used: Submodule.mem_iSup_iff_exists_finset
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
φ₁ : Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)

Tactic:
suffices
      Continuous[t₁, t𝕜] φ ↔ ∃ s : Finset ι, Continuous[t₂ s, t𝕜] φ by
    simp_rw [this, ← mem_span_iff_continuous_of_finite, Submodule.span_range_eq_iSup,
      iSup_subtype]
    rw [Submodule.mem_iSup_iff_exists_finset]
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
⊢ IsTopologicalAddGroup E

Tactic:
have t₁_group : @IsTopologicalAddGroup E t₁ _ :=
    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
⊢ ∀ (s : Finset ι), IsTopologicalAddGroup E

Tactic:
have t₂_group (s : Finset ι) : @IsTopologicalAddGroup E (t₂ s) _ :=
    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
⊢ ContinuousSMul 𝕜 E

Tactic:
have t₁_smul : @ContinuousSMul 𝕜 E _ _ t₁ :=
    continuousSMul_iInf fun _ ↦ continuousSMul_induced _
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
⊢ ∀ (s : Finset ι), ContinuousSMul 𝕜 E

Tactic:
have t₂_smul (s : Finset ι) : @ContinuousSMul 𝕜 E _ _ (t₂ s) :=
    continuousSMul_iInf fun _ ↦ continuousSMul_induced _
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
simp_rw :
  Continuous[t₁, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ) ↔
    ∃ (s : Finset ι), Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
⊢ Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)

Tactic:
simp_rw [WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const]

Premises used: norm_withSeminorms, forall_const, WithSeminorms.continuous_iff_continuous_comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
rw :
  Membership.mem (γ := Filter E) (⨅ (i : ι), 𝓝 0)
    (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)
| Continuous[t₁, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)

Tactic:
rw [Seminorm.continuous_iff one_pos, nhds_iInf]

Premises used: nhds_iInf, Seminorm.continuous_iff, one_pos
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
conv :
  Membership.mem (γ := Filter E) (⨅ (i : ι), 𝓝 0)
      (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1) ↔
    ∃ (s : Finset ι), Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
⊢ Continuous[t₁, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ) ↔
    ∃ (s : Finset ι), Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)

Tactic:
conv in Continuous _ => rw [Seminorm.continuous_iff one_pos, nhds_iInf]

Premises used: nhds_iInf, Continuous, Seminorm.continuous_iff, one_pos