awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Continuous[p.moduleFilterBasis.topology, q.moduleFilterBasis.topology] id

Tactic:
refine continuous_of_isBounded (.mk (topology := _) rfl) (.mk (topology := _) rfl)
    LinearMap.id (by assumption)

Premises used: LinearMap.id, WithSeminorms.mk, WithSeminorms.continuous_of_isBounded, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded q p LinearMap.id

Tactic:
assumption
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Continuous[q.moduleFilterBasis.topology, p.moduleFilterBasis.topology] id

Tactic:
refine continuous_of_isBounded (.mk (topology := _) rfl) (.mk (topology := _) rfl)
    LinearMap.id (by assumption)

Premises used: LinearMap.id, WithSeminorms.mk, WithSeminorms.continuous_of_isBounded, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := Finset ι) fun (s : Finset ι) ↦ s.sup p

Tactic:
hp.congr ?_ ?_

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
refine_1 : Seminorm.IsBounded p (fun (s : Finset ι) ↦ s.sup p) LinearMap.id
refine_2 : Seminorm.IsBounded (fun (s : Finset ι) ↦ s.sup p) p LinearMap.id
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := Finset ι) fun (s : Finset ι) ↦ s.sup p

Tactic:
refine hp.congr ?_ ?_

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ∃ (s_1 : Finset ι) (C : ℝ≥0), comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ C • s_1.sup p

Tactic:
⟨s, 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
refine_1 : comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 (s.sup p)
⊢ ∃ (s_1 : Finset ι) (C : ℝ≥0), comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ C • s_1.sup p

Tactic:
refine ⟨s, 1, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
refine_1 :
  LE.le.{u_6} (α := Seminorm 𝕜 E) (comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id)
    (comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id)
⊢ comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 (s.sup p)

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ LE.le.{u_6} (α := Seminorm 𝕜 E) (comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id)
    (comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id)

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ (s : Finset (Finset ι)) (C : ℝ≥0),
    (p i).comp LinearMap.id ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (s : Finset ι) ↦ s.sup p)

Tactic:
⟨{{i}}, 1, ?_⟩

Premises used: Exists.intro, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
i : ι
refine_2 :
  (p i).comp LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {{i}} fun (s : Finset ι) ↦ s.sup p)
⊢ ∃ (s : Finset (Finset ι)) (C : ℝ≥0),
    (p i).comp LinearMap.id ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (s : Finset ι) ↦ s.sup p)

Tactic:
refine ⟨{{i}}, 1, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
i : ι
refine_2 : (p i).comp LinearMap.id ≤ (p i).comp LinearMap.id
⊢ (p i).comp LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {{i}} fun (s : Finset ι) ↦ s.sup p)

Tactic:
rw [Finset.sup_singleton, Finset.sup_singleton, one_smul]

Premises used: Finset.sup_singleton, one_smul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ (p i).comp LinearMap.id

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (Finset.Iic i).sup p

Tactic:
hp.congr ?_ ?_

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
refine_1 : Seminorm.IsBounded p (fun (i : ι) ↦ (Finset.Iic i).sup p) LinearMap.id
refine_2 : Seminorm.IsBounded (fun (i : ι) ↦ (Finset.Iic i).sup p) p LinearMap.id
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (Finset.Iic i).sup p

Tactic:
refine hp.congr ?_ ?_

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ (s : Finset ι) (C : ℝ≥0), comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ C • s.sup p

Tactic:
⟨Finset.Iic i, 1, ?_⟩

Premises used: Exists.intro, Finset.Iic, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
refine_1 : comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 ((Finset.Iic i).sup p)
⊢ ∃ (s : Finset ι) (C : ℝ≥0), comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ C • s.sup p

Tactic:
refine ⟨Finset.Iic i, 1, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
refine_1 :
  LE.le.{u_6} (α := Seminorm 𝕜 E) (comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id)
    (comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id)
⊢ comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 ((Finset.Iic i).sup p)

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ LE.le.{u_6} (α := Seminorm 𝕜 E) (comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id)
    (comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id)

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ (s : Finset ι) (C : ℝ≥0),
    (p i).comp LinearMap.id ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (i : ι) ↦ (Finset.Iic i).sup p)

Tactic:
⟨{i}, 1, ?_⟩

Premises used: Exists.intro, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
refine_2 :
  (p i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {i} fun (i : ι) ↦ (Finset.Iic i).sup p)
⊢ ∃ (s : Finset ι) (C : ℝ≥0),
    (p i).comp LinearMap.id ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (i : ι) ↦ (Finset.Iic i).sup p)

Tactic:
refine ⟨{i}, 1, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
refine_2 : (p i).comp LinearMap.id ≤ (Finset.Iic i).sup p
⊢ (p i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {i} fun (i : ι) ↦ (Finset.Iic i).sup p)

Tactic:
rw [Finset.sup_singleton, one_smul]

Premises used: Finset.sup_singleton, one_smul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ (Finset.Iic i).sup p

Tactic:
(Finset.le_sup (Finset.mem_Iic.mpr le_rfl) : p i ≤ (Finset.Iic i).sup p)

Premises used: Iff.mpr, le_rfl, Finset.mem_Iic, Finset.le_sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ (Finset.Iic i).sup p

Tactic:
exact (Finset.le_sup (Finset.mem_Iic.mpr le_rfl) : p i ≤ (Finset.Iic i).sup p)

Premises used: Iff.mpr, le_rfl, Finset.mem_Iic, Finset.le_sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))

Tactic:
hp.congr ?_ ?_

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
refine_1 : Seminorm.IsBounded.{u_2, u_2, u_6, u_6, u_9, u_10} (ι' := ι') p (p ∘ (⇑e : (a : ι') → ι)) LinearMap.id
refine_2 : Seminorm.IsBounded.{u_2, u_2, u_6, u_6, u_10, u_9} (ι := ι') (p ∘ (⇑e : (a : ι') → ι)) p LinearMap.id
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))

Tactic:
refine hp.congr ?_ ?_

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι'
h :
  ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup (singleton (α := ι) ((e : (a : ι') → ι) i : ι)) p)
⊢ ∃ (s : Finset ι) (C : ℝ≥0), ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤ C • s.sup p

Tactic:
use {e i}, 1

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι
h :
  (p i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) 1
      (Finset.sup (β := ι') (singleton (α := ι') ((e.symm : (a : ι) → ι') i : ι')) (p ∘ (⇑e : (a : ι') → ι)))
⊢ ∃ (s : Finset ι') (C : ℝ≥0), (p i).comp LinearMap.id ≤ C • s.sup (p ∘ (⇑e : (a : ι') → ι))

Tactic:
use {e.symm i}, 1

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
h :
  ∀ (i : ι'),
    ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤
      HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup (singleton (α := ι) ((e : (a : ι') → ι) i : ι)) p)
h₁ :
  ∀ (i : ι),
    (p i).comp LinearMap.id ≤
      HSMul.hSMul (α := ℝ≥0) 1
        (Finset.sup (β := ι') (singleton (α := ι') ((e.symm : (a : ι) → ι') i : ι')) (p ∘ (⇑e : (a : ι') → ι)))
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))

Tactic:
refine hp.congr ?_ ?_ <;>
  intro i <;>
  [use {e i}, 1; use {e.symm i}, 1]

Premises used: WithSeminorms.congr
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι'
⊢ ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup (singleton (α := ι) ((e : (a : ι') → ι) i : ι)) p)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι
⊢ (p i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) 1
      (Finset.sup (β := ι') (singleton (α := ι') ((e.symm : (a : ι) → ι') i : ι')) (p ∘ (⇑e : (a : ι') → ι)))

Tactic:
simp
-- 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) → ℝ)
x : F
hx : ‖x‖ = 0
⊢ Eq (α := ℝ) ((q : (a : F) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
(map_zero q) ▸
    ((specializes_iff_mem_closure.mpr <| mem_closure_zero_iff_norm.mpr hx).map hq).eq.symm

Premises used: Iff.mpr, specializes_iff_mem_closure, Eq.rec, map_zero, Specializes.eq, mem_closure_zero_iff_norm, Specializes.map, Eq.symm
-- 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) → ℝ)
⊢ Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)

Tactic:
have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
-- 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)
rcases :
  ∀ (ε : ℝ) (ε_pos : 0 < ε) (hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))),
    ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖

Tactic:
rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' <| Iio_mem_nhds one_pos)
    with ⟨ε, ε_pos, hε⟩

Premises used: Iio_mem_nhds, Filter.HasBasis.mem_iff, Iff.mp, NormedAddGroup.nhds_zero_basis_norm_lt, one_pos
-- 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))
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Premises used: NormedField.exists_one_lt_norm
-- 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‖
⊢ 0 < ‖c‖ / ε

Tactic:
positivity
-- 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‖
⊢ 0 < ‖c‖ / ε

Tactic:
have : 0 < ‖c‖ / ε := by positivity
-- 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‖ / ε
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖

Tactic:
⟨‖c‖ / ε, this, fun x ↦ ?_⟩

Premises used: Norm.norm, HDiv.hDiv, And.intro, Exists.intro
-- 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‖ / ε
refine : ∀ (x : F), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖

Tactic:
refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
-- 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
pos : ∀ (hx : ‖x‖ = 0), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
neg : ∀ (hx : ¬‖x‖ = 0), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖

Tactic:
by_cases hx : ‖x‖ = 0
-- 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
pos : LE.le (α := ℝ) ((q : (a : F) → ℝ) x : ℝ) (0 : ℝ)
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖

Tactic:
rw [hx, mul_zero]

Premises used: MulZeroClass.mul_zero
-- 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
⊢ LE.le (α := ℝ) ((q : (a : F) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
le_of_eq (map_eq_zero_of_norm_eq_zero q hq hx)

Premises used: Seminorm.map_eq_zero_of_norm_eq_zero, le_of_eq
-- 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
⊢ LE.le (α := ℝ) ((q : (a : F) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact le_of_eq (map_eq_zero_of_norm_eq_zero q hq hx)

Premises used: Seminorm.map_eq_zero_of_norm_eq_zero, le_of_eq
-- 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
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖

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

Premises used: Seminorm.bound_of_shell, normSeminorm