awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : ι
⊢ Eq (α := Filter E) (comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))

Tactic:
Filter.comap_comap

Premises used: Filter.comap_comap
-- 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
i : ι
⊢ Eq (α := Filter E) (comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))

Tactic:
exact Filter.comap_comap

Premises used: Filter.comap_comap
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
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
inst_8 : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
⊢ PolynormableSpace 𝕜 E

Tactic:
f.withSeminorms_induced (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace

Premises used: WithSeminorms.toPolynormableSpace, PolynormableSpace.withSeminorms, LinearMap.withSeminorms_induced
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
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
inst_8 : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
⊢ PolynormableSpace 𝕜 E

Tactic:
exact f.withSeminorms_induced (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace

Premises used: WithSeminorms.toPolynormableSpace, PolynormableSpace.withSeminorms, LinearMap.withSeminorms_induced
-- 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
inst_8 : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F)
rw : WithSeminorms (q.comp f)
⊢ WithSeminorms (q.comp f)

Tactic:
rw [hf.eq_induced]

Premises used: Topology.IsInducing.eq_induced
-- 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
inst_8 : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F)
⊢ WithSeminorms (q.comp f)

Tactic:
f.withSeminorms_induced hq

Premises used: LinearMap.withSeminorms_induced
-- 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
inst_8 : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F)
⊢ WithSeminorms (q.comp f)

Tactic:
exact f.withSeminorms_induced hq

Premises used: LinearMap.withSeminorms_induced
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
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
inst_8 : PolynormableSpace 𝕜₂ F
inst_9 : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F)
⊢ PolynormableSpace 𝕜 E

Tactic:
hf.withSeminorms (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace

Premises used: Topology.IsInducing.withSeminorms, WithSeminorms.toPolynormableSpace, PolynormableSpace.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 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
inst_8 : PolynormableSpace 𝕜₂ F
S : Submodule 𝕜₂ F
⊢ PolynormableSpace.{u_3, u_7} 𝕜₂ ↥S

Tactic:
IsInducing.polynormableSpace (f := S.subtype) .subtypeVal

Premises used: Topology.IsInducing.polynormableSpace, Topology.IsInducing.subtypeVal
-- 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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
⊢ ∀ (i : ι), IsTopologicalAddGroup E

Tactic:
have : ∀ i, @IsTopologicalAddGroup E (t i) _ :=
    fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ (t i) _ (hp i)
-- 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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this : ∀ (i : ι), IsTopologicalAddGroup E
⊢ IsTopologicalAddGroup E

Tactic:
have : @IsTopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance
-- 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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this_1 : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
simp_rw :
  ∀ (hp : ∀ (i : ι), t i = ⨅ (i_1 : κ i), UniformSpace.toTopologicalSpace),
    Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : (i : ι) × κ i), UniformSpace.toTopologicalSpace)
⊢ WithSeminorms (SeminormFamily.sigma (κ := κ) p)

Tactic:
simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢

Premises used: SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf
-- 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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
this_1 : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ (i_1 : κ i), UniformSpace.toTopologicalSpace
rw : Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : ι), ⨅ (j : κ i), UniformSpace.toTopologicalSpace)
⊢ Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : (i : ι) × κ i), UniformSpace.toTopologicalSpace)

Tactic:
rw [iInf_sigma]

Premises used: iInf_sigma
-- 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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
this_1 : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ (i_1 : κ i), UniformSpace.toTopologicalSpace
⊢ Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : ι), ⨅ (j : κ i), UniformSpace.toTopologicalSpace)

Tactic:
iInf_congr hp

Premises used: iInf_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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
this_1 : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ (i_1 : κ i), UniformSpace.toTopologicalSpace
⊢ Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : ι), ⨅ (j : κ i), UniformSpace.toTopologicalSpace)

Tactic:
exact iInf_congr hp

Premises used: iInf_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
t : ι → TopologicalSpace E
ht : ∀ (i : ι), PolynormableSpace 𝕜 E
x : TopologicalSpace E := ⨅ (i : ι), t i
⊢ PolynormableSpace 𝕜 E

Tactic:
withSeminorms_iInf (fun i ↦ (ht i).withSeminorms') |>.toPolynormableSpace

Premises used: WithSeminorms.toPolynormableSpace, withSeminorms_iInf
-- 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
t : ι → TopologicalSpace E
ht : ∀ (i : ι), PolynormableSpace 𝕜 E
x : TopologicalSpace E := ⨅ (i : ι), t i
⊢ PolynormableSpace 𝕜 E

Tactic:
exact withSeminorms_iInf (fun i ↦ (ht i).withSeminorms') |>.toPolynormableSpace

Premises used: WithSeminorms.toPolynormableSpace, withSeminorms_iInf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
rw : PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
rw [sInf_eq_iInf']

Premises used: sInf_eq_iInf'
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
.iInf fun t ↦ hts t.1 t.2

Premises used: PolynormableSpace.iInf, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
exact .iInf fun t ↦ hts t.1 t.2
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
rw : PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
rw [← sInf_pair]

Premises used: sInf_pair
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
⊢ ∀ (t : TopologicalSpace E), Membership.mem (γ := Set (TopologicalSpace E)) {t₁, t₂} t → PolynormableSpace 𝕜 E

Tactic:
simp [ht₁, ht₂]
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
exact .sInf (by simp [ht₁, ht₂])
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
ι : Type u_9
inst : NormedField 𝕜
κ : ι → Type u_11
E : ι → Type u_12
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_12} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
p : (i : ι) → SeminormFamily.{u_2, u_12, u_11} 𝕜 (E i) (κ i)
hp : ∀ (i : ι), WithSeminorms (p i)
⊢ WithSeminorms (𝕜 := 𝕜) (E := (i : ι) → E i) (ι := (i : ι) × κ i)
    (SeminormFamily.sigma (κ := κ) fun (i : ι) ↦ (p i).comp (σ₁₂ := RingHom.id 𝕜) (LinearMap.proj (φ := E) i))

Tactic:
withSeminorms_iInf fun i ↦ (LinearMap.proj i).withSeminorms_induced (hp i)

Premises used: Set.Mem, setOf, LinearMap.proj, OrderDual, withSeminorms_iInf, LinearMap.withSeminorms_induced
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕝 : Type u_4
𝕝₂ : Type u_5
E_1 : Type u_6
F : Type u_7
G : Type u_8
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E_1
inst_2 : Module 𝕜 E_1
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
E : ι → Type u_11
inst_8 : (i : ι) → AddCommGroup (E i)
inst_9 : (i : ι) → Module.{u_2, u_11} 𝕜 (E i)
inst_10 : (i : ι) → TopologicalSpace (E i)
inst_11 : ∀ (i : ι), PolynormableSpace.{u_2, u_11} 𝕜 (E i)
⊢ PolynormableSpace 𝕜 ((i : ι) → E i)

Tactic:
.iInf fun i ↦ .induced (LinearMap.proj (R := 𝕜) (φ := E) i)

Premises used: Set.Mem, setOf, PolynormableSpace.induced, PolynormableSpace.iInf, LinearMap.proj, OrderDual
-- 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 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
E₁ : Type u_11
E₂ : Type u_12
inst_8 : AddCommGroup E₁
inst_9 : AddCommGroup E₂
inst_10 : Module 𝕜 E₁
inst_11 : Module 𝕜 E₂
inst_12 : TopologicalSpace E₁
inst_13 : TopologicalSpace E₂
inst_14 : PolynormableSpace 𝕜 E₁
inst_15 : PolynormableSpace 𝕜 E₂
⊢ PolynormableSpace 𝕜 (E₁ × E₂)

Tactic:
.inf (.induced <| LinearMap.fst 𝕜 E₁ E₂) (.induced <| LinearMap.snd 𝕜 E₁ E₂)

Premises used: LinearMap.fst, LinearMap.snd, setOf, PolynormableSpace.induced, PolynormableSpace.inf
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace 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 : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ IsUniformAddGroup E

Tactic:
have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
rw : IsCountablyGenerated.{u_6} (α := E) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
⊢ IsCountablyGenerated.{u_6} (α := E) (𝓝 0)

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]

Premises used: SeminormFamily.withSeminorms_iff_nhds_eq_iInf, Iff.mp
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ IsCountablyGenerated.{u_6} (α := E) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))

Tactic:
Filter.iInf.isCountablyGenerated _

Premises used: Filter.iInf.isCountablyGenerated
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ IsCountablyGenerated.{u_6} (α := E) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))

Tactic:
exact Filter.iInf.isCountablyGenerated _

Premises used: Filter.iInf.isCountablyGenerated
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ IsCountablyGenerated.{u_6} (α := E) (𝓝 0)

Tactic:
have : (𝓝 (0 : E)).IsCountablyGenerated := by
    rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
    exact Filter.iInf.isCountablyGenerated _
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this : IsCountablyGenerated.{u_6} (α := E) (𝓝 0)
⊢ (𝓤 E).IsCountablyGenerated

Tactic:
have : (uniformity E).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this_3 : IsCountablyGenerated.{u_6} (α := E) (𝓝 0)
this : (𝓤 E).IsCountablyGenerated
⊢ FirstCountableTopology E

Tactic:
UniformSpace.firstCountableTopology E

Premises used: UniformSpace.firstCountableTopology
-- 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
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this_3 : IsCountablyGenerated.{u_6} (α := E) (𝓝 0)
this : (𝓤 E).IsCountablyGenerated
⊢ FirstCountableTopology E

Tactic:
exact UniformSpace.firstCountableTopology E

Premises used: UniformSpace.firstCountableTopology
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
h : A.IsHermitian
i : n
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (A i i) = A i i
rw₁ : star (A i i) = A i i
rw₂ : Aᴴ i i = A i i
rw₃ rw₄ : A i i = A i i
⊢ (↑((re : (a : 𝕜) → ℝ) (A i i)) : 𝕜) = A i i

Tactic:
rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]

Premises used: RCLike.star_def, Matrix.IsHermitian.eq, RCLike.conj_eq_iff_re, Matrix.conjTranspose_apply
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
h : A.IsHermitian
⊢ (fun (i : n) ↦ (↑((re : (a : 𝕜) → ℝ) (A.diag i)) : 𝕜)) = A.diag

Tactic:
funext h.coe_re_apply_self

Premises used: funext, Matrix.IsHermitian.coe_re_apply_self
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
⊢ FiniteDimensional 𝕜 E

Tactic:
have : FiniteDimensional 𝕜 E := b.toBasis.finiteDimensional_of_finite
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
simp_rw :
  (∀ (x y : E),
      inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
        inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y) ↔
    A.IsHermitian
⊢ LinearMap.IsSymmetric.{u_1, u_4} (𝕜 := 𝕜) (E := E) ((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A) ↔
    A.IsHermitian

Tactic:
simp_rw [LinearMap.IsSymmetric, ← LinearMap.adjoint_inner_left, ← toLin_conjTranspose]

Premises used: Matrix.toLin_conjTranspose, LinearMap.adjoint_inner_left, LinearMap.IsSymmetric
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
h : A.IsHermitian
x x_1 : E
rw rw₁ :
  inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) x_1 =
    inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) x_1
⊢ inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) x_1 =
    inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) x_1

Tactic:
rw [h.eq]

Premises used: Matrix.IsHermitian.eq
-- Module: Mathlib.Analysis.Matrix.Hermitian
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
refine :
  ∀
    (h :
      ∀ (x y : E),
        inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
          inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y),
    A.IsHermitian
⊢ (∀ (x y : E),
      inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
        inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y) ↔
    A.IsHermitian

Tactic:
refine ⟨fun h ↦ ?_, fun h _ _ ↦ by rw [h.eq]⟩