awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
refine :
  Eq (α := Prod.{u_2, u_4} 𝕜 (WeakBilin B) → (y : F) → 𝕜)
    (fun (x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦
      HSMul.hSMul (β := (y : F) → 𝕜) x.1
        (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x))
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)

Tactic:
refine cast (congr_arg _ ?_) (continuous_fst.smul ((coeFn_continuous B).comp continuous_snd))

Premises used: Continuous.comp, cast, continuous_snd, continuous_fst, congr_arg, Continuous.smul, WeakBilin.coeFn_continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
h :
  ∀ (x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) (x_1 : F),
    HSMul.hSMul (β := (y : F) → 𝕜) x.1
        (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x)
        x_1 =
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
          fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
        x x_1
⊢ Eq (α := Prod.{u_2, u_4} 𝕜 (WeakBilin B) → (y : F) → 𝕜)
    (fun (x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦
      HSMul.hSMul (β := (y : F) → 𝕜) x.1
        (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x))
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
      fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousSMul 𝕜 𝕜
x : Prod.{u_2, u_4} 𝕜 (WeakBilin B)
x_1 : F
⊢ HSMul.hSMul (β := (y : F) → 𝕜) x.1
      (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘ Prod.snd) x)
      x_1 =
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (p : Prod.{u_2, u_4} 𝕜 (WeakBilin B)) ↦ p.1 • p.2)
      x x_1

Tactic:
simp only [Function.comp_apply, Pi.smul_apply, map_smulₛₗ, RingHom.id_apply, LinearMap.smul_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply, MulActionSemiHomClass.map_smulₛₗ, Function.comp_apply, Pi.smul_apply
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
f : F
⊢ Continuous[instTopologicalSpace B, inst]
    (AddHom.toFun (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜) ((B.flip : (a : F) → E →ₗ[𝕜] 𝕜) f)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
x x_1 : F
h :
  ∀ (x_2 : WeakBilin B),
    Eq.{u_2 + 1} (α := 𝕜)
      (({ toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x + x_1), cont := ⋯ } : (a : WeakBilin B) → 𝕜) x_2 : 𝕜)
      ((HAdd.hAdd (α := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B))
              { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x, cont := ⋯ :
                ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
              { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
                ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 } :
            (a : WeakBilin B) → 𝕜)
          x_2 :
        𝕜)
⊢ { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x + x_1), cont := ⋯ } =
    HAdd.hAdd (α := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B))
      { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x, cont := ⋯ :
        ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
      { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
        ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
x x_1 : F
x_2 : WeakBilin B
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (({ toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x + x_1), cont := ⋯ } : (a : WeakBilin B) → 𝕜) x_2 : 𝕜)
    ((HAdd.hAdd (α := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B))
            { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x, cont := ⋯ :
              ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }
            { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
              ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 } :
          (a : WeakBilin B) → 𝕜)
        x_2 :
      𝕜)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
x : 𝕜
x_1 : F
h :
  ∀ (x_2 : WeakBilin B),
    Eq.{u_2 + 1} (α := 𝕜)
      (({ toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x • x_1), cont := ⋯ } : (a : WeakBilin B) → 𝕜) x_2 : 𝕜)
      ((HSMul.hSMul (α := 𝕜) (β := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
              { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
                ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 } :
            (a : WeakBilin B) → 𝕜)
          x_2 :
        𝕜)
⊢ { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x • x_1), cont := ⋯ } =
    HSMul.hSMul (α := 𝕜) (β := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
        ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 }

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommSemiring 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : ContinuousConstSMul 𝕜 𝕜
x : 𝕜
x_1 : F
x_2 : WeakBilin B
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (({ toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) (x • x_1), cont := ⋯ } : (a : WeakBilin B) → 𝕜) x_2 : 𝕜)
    ((HSMul.hSMul (α := 𝕜) (β := StrongDual.{u_2, u_4} 𝕜 (WeakBilin B)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
            { toLinearMap := (B.flip : (a : F) → E →ₗ[𝕜] 𝕜) x_1, cont := ⋯ :
              ContinuousLinearMap.{u_2, u_2, u_4, u_2} (RingHom.id 𝕜) (WeakBilin B) 𝕜 } :
          (a : WeakBilin B) → 𝕜)
        x_2 :
      𝕜)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ ContinuousAdd.{u_4} (WeakBilin B)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
⊢ Continuous[instTopologicalSpace B, instTopologicalSpace B] fun (a : WeakBilin B) ↦ -a

Tactic:
continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => ?_)

Premises used: Iff.mpr, continuous_pi_iff, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
refine :
  ∀ (y : F),
    Continuous[instTopologicalSpace B, inst] fun (a : WeakBilin B) ↦
      ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
          fun (a : WeakBilin B) ↦ -a)
        a y
⊢ Continuous[instTopologicalSpace B, instTopologicalSpace B] fun (a : WeakBilin B) ↦ -a

Tactic:
refine continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => ?_)

Premises used: Iff.mpr, continuous_pi_iff, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
y : F
⊢ Continuous[instTopologicalSpace B, inst] fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y

Tactic:
cast (congr_arg _ ?_) (eval_continuous B (-y))

Premises used: cast, congr_arg, WeakBilin.eval_continuous, Neg.neg
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
y : F
refine :
  Eq (α := (a : WeakBilin B) → 𝕜)
    (fun (x : WeakBilin B) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y)) fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y
⊢ Continuous[instTopologicalSpace B, inst] fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y

Tactic:
refine cast (congr_arg _ ?_) (eval_continuous B (-y))

Premises used: cast, congr_arg, WeakBilin.eval_continuous, Neg.neg
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
y : F
h :
  ∀ (x : WeakBilin B),
    Eq.{u_2 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y) : 𝕜)
      (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
            fun (a : WeakBilin B) ↦ -a)
          x y :
        𝕜)
⊢ Eq (α := (a : WeakBilin B) → 𝕜)
    (fun (x : WeakBilin B) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y)) fun (a : WeakBilin B) ↦
    ((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
        fun (a : WeakBilin B) ↦ -a)
      a y

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : TopologicalSpace 𝕜
inst_1 : CommRing 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst_6 : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ Eq.{u_2 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (-y) : 𝕜)
    (((fun (x : WeakBilin B) (y : F) ↦ (((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y) ∘
          fun (a : WeakBilin B) ↦ -a)
        x y :
      𝕜)

Tactic:
simp only [map_neg, Function.comp_apply, LinearMap.neg_apply]

Premises used: LinearMap.neg_apply, map_neg, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
M : Type u_6
inst_7 : Monoid M
inst_8 : DistribMulAction M 𝕜
inst_9 : SMulCommClass 𝕜 M 𝕜
inst_10 : ContinuousConstSMul M 𝕜
⊢ ContinuousConstSMul M (WeakDual 𝕜 E)

Tactic:
⟨fun m =>
    continuous_induced_rng.2 <| (WeakBilin.coeFn_continuous (topDualPairing 𝕜 E)).const_smul m⟩

Premises used: Iff.mpr, ContinuousConstSMul.mk, topDualPairing, WeakBilin.coeFn_continuous, Continuous.const_smul, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
M : Type u_6
inst_7 : Monoid M
inst_8 : DistribMulAction M 𝕜
inst_9 : SMulCommClass 𝕜 M 𝕜
inst_10 : TopologicalSpace M
inst_11 : ContinuousSMul M 𝕜
⊢ ContinuousSMul M (WeakDual 𝕜 E)

Tactic:
⟨continuous_induced_rng.2 <|
      continuous_fst.smul ((WeakBilin.coeFn_continuous (topDualPairing 𝕜 E)).comp continuous_snd)⟩

Premises used: Iff.mpr, Continuous.comp, continuous_snd, continuous_fst, Continuous.smul, topDualPairing, WeakBilin.coeFn_continuous, ContinuousSMul.mk, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x' : StrongDual 𝕜 E
⊢ Eq (α := (a : E) → 𝕜) (⇑((toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) x' : WeakDual 𝕜 E) : (a : E) → 𝕜)
    (⇑x' : (a : E) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x' : StrongDual 𝕜 E
y : E
⊢ Eq.{u_2 + 1} (α := 𝕜) ((((toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) x' : WeakDual 𝕜 E) : (a : E) → 𝕜) y : 𝕜)
    ((x' : (a : E) → 𝕜) y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x' y' : StrongDual 𝕜 E
⊢ Eq (α := WeakDual 𝕜 E) ((toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) x' : WeakDual 𝕜 E)
      ((toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) y' : WeakDual 𝕜 E) ↔
    x' = y'

Tactic:
(LinearEquiv.injective toWeakDual).eq_iff

Premises used: StrongDual.toWeakDual, Function.Injective.eq_iff, LinearEquiv.injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x : WeakDual 𝕜 E
y : E
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E) : (a : E) → 𝕜) y : 𝕜)
    ((x : (a : E) → 𝕜) y : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x' : WeakDual 𝕜 E
⊢ Eq (α := (a : E) → 𝕜) (⇑((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) x' : StrongDual 𝕜 E) : (a : E) → 𝕜)
    (⇑x' : (a : E) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
x' y' : WeakDual 𝕜 E
⊢ Eq (α := StrongDual 𝕜 E) ((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) x' : StrongDual 𝕜 E)
      ((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) y' : StrongDual 𝕜 E) ↔
    x' = y'

Tactic:
(LinearEquiv.injective toStrongDual).eq_iff

Premises used: Function.Injective.eq_iff, WeakDual.toStrongDual, LinearEquiv.injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
⊢ Continuous[_, Pi.topologicalSpace] fun (x : WeakDual 𝕜 E) (y : E) ↦ (x : (a : E) → 𝕜) y

Tactic:
continuous_induced_dom

Premises used: WeakDual, continuous_induced_dom
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
y : E
⊢ Continuous[_, inst_1] fun (x : WeakDual 𝕜 E) ↦ (x : (a : E) → 𝕜) y

Tactic:
continuous_pi_iff.mp coeFn_continuous y

Premises used: WeakDual.coeFn_continuous, continuous_pi_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace α
g : α → WeakDual 𝕜 E
h : ∀ (y : E), Continuous[inst_7, inst_1] fun (a : α) ↦ (g a : (a : E) → 𝕜) y
⊢ Continuous[inst_7, _] g

Tactic:
continuous_induced_rng.2 (continuous_pi_iff.mpr h)

Premises used: Iff.mpr, continuous_pi_iff, WeakDual, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space 𝕜
⊢ T2Space (WeakDual 𝕜 E)

Tactic:
(WeakBilin.isEmbedding ContinuousLinearMap.coe_injective).t2Space

Premises used: WeakBilin.isEmbedding, WeakDual, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommRing 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : IsTopologicalAddGroup 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : IsTopologicalAddGroup E
⊢ IsTopologicalAddGroup (WeakDual 𝕜 E)

Tactic:
WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E)

Premises used: instAddCommMonoidWeakDual._aux_1, instAddCommMonoidWeakBilin._aux_1, instAddCommMonoidWeakBilin._aux_4, topDualPairing, WeakBilin, WeakDual, WeakBilin.instIsTopologicalAddGroup, instAddCommMonoidWeakDual._aux_2
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : CommSemiring 𝕝
inst_8 : Module 𝕝 𝕜
inst_9 : Module 𝕝 E
inst_10 : IsScalarTower 𝕝 𝕜 E
⊢ IsScalarTower.{u_3, u_2, u_4} 𝕝 𝕜 (WeakSpace 𝕜 E)

Tactic:
WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip

Premises used: instModuleWeakBilin._aux_1, WeakBilin.instIsScalarTower, WeakSpace.instModule'._aux_1, topDualPairing, LinearMap.flip, WeakSpace
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul.{u_2, u_4} 𝕜 (WeakSpace 𝕜 E)

Tactic:
WeakBilin.instContinuousSMul _

Premises used: instModuleWeakBilin._aux_1, WeakBilin.instContinuousSMul, WeakSpace.instModule'._aux_1, WeakSpace
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : AddCommMonoid F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
f : E →L[𝕜] F
x : E
⊢ Eq.{u_5 + 1} (α := WeakSpace 𝕜 F)
    (((map f : ContinuousLinearMap.{u_2, u_2, u_4, u_5} (RingHom.id 𝕜) (WeakSpace 𝕜 E) (WeakSpace 𝕜 F)) :
          (a : WeakSpace 𝕜 E) → WeakSpace 𝕜 F)
        x :
      WeakSpace 𝕜 F)
    ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
𝕜 : Type u_2
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : AddCommMonoid F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
f : E →L[𝕜] F
⊢ Eq (α := (a : WeakSpace 𝕜 E) → WeakSpace 𝕜 F) (⇑(map f) : (a : WeakSpace 𝕜 E) → WeakSpace 𝕜 F) (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.WeakDual
Goal:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : AddCommMonoid E
inst_5 : Module 𝕜 E
inst_6 : TopologicalSpace E
h :
  ∀ (y : E →L[𝕜] 𝕜),
    Continuous[inst_6, inst_1] fun (a : E) ↦
      (((LinearMap.flip (topDualPairing 𝕜 E) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
              (AddHom.toFun (LinearMap.toAddHom (↑(toWeakSpace 𝕜 E) : E →ₗ[𝕜] WeakSpace 𝕜 E)) a) :
            (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) :
          (a : E →L[𝕜] 𝕜) → 𝕜)
        y
⊢ Continuous[inst_6, _] (AddHom.toFun (LinearMap.toAddHom (↑(toWeakSpace 𝕜 E) : E →ₗ[𝕜] WeakSpace 𝕜 E)))

Tactic:
apply WeakBilin.continuous_of_continuous_eval

Premises used: WeakBilin.continuous_of_continuous_eval