awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ContinuousSMul 𝕜 E
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)
have this : CompleteSpace (ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (i : ι) ↦ E) F)
Tactic: have := ContinuousMultilinearMap.completeSpace (F := F) h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ContinuousSMul 𝕜 E
h : IsCoherentWith (X := ι → E) {s : Set (ι → E) | IsVonNBounded 𝕜 s}
F : Type u_3
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
this : CompleteSpace (ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (i : ι) ↦ E) F)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)
have rw : IsComplete (α := ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) (range toContinuousMultilinearMap)
Tactic: rw [completeSpace_iff_isComplete_range
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
𝕜' : Type u_5
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra 𝕜' 𝕜
inst_10 : Module 𝕜' E
inst_11 : IsScalarTower 𝕜' 𝕜 E
inst_12 : Module 𝕜' F
inst_13 : IsScalarTower 𝕜' 𝕜 F
inst_14 : ContinuousSMul 𝕜 E
⊢ IsUniformEmbedding (α := E [⋀^ι]→L[𝕜] F) (β := E [⋀^ι]→L[𝕜'] F) (restrictScalars 𝕜')
have rw : IsUniformEmbedding (α := E [⋀^ι]→L[𝕜] F) (β := ContinuousMultilinearMap.{u_5, u_4, u_2, u_3} 𝕜' (fun (x : ι) ↦ E) F)
  (toContinuousMultilinearMap ∘ restrictScalars 𝕜')
Tactic: rw [← isUniformEmbedding_toContinuousMultilinearMap.of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
ι' : Type u_5
p : ι' → Prop
b : ι' → Set F
h : Filter.HasBasis (𝓝 0) p b
⊢ Filter.HasBasis (α := E [⋀^ι]→L[𝕜] F) (𝓝 0) (fun (Si : Set (ι → E) × ι') ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2)
    fun (Si : Set (ι → E) × ι') ↦ {f : E [⋀^ι]→L[𝕜] F | MapsTo (⇑f : (a : ι → E) → F) Si.1 (b Si.2)}
have rw : Filter.HasBasis (α := E [⋀^ι]→L[𝕜] F) (Filter.comap toContinuousMultilinearMap (𝓝 (toContinuousMultilinearMap 0)))
  (fun (Si : Set (ι → E) × ι') ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set (ι → E) × ι') ↦
  {f : E [⋀^ι]→L[𝕜] F | MapsTo (⇑f : (a : ι → E) → F) Si.1 (b Si.2)}
Tactic: rw [nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x x_1 : G
⊢ { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x + x_1),
      map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } =
    { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x,
        map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } +
      { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
        map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F }
have H : ∀ (x_2 : ι → E),
  Eq.{u_3 + 1} (α := F)
    (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x + x_1),
            map_eq_zero_of_eq' := sorry : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)
    (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x,
              map_eq_zero_of_eq' := sorry : E [⋀^ι]→L[𝕜] F } +
            { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
              map_eq_zero_of_eq' := sorry : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F
hf :
  ∀ (x : G) (v : (i : ι) → E) (i j : ι),
    v i = v j →
      i ≠ j →
        Eq.{u_3 + 1} (α := F)
          ((((f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x :
                  ContinuousMultilinearMap.{u_1, u_4, u_2, u_3} 𝕜 (fun (x : ι) ↦ E) F) :
                (a : (i : ι) → E) → F)
              v :
            F)
          (0 : F)
x : 𝕜
x_1 : G
⊢ { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x • x_1),
      map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F } =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
        map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→L[𝕜] F }
have H : ∀ (x_2 : ι → E),
  Eq.{u_3 + 1} (α := F)
    (({ toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) (x • x_1),
            map_eq_zero_of_eq' := sorry : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
            { toContinuousMultilinearMap := (f : (a : G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) F) x_1,
              map_eq_zero_of_eq' := sorry : E [⋀^ι]→L[𝕜] F } :
          (a : ι → E) → F)
        x_2 :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : Module 𝕜 G
inst_10 : TopologicalSpace G
inst_11 : ContinuousConstSMul 𝕜 F
E' : Type u_6
inst_12 : AddCommGroup E'
inst_13 : Module 𝕜 E'
inst_14 : TopologicalSpace E'
f : E →L[𝕜] E'
⊢ Continuous[instTopologicalSpace, instTopologicalSpace]
    (AddHom.toFun (LinearMap.toAddHom (compContinuousLinearMapₗ f)))
have rw : Continuous[instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
  (toContinuousMultilinearMap ∘ AddHom.toFun (LinearMap.toAddHom (compContinuousLinearMapₗ f)))
Tactic: rw [isEmbedding_toContinuousMultilinearMap.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
g : F →L[𝕜] G
⊢ Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousAlternatingMap.instTopologicalSpace]
    (AddHom.toFun
      (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
        ((compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g)))
have rw : Continuous[ContinuousAlternatingMap.instTopologicalSpace, ContinuousMultilinearMap.instTopologicalSpace]
  (ContinuousAlternatingMap.toContinuousMultilinearMap ∘
    AddHom.toFun
      (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
        ((compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g)))
Tactic: rw [ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
x x_1 : F →L[𝕜] G
⊢ (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) (x + x_1);
    { toLinearMap := __LinearMap, cont := ⋯ }) =
    HAdd.hAdd (α := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
      (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x;
      { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
      (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
      { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
have h : ∀ (x_2 : E [⋀^ι]→L[𝕜] F) (x_3 : ι → E),
  Eq.{u_4 + 1} (α := G)
    ((((let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                  (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                    (x + x_1);
                { toLinearMap := __LinearMap, cont := sorry } :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)
    ((((HAdd.hAdd (α := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
                  (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x;
                  { toLinearMap := __LinearMap, cont := sorry : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
                  (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
                  { toLinearMap := __LinearMap, cont := sorry : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G }) :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
x : 𝕜
x_1 : F →L[𝕜] G
⊢ (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) (x • x_1);
    { toLinearMap := __LinearMap, cont := ⋯ }) =
    HSMul.hSMul (α := 𝕜) (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
        (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
      { toLinearMap := __LinearMap, cont := ⋯ : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G })
have h : ∀ (x_2 : E [⋀^ι]→L[𝕜] F) (x_3 : ι → E),
  Eq.{u_4 + 1} (α := G)
    ((((let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                  (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G)
                    (x • x_1);
                { toLinearMap := __LinearMap, cont := sorry } :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)
    ((((HSMul.hSMul (α := 𝕜) (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                  (let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
                    (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) x_1;
                  { toLinearMap := __LinearMap, cont := sorry : E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G }) :
                (a : E [⋀^ι]→L[𝕜] F) → E [⋀^ι]→L[𝕜] G)
              x_2 :
            E [⋀^ι]→L[𝕜] G) :
          (a : ι → E) → G)
        x_3 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Topology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : AddCommGroup G
inst_11 : Module 𝕜 G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : ContinuousConstSMul 𝕜 G
⊢ Continuous[topologicalSpace, topologicalSpace] fun (g : F →L[𝕜] G) ↦
    let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g;
    { toLinearMap := __LinearMap, cont := ⋯ }
have rw : Continuous[topologicalSpace, topologicalSpace]
  (Function.comp (β := E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G)
    (comp (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)) fun (g : F →L[𝕜] G) ↦
    let __LinearMap : E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G :=
      (compContinuousAlternatingMapₗ 𝕜 E F G : (a : F →L[𝕜] G) → E [⋀^ι]→L[𝕜] F →ₗ[𝕜] E [⋀^ι]→L[𝕜] G) g;
    { toLinearMap := __LinearMap, cont := sorry })
Tactic: rw [ContinuousLinearMap.isEmbedding_postcomp
      (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)
      ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap |>.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : R × M) ↦ p.1 • p.2
have hmul₁ : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
Tactic: rw [← nhds_prod_eq] at hmul
Cleared hypotheses: hmul, hmulleft, hmulright
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : R × M) ↦ p.1 • p.2
have refine_1 : ContinuousAt (Y := M)
  (fun (x : R × M) ↦
    ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x.1 : M →+ M) : (a : M) → M) x.2)
  (0, 0)
Tactic: refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
refine_1 :
  ContinuousAt (Y := M)
    (fun (x : R × M) ↦
      ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x.1 : M →+ M) : (a : M) → M) x.2)
    (0, 0)
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : R × M) ↦ p.1 • p.2
have refine_2 : ∀ (x : R),
  ContinuousAt.{u_2, u_2} (X := M) (Y := M)
    (⇑(((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) 0
Tactic: refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTopologicalRing R
inst_6 : IsTopologicalAddGroup M
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
refine_1 :
  ContinuousAt (Y := M)
    (fun (x : R × M) ↦
      ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x.1 : M →+ M) : (a : M) → M) x.2)
    (0, 0)
refine_2 :
  ∀ (x : R),
    ContinuousAt.{u_2, u_2} (X := M) (Y := M)
      (⇑(((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) 0
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : R × M) ↦ p.1 • p.2
have refine_3 : ∀ (y : M),
  ContinuousAt.{u_1, u_2} (Y := M)
    (fun (x : R) ↦
      ((((AddMonoidHom.smul : AddMonoidHom.{u_1, u_2} R (M →+ M)) : (a : R) → M →+ M) x : M →+ M) : (a : M) → M) y)
    0
Tactic: refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
hs : (interior (↑s : Set M)).Nonempty
⊢ s = ⊤
have rcases : ∀ (y : M) (hy : y ∈ interior (↑s : Set M)), s = ⊤
Tactic: rcases hs with ⟨y, hy⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : y ∈ interior (↑s : Set M)
⊢ s = ⊤
have refine : ∀ (x : M), x ∈ s
Tactic: refine Submodule.eq_top_iff'.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : y ∈ interior (↑s : Set M)
x : M
⊢ x ∈ s
have rw : ∀ (hy : (↑s : Set M) ∈ 𝓝 y) (x : M), x ∈ s
Tactic: rw [mem_interior_iff_mem_nhds] at hy
Cleared hypotheses: hy, x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
⊢ x ∈ s
have this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 (y + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 x))
Tactic: have : Tendsto (fun c : R => y + c • x) (𝓝[{ x : R | IsUnit x }] 0) (𝓝 (y + (0 : R) • x)) :=
    tendsto_const_nhds.add ((tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).smul tendsto_const_nhds)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 (y + HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 x))
⊢ x ∈ s
have this₁ : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
Tactic: rw [zero_smul, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
⊢ x ∈ s
have obtain : ∀ (u : Rˣ) (hu : y + (↑u : R) • x ∈ s), x ∈ s
Tactic: obtain ⟨_, hu : y + _ • _ ∈ s, u, rfl⟩ :=
    nonempty_of_mem (inter_mem (Filter.mem_map.1 (this hy)) self_mem_nhdsWithin)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : ContinuousAdd M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : NeBot.{u_1} (α := R) (𝓝[{x : R | IsUnit x}] 0)
s : Submodule R M
y : M
hy : (↑s : Set M) ∈ 𝓝 y
x : M
this : Tendsto (fun (c : R) ↦ y + c • x) (𝓝[{x : R | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : y + (↑u : R) • x ∈ s
⊢ x ∈ s
have hy' : y ∈ s
Tactic: have hy' : y ∈ ↑s := mem_of_mem_nhds hy