awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), ‖normalize x‖ = 1 ↔ x ≠ 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0
have neg : ∀ (hx : ¬x = 0), ‖normalize x‖ = 1 ↔ x ≠ 0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
⊢ normalize (normalize x) = normalize x
have pos : ∀ (hx : x = 0), normalize (normalize x) = normalize x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), normalize (normalize x) = normalize x
⊢ normalize (normalize x) = normalize x
have neg : ∀ (hx : ¬x = 0), normalize (normalize x) = normalize x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
hr : r < 0
x : V
⊢ 0 < -r
have linarith : -r ≤ 0 → r - 0 + (-r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
x : V
⊢ normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
have inl : ∀ (h_pos : 0 < r),
  normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
Tactic: rcases lt_trichotomy 0 r with (h_pos | rfl | h_neg)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
x : V
inl :
  ∀ (h_pos : 0 < r),
    normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
⊢ normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
have inr : normalize (HSMul.hSMul (α := ℝ) 0 x) =
  HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ) (normalize x)
Tactic: rcases lt_trichotomy 0 r with (h_pos | rfl | h_neg)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
x : V
inl :
  ∀ (h_pos : 0 < r),
    normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
inr :
  normalize (HSMul.hSMul (α := ℝ) 0 x) =
    HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ) (normalize x)
⊢ normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
have inr₁ : ∀ (h_neg : r < 0),
  normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
Tactic: rcases lt_trichotomy 0 r with (h_pos | rfl | h_neg)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
⊢ LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
      ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
            (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
          (a • x) ∘ₗ
        ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
      ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (a • x)) ⋯ =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
          ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
              x ∘ₗ
            ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
          ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯ :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
have h : ∀ (x_1 : ContinuousMultilinearMap 𝕜 E F),
  Eq.{uF + 1} (α := F)
    (((LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
              ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                    (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                  (a • x) ∘ₗ
                ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
              ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (a • x)) sorry :
            ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)
    ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
            (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    x ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) sorry :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ BddAbove (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)}
have h : Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
  (upperBounds
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)})
  (projectiveSeminorm (E := E))
Tactic: use projectiveSeminorm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
    (upperBounds
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)})
    (projectiveSeminorm (E := E))
have h : ∀ (x : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) (x_1 : Type (max uι u𝕜 uE)) (x_2 : SeminormedAddCommGroup x_1)
  (x_3 : NormedSpace 𝕜 x_1)
  (h :
    x =
      Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1) :
          Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1))
        (toDualContinuousMultilinearMap (E := E) x_1)),
  x ≤ projectiveSeminorm (E := E)
Tactic: simp only [mem_upperBounds, Set.mem_setOf_eq, forall_exists_index]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) (injectiveSeminorm (E := E)) (projectiveSeminorm (E := E))
have rw : LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
  (sSup
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)})
  (projectiveSeminorm (E := E))
Tactic: rw [injectiveSeminorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (sSup
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)})
    (projectiveSeminorm (E := E))
have refine_1 : Set.Nonempty (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
  {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
    ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
      p =
        Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
          (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
            Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
          (toDualContinuousMultilinearMap (E := E) G)}
Tactic: refine csSup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
refine_1 :
  Set.Nonempty (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)}
⊢ LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (sSup
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)})
    (projectiveSeminorm (E := E))
have refine_2 : ∀ (b : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)),
  Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)}
      b →
    b ≤ projectiveSeminorm (E := E)
Tactic: refine csSup_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ Set.Nonempty (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)}
have refine_1 : Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
  {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
    ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
      p =
        Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
          (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
            Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
          (toDualContinuousMultilinearMap (E := E) G)}
  0
Tactic: existsi 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
    Eq (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) 0
      (Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
        (toDualContinuousMultilinearMap (E := E) G))
have refine_1 : Eq (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) 0
  (Seminorm.comp
    (normSeminorm 𝕜
        (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
          PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
      Seminorm 𝕜
        (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
          PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
    (toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
Tactic: existsi PUnit, inferInstance, inferInstance
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ Eq (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) 0
    (Seminorm.comp
      (normSeminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
        Seminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
      (toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
have refine_1 : ∀ (x : ⨂[𝕜] (i : ι), E i),
  Eq (α := ℝ) ((0 : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x : ℝ)
    ((Seminorm.comp
            (normSeminorm 𝕜
                (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                  PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
              Seminorm 𝕜
                (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                  PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
            (toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
          (a : ⨂[𝕜] (i : ι), E i) → ℝ)
        x :
      ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ 0 =
    norm (E :=
      ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
        PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
      ((toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} :
            (a : ⨂[𝕜] (i : ι), E i) →
              ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
          x :
        ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
          PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
have refine_1 : 0 =
  norm (E :=
    ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
      PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
    0
Tactic: rw [Subsingleton.elim (toDualContinuousMultilinearMap PUnit.{(max (max uE uι) u𝕜) + 1} x) 0,
      norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
refine_1 :
  0 =
    norm (E :=
      ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
        PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
      0
⊢ 0 =
    norm (E :=
      ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
        PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
      ((toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} :
            (a : ⨂[𝕜] (i : ι), E i) →
              ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
          x :
        ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
          PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
have refine_1₁ : Eq (α := ℝ) 0 0
Tactic: rw [Subsingleton.elim (toDualContinuousMultilinearMap PUnit.{(max (max uE uι) u𝕜) + 1} x) 0,
      norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
hp :
  ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
    p =
      Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
        (toDualContinuousMultilinearMap (E := E) G)
⊢ p ≤ projectiveSeminorm (E := E)
have refine_2 : ∀ (G : Type (max uι u𝕜 uE)) (w : SeminormedAddCommGroup G) (w_1 : NormedSpace 𝕜 G)
  (h :
    p =
      Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
        (toDualContinuousMultilinearMap (E := E) G)),
  p ≤ projectiveSeminorm (E := E)
Tactic: obtain ⟨G, _, _, h⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w : SeminormedAddCommGroup G
w_1 : NormedSpace 𝕜 G
h :
  p =
    Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
      (toDualContinuousMultilinearMap (E := E) G)
⊢ p ≤ projectiveSeminorm (E := E)
have refine_2 : LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
  (Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
    (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
    (toDualContinuousMultilinearMap (E := E) G))
  (projectiveSeminorm (E := E))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ Eq (α := MultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i))
    (ContinuousMultilinearMap.toMultilinearMap (M₁ := E) (tprodL 𝕜 (E := E))) (tprod 𝕜 (s := E))
have H : ∀ (x : (i : ι) → E i),
  Eq (α := ⨂[𝕜] (i : ι), E i)
    ((ContinuousMultilinearMap.toMultilinearMap (M₁ := E) (tprodL 𝕜 (E := E)) : (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
        x :
      ⨂[𝕜] (i : ι), E i)
    ((tprod 𝕜 (s := E) : (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i) x : ⨂[𝕜] (i : ι), E i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
    ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i) :
          (a : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i)) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
        (tprodL 𝕜 (E := E)) :
      (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
    (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i) : (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
have h : ∀ (x : ⨂[𝕜] (i : ι), E i),
  Eq (α := ⨂[𝕜] (i : ι), E i)
    ((((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i) :
                (a : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i)) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
              (tprodL 𝕜 (E := E)) :
            (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i) :
          (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E i)
        x :
      ⨂[𝕜] (i : ι), E i)
    ((ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i) : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E i) x : ⨂[𝕜] (i : ι), E i)
Tactic: ext