awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
⊢ LE.le (α := ℝ) ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (⨂ₜ[𝕜] (i : ι), m i) : ℝ)
    (∏ i : ι, ‖m i‖ : ℝ)
have h : ∏ i : ι, ‖m i‖ =
  projectiveSeminormAux.{uι, u𝕜, uE} (𝕜 := 𝕜) (E := E)
    (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
          Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i)) x)
          (FreeAddMonoid.of (1, m)) sorry) :
      FreeAddMonoid (𝕜 × ((i : ι) → E i)))
Tactic: convert! ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of ((1 : 𝕜), m), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
h :
  ∏ i : ι, ‖m i‖ =
    projectiveSeminormAux.{uι, u𝕜, uE} (𝕜 := 𝕜) (E := E)
      (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
            Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i)) x)
            (FreeAddMonoid.of (1, m)) ⋯) :
        FreeAddMonoid (𝕜 × ((i : ι) → E i)))
⊢ LE.le (α := ℝ) ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (⨂ₜ[𝕜] (i : ι), m i) : ℝ)
    (∏ i : ι, ‖m i‖ : ℝ)
have convert_2 : Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i))
  (FreeAddMonoid.of (1, m))
Tactic: convert! ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of ((1 : 𝕜), m), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    ‖f‖ * ‖x‖
have rw : norm.{u_1} (E := G)
    ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
            (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
          (a : ⨂[𝕜] (i : ι), E i) → G)
        x :
      G) ≤
  ⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
    projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))) * ‖f‖
Tactic: rw [norm_def, mul_comm, Real.iInf_mul_of_nonneg (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    ⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))) * ‖f‖
have refine : ∀ (x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))) (p : FreeAddMonoid (𝕜 × ((i : ι) → E i)))
  (hp : p ∈ x.lifts (s := E)),
  norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x_2 : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦ x_2 ∈ x.lifts (s := E)) p hp) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖
Tactic: refine le_ciInf fun ⟨p, hp⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x_2 : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦ x_2 ∈ x.lifts (s := E)) p hp) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖
have rw! : norm.{u_1} (E := G)
    (Multiset.sum
      (↑(List.map (α := 𝕜 × ((i : ι) → E i))
            (Function.comp (β := ⨂[𝕜] (i : ι), E i)
              (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                      (f.toMultilinearMap (M₁ := E)) :
                    (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                (a : ⨂[𝕜] (i : ι), E i) → G)
              fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
            ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
        Multiset G)) ≤
  projectiveSeminormAux (E := E)
      (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
            Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
              (lifts (s := E)
                (List.sum
                  (List.map
                    (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                    ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                      p))))
              x)
            p sorry) :
        FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
    ‖f‖
Tactic: rw! [← ((mem_lifts_iff x p).mp hp), ← List.sum_map_hom, ← Multiset.sum_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
⊢ norm.{u_1} (E := G)
      (Multiset.sum
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
              Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
                (lifts (s := E)
                  (List.sum
                    (List.map
                      (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                        p))))
                x)
              p ⋯) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖
have grw : Multiset.sum
    (Multiset.map (fun (x : G) ↦ ‖x‖)
      (↑(List.map (α := 𝕜 × ((i : ι) → E i))
            (Function.comp (β := ⨂[𝕜] (i : ι), E i)
              (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                      (f.toMultilinearMap (M₁ := E)) :
                    (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                (a : ⨂[𝕜] (i : ι), E i) → G)
              fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
            ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
        Multiset G)) ≤
  projectiveSeminormAux (E := E)
      (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
            Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
              (lifts (s := E)
                (List.sum
                  (List.map
                    (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                    ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                      p))))
              x)
            p sorry) :
        FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
    ‖f‖
Tactic: grw [norm_multiset_sum_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
⊢ Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
              Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
                (lifts (s := E)
                  (List.sum
                    (List.map
                      (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                        p))))
                x)
              p ⋯) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖
have simp : LE.le (α := ℝ)
  (Multiset.sum
    (Multiset.map (fun (x : G) ↦ ‖x‖)
      (↑(List.map (α := 𝕜 × ((i : ι) → E i))
            (Function.comp (β := ⨂[𝕜] (i : ι), E i)
              (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                      (f.toMultilinearMap (M₁ := E)) :
                    (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                (a : ⨂[𝕜] (i : ι), E i) → G)
              fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
            ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
        Multiset G)))
  (List.sum
    (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
      (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))))
Tactic: simp only [mul_comm, ← smul_eq_mul, List.smul_sum, projectiveSeminormAux]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
⊢ LE.le (α := ℝ)
    (Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)))
    (List.sum
      (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
        (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))))
have refine : List.Forall₂ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2)
  (List.map (fun (x : G) ↦ ‖x‖)
    (List.map (α := 𝕜 × ((i : ι) → E i))
      (Function.comp (β := ⨂[𝕜] (i : ι), E i)
        (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
          (a : ⨂[𝕜] (i : ι), E i) → G)
        fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)))
  (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
    (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)))
Tactic: refine List.Forall₂.sum_le_sum ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x‖ = 1
have this : ‖x‖ ≠ 0
Tactic: have : ‖x‖ ≠ 0 := by simp [hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖x‖ : 𝕜)⁻¹ • x‖ = r
have this : ‖x‖ ≠ 0
Tactic: have : ‖x‖ ≠ 0 := by simp [hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have pos : ∀ (z_zero : z = 0), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
Tactic: by_cases z_zero : z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
pos : ∀ (z_zero : z = 0), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have neg : ∀ (z_zero : ¬z = 0), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
Tactic: by_cases z_zero : z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : z = 0
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have pos : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) 0 : 𝕜) ≤ c / r * norm.{u_2} (E := E) 0
Tactic: rw [z_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : z = 0
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) 0 : 𝕜) ≤ c / r * norm.{u_2} (E := E) 0
have pos : LE.le (α := ℝ) 0 0
Tactic: simp only [map_zero, norm_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have hz₁ : let z₁ := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z;
z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
Tactic: set z₁ := ((r : 𝕜) * (‖z‖ : 𝕜)⁻¹) • z with hz₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
have a : Membership.mem (γ := Set E) (sphere 0 r) z₁
Tactic: apply h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
⊢ Membership.mem (γ := Set E) (sphere 0 r) z₁
have a : ‖z₁‖ = r
Tactic: rw [mem_sphere_zero_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
Tactic: have norm_f_z₁ : ‖f z₁‖ ≤ c := by
    apply h
    rw [mem_sphere_zero_iff_norm]
    exact norm_smul_inv_norm' r_pos.le z_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
Tactic: have r_ne_zero : (r : 𝕜) ≠ 0 := RCLike.ofReal_ne_zero.mpr r_pos.ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
⊢ (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
have rw : (f : (a : E) → 𝕜) z =
  HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜) *
    HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹) ((f : (a : E) → 𝕜) z : 𝕜)
Tactic: rw [hz₁, map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
⊢ (f : (a : E) → 𝕜) z =
    HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜) *
      HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹) ((f : (a : E) → 𝕜) z : 𝕜)
have rw : Ne.{u_1 + 1} (α := 𝕜) (↑‖z‖ : 𝕜) 0
Tactic: rw [← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ r_ne_zero, mul_inv_cancel₀, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
Tactic: have eq : f z = ‖z‖ / r * f z₁ := by
    rw [hz₁, map_smul, smul_eq_mul]
    rw [← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ r_ne_zero, mul_inv_cancel₀, one_mul]
    simp only [z_zero, RCLike.ofReal_eq_zero, norm_eq_zero, Ne, not_false_iff]