awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
h :
  ∀ (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
    Eq.{u_1 + 1} (α := 𝕜)
      (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 1,
              continuous_toFun := ⋯ } :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a :
        𝕜)
      ((1 : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜) a : 𝕜)
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 1, continuous_toFun := ⋯ } 1

Tactic:
ext a
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 1, continuous_toFun := ⋯ } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
    ((1 : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜) a : 𝕜)

Tactic:
simp only [coe_mk, coe_one, Pi.one_apply, map_one a]

Premises used: Pi.one_apply, map_one, ContinuousMap.coe_mk, ContinuousMap.coe_one
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a b : A
h :
  ∀ (a_1 : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
    Eq.{u_1 + 1} (α := 𝕜)
      (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a * b),
              continuous_toFun := ⋯ } :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a_1 :
        𝕜)
      ((HMul.hMul (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
              { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a,
                continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
              { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b,
                continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) } :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a_1 :
        𝕜)
⊢ { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a * b),
      continuous_toFun := ⋯ } =
    HMul.hMul (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a b : A
a_1 : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a * b),
            continuous_toFun := ⋯ } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)
    ((HMul.hMul (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a,
              continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b,
              continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)

Tactic:
simp only [map_mul, coe_mk, coe_mul, Pi.mul_apply]

Premises used: Pi.mul_apply, map_mul, ContinuousMap.coe_mk, ContinuousMap.coe_mul
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
h :
  ∀ (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
    Eq.{u_1 + 1} (α := 𝕜)
      (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 0,
              continuous_toFun := ⋯ } :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a :
        𝕜)
      ((0 : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜) a : 𝕜)
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 0, continuous_toFun := ⋯ } 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) 0, continuous_toFun := ⋯ } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
    ((0 : (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜) a : 𝕜)

Tactic:
simp only [map_zero, coe_mk, coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, map_zero, ContinuousMap.coe_zero, ContinuousMap.coe_mk
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a b : A
h :
  ∀ (a_1 : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
    Eq.{u_1 + 1} (α := 𝕜)
      (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a + b),
              continuous_toFun := ⋯ } :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a_1 :
        𝕜)
      ((HAdd.hAdd (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
              { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a,
                continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
              { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b,
                continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) } :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a_1 :
        𝕜)
⊢ { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a + b),
      continuous_toFun := ⋯ } =
    HAdd.hAdd (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
      { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b, continuous_toFun := ⋯ :
        C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
a b : A
a_1 : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (({ toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) (a + b),
            continuous_toFun := ⋯ } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)
    ((HAdd.hAdd (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) a,
              continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) }
            { toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ (φ : (a : A) → 𝕜) b,
              continuous_toFun := ⋯ : C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) } :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a_1 :
      𝕜)

Tactic:
simp only [map_add, coe_mk, coe_add, Pi.add_apply]

Premises used: map_add, Pi.add_apply, ContinuousMap.coe_add, ContinuousMap.coe_mk
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
k : 𝕜
h :
  ∀ (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))),
    Eq.{u_1 + 1} (α := 𝕜)
      ((({
                toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦
                  (φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A),
                continuous_toFun := ⋯ } :
              C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜)) :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a :
        𝕜)
      ((((algebraMap 𝕜 C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) :
                  (a : 𝕜) → C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
                k :
              C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜)) :
            (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
          a :
        𝕜)
⊢ Eq (α := C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    ({
        toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦
          (φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A),
        continuous_toFun := ⋯ } :
      C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
    ((algebraMap 𝕜 C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) :
          (a : 𝕜) → C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
        k :
      C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : IsTopologicalRing 𝕜
inst_4 : TopologicalSpace A
inst_5 : Semiring A
inst_6 : Algebra 𝕜 A
k : 𝕜
a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((({
              toFun := fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦
                (φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) k : A),
              continuous_toFun := ⋯ } :
            C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜)) :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)
    ((((algebraMap 𝕜 C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜) :
                (a : 𝕜) → C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜))
              k :
            C((↑(characterSpace 𝕜 A) : Type (max u_1 u_2)), 𝕜)) :
          (a : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) → 𝕜)
        a :
      𝕜)

Tactic:
simp [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : RingHomSurjective σ
inst_11 : RingHomIsometric σ
inst_12 : TopologicalSpace E
inst_13 : IsTopologicalAddGroup E
inst_14 : TopologicalSpace F
inst_15 : IsTopologicalAddGroup F
inst_16 : ContinuousSMul 𝕜₁ E
inst_17 : ContinuousSMul 𝕜₂ F
⊢ ContinuousSMul 𝕜₂ (E →SL_c[σ] F)

Tactic:
UniformConvergenceCLM.continuousSMul σ F { S | IsCompact S }
    (fun _ hs => hs.isVonNBounded 𝕜₁)

Premises used: setOf, UniformConvergenceCLM.continuousSMul, IsCompact.isVonNBounded, IsCompact
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
⊢ ContinuousEvalConst (E →SL_c[σ] F) E F

Tactic:
UniformConvergenceCLM.continuousEvalConst σ F _ sUnion_isCompact_eq_univ

Premises used: UniformConvergenceCLM.continuousEvalConst, Set.sUnion_isCompact_eq_univ
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_3 : RingHomCompTriple σ τ ρ
E : Type u_4
F : Type u_5
G : Type u_6
inst_4 : AddCommGroup E
inst_5 : Module 𝕜₁ E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : T2Space F
⊢ T2Space (E →SL_c[σ] F)

Tactic:
UniformConvergenceCLM.t2Space σ F _ sUnion_isCompact_eq_univ

Premises used: UniformConvergenceCLM.t2Space, Set.sUnion_isCompact_eq_univ
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_7
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
⊢ HasBasis (α := E →SL_c[σ] F) (𝓝 0) (fun (Si : Prod.{u_4, u_7} (Set E) ι) ↦ IsCompact Si.1 ∧ p Si.2)
    fun (Si : Prod.{u_4, u_7} (Set E) ι) ↦
    {f : E →SL_c[σ] F | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}

Tactic:
UniformConvergenceCLM.hasBasis_nhds_zero_of_basis σ F { S | IsCompact S }
    ⟨∅, isCompact_empty⟩
    (directedOn_of_sup_mem fun _ _ => IsCompact.union) h

Premises used: Set.Mem, setOf, directedOn_of_sup_mem, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, Exists.intro, IsCompact.union, EmptyCollection.emptyCollection, IsCompact, isCompact_empty
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_4
F : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
⊢ HasBasis (α := E →SL_c[σ] F) (𝓝 0)
    (fun (SV : Prod.{u_4, u_5} (Set E) (Set F)) ↦ IsCompact SV.1 ∧ Membership.mem (γ := Filter F) (𝓝 0) SV.2)
    fun (SV : Prod.{u_4, u_5} (Set E) (Set F)) ↦
    {f : E →SL_c[σ] F | ∀ x ∈ SV.1, Membership.mem (α := F) SV.2 ((f : (a : E) → F) x : F)}

Tactic:
CompactConvergenceCLM.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets

Premises used: CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, Set.Mem, setOf, nhds, Filter.basis_sets, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
inst : NormedField 𝕜₁
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module 𝕜₁ E
inst_3 : TopologicalSpace E
ι : Type u_7
F : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (F i)
inst_5 : (i : ι) → Module.{u_1, u_8} 𝕜₁ (F i)
inst_6 : (i : ι) → TopologicalSpace (F i)
inst_7 : ∀ (i : ι), IsTopologicalAddGroup.{u_8} (F i)
inst_8 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_8} 𝕜₁ (F i)
T : (i : ι) → CompactConvergenceCLM.{u_1, u_1, u_4, u_8} (RingHom.id 𝕜₁) E (F i)
e : E
i : ι
⊢ Eq.{u_8 + 1} (α := F i)
    ((((piEquivL 𝕜₁ E F : (a : (i : ι) → E →L_c[𝕜₁] F i) → E →L_c[𝕜₁] (i : ι) → F i) T : E →L_c[𝕜₁] (i : ι) → F i) :
          (a : E) → (i : ι) → F i)
        e i :
      F i)
    ((T i : (a : E) → F i) e : F i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
inst : NormedField 𝕜₁
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module 𝕜₁ E
inst_3 : TopologicalSpace E
ι : Type u_7
F : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (F i)
inst_5 : (i : ι) → Module.{u_1, u_8} 𝕜₁ (F i)
inst_6 : (i : ι) → TopologicalSpace (F i)
inst_7 : ∀ (i : ι), IsTopologicalAddGroup.{u_8} (F i)
inst_8 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_8} 𝕜₁ (F i)
T : E →L_c[𝕜₁] (i : ι) → F i
e : E
i : ι
⊢ Eq.{u_8 + 1} (α := F i)
    ((((ContinuousLinearEquiv.symm (piEquivL 𝕜₁ E F) : (a : E →L_c[𝕜₁] (i : ι) → F i) → (i : ι) → E →L_c[𝕜₁] F i) T i :
            CompactConvergenceCLM.{u_1, u_1, u_4, u_8} (RingHom.id 𝕜₁) E (F i)) :
          (a : E) → F i)
        e :
      F i)
    ((T : (a : E) → (i : ι) → F i) e i : F i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂_1 : Type u_2
𝕜₃_1 : Type u_3
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂_1
inst_2 : NormedField 𝕜₃_1
σ : 𝕜₁ →+* 𝕜₂_1
τ : 𝕜₂_1 →+* 𝕜₃_1
ρ : 𝕜₁ →+* 𝕜₃_1
inst_3 : RingHomCompTriple σ τ ρ
E_1 : Type u_4
F_1 : Type u_5
G_1 : Type u_6
inst_4 : AddCommGroup E_1
inst_5 : Module 𝕜₁ E_1
inst_6 : AddCommGroup F_1
inst_7 : Module 𝕜₂_1 F_1
inst_8 : AddCommGroup G_1
inst_9 : Module 𝕜₃_1 G_1
𝕜 : Type u_7
𝕜₂ : Type u_8
𝕜₃ : Type u_9
𝕜₄ : Type u_10
E : Type u_11
F : Type u_12
G : Type u_13
H : Type u_14
inst_10 : AddCommGroup E
inst_11 : AddCommGroup F
inst_12 : AddCommGroup G
inst_13 : AddCommGroup H
inst_14 : NormedField 𝕜
inst_15 : NormedField 𝕜₂
inst_16 : NormedField 𝕜₃
inst_17 : NormedField 𝕜₄
inst_18 : Module 𝕜 E
inst_19 : Module 𝕜₂ F
inst_20 : Module 𝕜₃ G
inst_21 : Module 𝕜₄ H
inst_22 : TopologicalSpace E
inst_23 : TopologicalSpace F
inst_24 : TopologicalSpace G
inst_25 : TopologicalSpace H
inst_26 : IsTopologicalAddGroup G
inst_27 : IsTopologicalAddGroup H
inst_28 : ContinuousConstSMul 𝕜₃ G
inst_29 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_30 : RingHomInvPair σ₁₂ σ₂₁
inst_31 : RingHomInvPair σ₂₁ σ₁₂
inst_32 : RingHomInvPair σ₃₄ σ₄₃
inst_33 : RingHomInvPair σ₄₃ σ₃₄
inst_34 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_35 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_36 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_37 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_38 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_39 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
s : Set F
⊢ Membership.mem (γ := Set (Set F)) {S : Set F | IsCompact S} s ↔
    Membership.mem (γ := Set (Set E)) {S : Set E | IsCompact S} ((⇑e₁₂ : (a : E) → F) ⁻¹' s)

Tactic:
simp [← e₁₂.toHomeomorph.isCompact_preimage]

Premises used: Homeomorph.isCompact_preimage, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜 : Type u_7
𝕜₂ : Type u_8
𝕜₃ : Type u_9
𝕜₄ : Type u_10
E : Type u_11
F : Type u_12
G : Type u_13
H : Type u_14
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : NormedField 𝕜₂
inst_6 : NormedField 𝕜₃
inst_7 : NormedField 𝕜₄
inst_8 : Module 𝕜 E
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₃ G
inst_11 : Module 𝕜₄ H
inst_12 : TopologicalSpace E
inst_13 : TopologicalSpace F
inst_14 : TopologicalSpace G
inst_15 : TopologicalSpace H
inst_16 : IsTopologicalAddGroup G
inst_17 : IsTopologicalAddGroup H
inst_18 : ContinuousConstSMul 𝕜₃ G
inst_19 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_20 : RingHomInvPair σ₁₂ σ₂₁
inst_21 : RingHomInvPair σ₂₁ σ₁₂
inst_22 : RingHomInvPair σ₃₄ σ₄₃
inst_23 : RingHomInvPair σ₄₃ σ₃₄
inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
φ : E →SL_c[σ₁₄] H
f : F
⊢ Eq.{u_13 + 1} (α := G)
    ((((e₁₂.compactConvergenceCLMCongrSL e₄₃ : (a : E →SL_c[σ₁₄] H) → F →SL_c[σ₂₃] G) φ : F →SL_c[σ₂₃] G) : (a : F) → G)
        f :
      G)
    ((e₄₃ : (a : H) → G) ((φ : (a : E) → H) ((e₁₂.symm : (a : F) → E) f : E) : H) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜 : Type u_7
𝕜₂ : Type u_8
𝕜₃ : Type u_9
𝕜₄ : Type u_10
E : Type u_11
F : Type u_12
G : Type u_13
H : Type u_14
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : NormedField 𝕜₂
inst_6 : NormedField 𝕜₃
inst_7 : NormedField 𝕜₄
inst_8 : Module 𝕜 E
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₃ G
inst_11 : Module 𝕜₄ H
inst_12 : TopologicalSpace E
inst_13 : TopologicalSpace F
inst_14 : TopologicalSpace G
inst_15 : TopologicalSpace H
inst_16 : IsTopologicalAddGroup G
inst_17 : IsTopologicalAddGroup H
inst_18 : ContinuousConstSMul 𝕜₃ G
inst_19 : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst_20 : RingHomInvPair σ₁₂ σ₂₁
inst_21 : RingHomInvPair σ₂₁ σ₁₂
inst_22 : RingHomInvPair σ₃₄ σ₄₃
inst_23 : RingHomInvPair σ₄₃ σ₃₄
inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
φ : F →SL_c[σ₂₃] G
e : E
⊢ Eq.{u_14 + 1} (α := H)
    ((((ContinuousLinearEquiv.symm (e₁₂.compactConvergenceCLMCongrSL e₄₃) : (a : F →SL_c[σ₂₃] G) → E →SL_c[σ₁₄] H) φ :
            E →SL_c[σ₁₄] H) :
          (a : E) → H)
        e :
      H)
    ((e₄₃.symm : (a : G) → H) ((φ : (a : F) → G) ((e₁₂ : (a : E) → F) e : F) : G) : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
Goal:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
G : Type u_10
H : Type u_11
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e₁ : E ≃L[𝕜] F
e₂ : H ≃L[𝕜] G
φ : E →L_c[𝕜] H
f : F
⊢ Eq.{u_10 + 1} (α := G)
    ((((e₁.compactConvergenceCLMCongr e₂ : (a : E →L_c[𝕜] H) → F →L_c[𝕜] G) φ : F →L_c[𝕜] G) : (a : F) → G) f : G)
    ((e₂ : (a : H) → G) ((φ : (a : E) → H) ((e₁.symm : (a : F) → E) f : E) : H) : G)

Tactic:
rfl

Premises used: rfl