awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x : F
hx : ¬‖x‖ = 0
neg :
  ∀ (x : F) (hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x) (hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε),
    (q : (a : F) → ℝ) x ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖

Tactic:
refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx

Premises used: Seminorm.bound_of_shell, normSeminorm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x_1 : F
hx : ¬‖x_1‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε
⊢ (q : (a : F) → ℝ) x ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)

Tactic:
(le_of_lt <| show q x < _ from hε hlt).trans ?_

Premises used: le_of_lt, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x_1 : F
hx : ¬‖x_1‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε
neg : 1 ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)
⊢ (q : (a : F) → ℝ) x ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)

Tactic:
refine (le_of_lt <| show q x < _ from hε hlt).trans ?_

Premises used: le_of_lt, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x_1 : F
hx : ¬‖x_1‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε
neg : 1 / (‖c‖ / ε) ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
neg₁ neg₂ neg₃ neg₄ : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
⊢ 1 ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)

Tactic:
rwa [← div_le_iff₀' this, one_div_div]

Premises used: div_le_iff₀', one_div_div
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] (⇑q : (a : E) → ℝ)
rcases :
  ∀ (V : Set E) (hV : V ∈ p.basisSets) (hε : id V ⊆ q.ball 0 1), ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, hε⟩

Premises used: Filter.HasBasis.mem_iff, Seminorm.ball_mem_nhds, Iff.mp, WithSeminorms.hasBasis, one_pos
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] (⇑q : (a : E) → ℝ)
V : Set E
hV : V ∈ p.basisSets
hε : id V ⊆ q.ball 0 1
rcases :
  ∀ (s : Finset ι) (ε : ℝ) (ε_pos : 0 < ε) (hV : (s.sup p).ball 0 ε ∈ p.basisSets)
    (hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1), ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩

Premises used: Iff.mp, SeminormFamily.basisSets_iff, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
apply : Metric.ball 0 ε ⊆ q.ball 0 1
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)

Tactic:
apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)

Premises used: Seminorm.continuous, Metric.ball_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
rw : (s.sup p).ball 0 ε ⊆ q.ball 0 1
⊢ Metric.ball 0 ε ⊆ q.ball 0 1

Tactic:
rw [← ball_eq_metric]

Premises used: Seminorm.ball_eq_metric
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
⊢ (s.sup p).ball 0 ε ⊆ q.ball 0 1

Tactic:
hε

Premises used: setOf, Seminorm.ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
⊢ (s.sup p).ball 0 ε ⊆ q.ball 0 1

Tactic:
exact hε
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)

Tactic:
have : Continuous q := by
    apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)
    rw [← ball_eq_metric]
    exact hε
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
this : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)
rcases :
  ∀ (C : ℝ) (C_pos : 0 < C) (hC : ∀ (x_2 : E), (q : (a : E) → ℝ) x_2 ≤ C * ‖x_2‖),
    ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩

Premises used: Seminorm.bound_of_continuous_normedSpace
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
this : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)
C : ℝ
C_pos : 0 < C
hC : ∀ (x_2 : E), (q : (a : E) → ℝ) x_2 ≤ C * ‖x_2‖
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩

Premises used: LT.lt.le, Ne.symm, Subtype.mk, congr_arg, And.intro, Exists.intro, NNReal.toReal, LT.lt.ne
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
this : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)
C : ℝ
C_pos : 0 < C
hC : ∀ (x_2 : E), (q : (a : E) → ℝ) x_2 ≤ C * ‖x_2‖
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
exact ⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E

Tactic:
have := hp.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hbasis : HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
hconvex : ∀ i ∈ p.basisSets, Convex ℝ (id i)
⊢ LocallyConvexSpace ℝ E

Tactic:
apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets

Premises used: Real, SeminormFamily.basisSets, Membership.mem, id, LocallyConvexSpace.ofBasisZero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hbasis :
  HasBasis (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (fun (s : Set E) ↦ s ∈ p.basisSets) id
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id

Tactic:
rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]

Premises used: AddGroupFilterBasis.nhds_eq, AddGroupFilterBasis.N_zero, WithSeminorms.topology_eq_withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ HasBasis (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (fun (s : Set E) ↦ s ∈ p.basisSets) id

Tactic:
FilterBasis.hasBasis _

Premises used: SeminormFamily.basisSets, Set.Mem, iSup, FilterBasis.hasBasis, Set.iUnion
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ HasBasis (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (fun (s : Set E) ↦ s ∈ p.basisSets) id

Tactic:
exact FilterBasis.hasBasis _

Premises used: FilterBasis.hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : s ∈ p.basisSets
⊢ Membership.mem (γ := Set (Set E)) (⋃ (s : Finset ι), ⋃ (r : ℝ), ⋃ (_ : 0 < r), {(s.sup p).ball 0 r}) s

Tactic:
change s ∈ Set.iUnion _ at hs

Premises used: Set.iUnion
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : Membership.mem (γ := Set (Set E)) (⋃ (s : Finset ι), ⋃ (r : ℝ), ⋃ (_ : 0 < r), {(s.sup p).ball 0 r}) s
⊢ ∃ (i : Finset ι) (i_1 : ℝ) (_ : 0 < i_1), s = (i.sup p).ball 0 i_1

Tactic:
simp_rw [Set.mem_iUnion, Set.mem_singleton_iff] at hs

Premises used: Set.mem_iUnion, Set.mem_singleton_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : ∃ (i : Finset ι) (i_1 : ℝ) (_ : 0 < i_1), s = (i.sup p).ball 0 i_1
hconvex : ∀ (I : Finset ι) (r : ℝ), 0 < r → Convex ℝ (id ((I.sup p).ball 0 r))
⊢ Convex ℝ (id s)

Tactic:
rcases hs with ⟨I, r, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
I : Finset ι
r : ℝ
w : 0 < r
⊢ Convex ℝ (id ((I.sup p).ball 0 r))

Tactic:
convex_ball _ _ _

Premises used: setOf, Seminorm.convex_ball, Seminorm.ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
I : Finset ι
r : ℝ
w : 0 < r
⊢ Convex ℝ (id ((I.sup p).ball 0 r))

Tactic:
exact convex_ball _ _ _

Premises used: Seminorm.convex_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : PolynormableSpace ℝ E
⊢ LocallyConvexSpace ℝ E

Tactic:
PolynormableSpace.withSeminorms ℝ E |>.toLocallyConvexSpace

Premises used: WithSeminorms.toLocallyConvexSpace, Real, PolynormableSpace.withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
⊢ LocallyConvexSpace ℝ E

Tactic:
(norm_withSeminorms 𝕜 E).toLocallyConvexSpace

Premises used: WithSeminorms.toLocallyConvexSpace, norm_withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace ℝ E
⊢ LocallyConvexSpace ℝ E

Tactic:
NormedSpace.toLocallyConvexSpace' ℝ

Premises used: Real, NormedSpace.toLocallyConvexSpace'
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
i : ι
f : E →ₛₗ[σ₁₂] F
⊢ q.comp f i = (q i).comp f

Tactic:
rfl

Premises used: SeminormFamily.comp, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
h : ∀ (x : E), Eq (α := ℝ) (((s.sup q).comp f : (a : E) → ℝ) x : ℝ) ((s.sup (q.comp f) : (a : E) → ℝ) x : ℝ)
⊢ (s.sup q).comp f = s.sup (q.comp f)

Tactic:
ext x
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
h :
  (↑(s.sup fun (i : ι) ↦ NNReal.mk ((q i : (a : F) → ℝ) ((f : (a : E) → F) x : F)) ⋯) : ℝ) =
    (↑(s.sup fun (i : ι) ↦ NNReal.mk ((q.comp f i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ Eq (α := ℝ) (((s.sup q).comp f : (a : E) → ℝ) x : ℝ) ((s.sup (q.comp f) : (a : E) → ℝ) x : ℝ)

Tactic:
rw [Seminorm.comp_apply, Seminorm.finset_sup_apply, Seminorm.finset_sup_apply]

Premises used: Seminorm.finset_sup_apply, Seminorm.comp_apply
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ (↑(s.sup fun (i : ι) ↦ NNReal.mk ((q i : (a : F) → ℝ) ((f : (a : E) → F) x : F)) ⋯) : ℝ) =
    (↑(s.sup fun (i : ι) ↦ NNReal.mk ((q.comp f i : (a : E) → ℝ) x) ⋯) : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
⊢ IsTopologicalAddGroup F

Tactic:
have := hq.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
⊢ IsTopologicalAddGroup E

Tactic:
have : IsTopologicalAddGroup E := topologicalAddGroup_induced f
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this_1 : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
this : IsTopologicalAddGroup E
rw :
  Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι), comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (⨅ (i : ι), comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))
⊢ WithSeminorms (q.comp f)

Tactic:
rw [(q.comp f).withSeminorms_iff_nhds_eq_iInf, nhds_induced, map_zero,
    q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.comap_iInf]

Premises used: map_zero, SeminormFamily.comp, Filter.comap_iInf, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_induced, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this_1 : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
this : IsTopologicalAddGroup E
⊢ Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι), comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (⨅ (i : ι), comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))

Tactic:
iInf_congr fun i => ?_

Premises used: iInf_congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this_1 : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
this : IsTopologicalAddGroup E
refine :
  ∀ (i : ι),
    Eq (α := Filter E) (comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
      (comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))
⊢ Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι), comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (⨅ (i : ι), comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))

Tactic:
refine iInf_congr fun i => ?_

Premises used: iInf_congr