awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
h :
  (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some i) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) i (z.2 i) i
⊢ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j) i
have h₁ : ∀ (hij : i ≠ j),
  (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j) i
Tactic: rcases eq_or_ne i j with rfl | hij
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (hypothesis)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)
have B₁ : ∀ (z : G × ((i : ι) → E i)),
  (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)
Tactic: have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)
have have : ∀ (z : G × ((i : ι) → E i)),
  (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)
Tactic: classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
have :
  ∀ (z : G × ((i : ι) → E i)),
    (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
      update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)
have have₁ : ∀
  (B_1 :
    ∀ (z : G × ((i : ι) → E i)),
      (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
        update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)),
  ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)
Tactic: classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ norm.{u_1} (E := F)
      ((MultilinearMap.mk (M₁ := fun (x : Option ι) ↦ G × ((i : ι) → E i))
              (fun (p : (i : Option ι) → G × ((i : ι) → E i)) ↦
                (((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (p none).1 : ContinuousMultilinearMap 𝕜 E F) :
                    (a : (i : ι) → E i) → F)
                  fun (i : ι) ↦ (p (some i)).2 i)
              ⋯ ⋯ :
            (a : (i : Option ι) → G × ((i : ι) → E i)) → F)
          b :
        F) ≤
    ‖B‖ * ∏ i : Option ι, ‖b i‖
have simp : norm.{u_1} (E := F)
    ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) :
          (a : (i : ι) → E i) → F)
        fun (i : ι) ↦ (b (some i)).2 i :
      F) ≤
  ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)
Tactic: simp only [MultilinearMap.coe_mk, Fintype.prod_option]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ norm.{u_1} (E := F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (b (some i)).2 i :
        F) ≤
    ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)
have apply : norm (E := ContinuousMultilinearMap 𝕜 E F)
      ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
    ∏ i : ι, ‖(b (some i)).2 i‖ ≤
  ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)
Tactic: apply (ContinuousMultilinearMap.le_opNorm _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)
have rw : norm (E := ContinuousMultilinearMap 𝕜 E F)
      ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
    ∏ i : ι, ‖(b (some i)).2 i‖ ≤
  ‖B‖ * ‖b none‖ * ∏ i : ι, ‖b (some i)‖
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * ‖b none‖ * ∏ i : ι, ‖b (some i)‖
have h₁ : norm (E := ContinuousMultilinearMap 𝕜 E F)
    ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) ≤
  ‖B‖ * ‖b none‖
Tactic: gcongr with i _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
h₁ :
  norm (E := ContinuousMultilinearMap 𝕜 E F)
      ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) ≤
    ‖B‖ * ‖b none‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * ‖b none‖ * ∏ i : ι, ‖b (some i)‖
have h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → ‖(b (some i)).2 i‖ ≤ ‖b (some i)‖
Tactic: gcongr with i _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
      ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) ≤
    ‖B‖ * ‖b none‖
have h₁ : ‖B‖ * ‖(b none).1‖ ≤ ‖B‖ * ‖b none‖
Tactic: apply (B.le_opNorm _).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ ‖B‖ * ‖(b none).1‖ ≤ ‖B‖ * ‖b none‖
have h₁ : ‖(b none).1‖ ≤ ‖b none‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
⊢ TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K
have obtain : ∀ (v : ℝ) (hv : ∀ x ∈ K, (g x).re ≤ v), TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K
Tactic: obtain ⟨v, hv⟩ : ∃ v, ∀ x ∈ K, (g x).re ≤ v := hg.imp <| by simp [mem_upperBounds]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
⊢ TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K
have this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
Tactic: have : ∀ᶠ i in p, ∀ x ∈ K, (f i x).re ≤ v + 1 := hf.re.eventually_forall_le (lt_add_one v) hv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
⊢ TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K
have refine : ∀ x ∈ K, Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ v + 1} (g x)
Tactic: refine (UniformContinuousOn.cexp _).comp_tendstoUniformlyOn_eventually (by simpa) ?_ hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
⊢ HasSumUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (1 + f i x)) (fun (x : α) ↦ ∑' (i : ι), log (1 + f i x)) K
have simp : TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∑ i ∈ x1, log (1 + f i x2))
  (fun (x : α) ↦ ∑' (i : ι), log (1 + f i x)) atTop K
Tactic: simp only [hasSumUniformlyOn_iff_tendstoUniformlyOn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∑ i ∈ x1, log (1 + f i x2))
    (fun (x : α) ↦ ∑' (i : ι), log (1 + f i x)) atTop K
have apply : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n
Tactic: apply tendstoUniformlyOn_tsum_of_cofinite_eventually <| hu.mul_left (3 / 2)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n
have h₁ : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ x ∈ K, ‖f i x‖ ≤ u i) x} x →
        Membership.mem (γ := Set ι)
          {x : ι |
            Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ u a ≤ 1 / 2) x} x →
              Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n) x} x}
          x}
    a
Tactic: filter_upwards [h, hu.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi hi' x hx
    using (norm_log_one_add_half_le_self <| (hi x hx).trans hi').trans (by simpa using hi x hx)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ x ∈ K, ‖f i x‖ ≤ u i) x} x →
          Membership.mem (γ := Set ι)
            {x : ι |
              Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ u a ≤ 1 / 2) x} x →
                Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n) x} x}
            x}
      a
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n
have h₂ : ∀ (a : ι), (∀ x ∈ K, ‖f a x‖ ≤ u a) → u a ≤ 1 / 2 → ∀ x ∈ K, ‖log (1 + f a x)‖ ≤ 3 / 2 * u a
Tactic: filter_upwards [h, hu.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi hi' x hx
    using (norm_log_one_add_half_le_self <| (hi x hx).trans hi').trans (by simpa using hi x hx)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (hypothesis)
Goal:
α : Type u_1
K : Set α
f : ℕ → α → ℂ
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (β := ℂ) (fun (n : ℕ) (x : α) ↦ ∑ m ∈ range n, log (1 + f m x))
    (fun (x : α) ↦ ∑' (n : ℕ), log (1 + f n x)) atTop K
have h₁ : ∀ᶠ (n : ℕ) in cofinite, ∀ x ∈ K, ‖f n x‖ ≤ u n
Tactic: rw [← Nat.cofinite_eq_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
⊢ HasProdUniformlyOn f (fun (x : α) ↦ ∏' (i : ι), f i x) s
have simp : TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop s
Tactic: simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s
have obtain : ∀ (r : α → ℂ) (hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s),
  TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s
Tactic: obtain ⟨r, hr⟩ := hf.exists