awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
⊢ Memℓp (E := fun (i : ι) ↦ ℝ) (g a) ∞
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a i‖)) ((↑K : ℝ) * dist a a₀ + M)
Tactic: use ↑K * dist a a₀ + M
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a i - g a₀ i| + |g a₀ i| ≤ (↑K : ℝ) * dist a a₀ + M
have h₁ : |g a i - g a₀ i| ≤ (↑K : ℝ) * dist a a₀
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
h₁ : |g a i - g a₀ i| ≤ (↑K : ℝ) * dist a a₀
⊢ |g a i - g a₀ i| + |g a₀ i| ≤ (↑K : ℝ) * dist a a₀ + M
have h₂ : |g a₀ i| ≤ M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ (fun (i : ι) ↦ ‖g a i‖) i ≤ (↑K : ℝ) * dist a a₀ + M
have a₁ : |g a i| = |g a i - g a₀ i + g a₀ i|
Tactic: calc
    |g a i| = |g a i - g a₀ i + g a₀ i| := by simp
    _ ≤ |g a i - g a₀ i| + |g a₀ i| := abs_add_le _ _
    _ ≤ ↑K * dist a a₀ + M := by
        gcongr
        · exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀
        · exact hM ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
a₁ : |g a i| = |g a i - g a₀ i + g a₀ i|
⊢ (fun (i : ι) ↦ ‖g a i‖) i ≤ (↑K : ℝ) * dist a a₀ + M
have a₂ : |g a i - g a₀ i| + |g a₀ i| ≤ (↑K : ℝ) * dist a a₀ + M
Tactic: calc
    |g a i| = |g a i - g a₀ i + g a₀ i| := by simp
    _ ≤ |g a i - g a₀ i| + |g a₀ i| := abs_add_le _ _
    _ ≤ ↑K * dist a a₀ + M := by
        gcongr
        · exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀
        · exact hM ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
⊢ LipschitzOnWith K f s ↔
    ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
have simp_rw : (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) ↔
  ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
Tactic: simp_rw [lipschitzOnWith_iff_dist_le_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
⊢ (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) ↔
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
have mp : (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) →
  ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
mp :
  (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) →
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
⊢ (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) ↔
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
have mpr : (∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y) →
  ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ dist ((↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ((↑(f y) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ≤ dist (f x) (f y)
have simp : ‖(↑(f x) : (i : ι) → ℝ) i - (↑(f y) : (i : ι) → ℝ) i‖ ≤ ‖f x - f y‖
Tactic: simp only [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
have dist : dist ((↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ((↑(f y) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ≤ dist (f x) (f y)
Tactic: calc
      dist (f x i) (f y i) ≤ dist (f x) (f y) := by
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm top_ne_zero (f x - f y) i
      _ ≤ K * dist x y := hfl x hx y hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
have mpr : ‖f x - f y‖ ≤ (↑K : ℝ) * dist x y
Tactic: rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖f x - f y‖ ≤ (↑K : ℝ) * dist x y
have mpr : 0 ≤ (↑K : ℝ) * dist x y
Tactic: apply lp.norm_le_of_forall_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
mpr : 0 ≤ (↑K : ℝ) * dist x y
⊢ ‖f x - f y‖ ≤ (↑K : ℝ) * dist x y
have mpr₁ : ∀ (i : ι), ‖(↑(f x - f y) : (i : ι) → ℝ) i‖ ≤ (↑K : ℝ) * dist x y
Tactic: apply lp.norm_le_of_forall_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
⊢ LipschitzWith K f ↔
    ∀ (i : ι), LipschitzWith (β := (fun (x : ι) ↦ ℝ) i) K fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i
have simp_rw : LipschitzOnWith K f Set.univ ↔ ∀ (i : ι), LipschitzOnWith (β := ℝ) K (fun (a : α) ↦ (↑(f a) : (i : ι) → ℝ) i) Set.univ
Tactic: simp_rw [← lipschitzOnWith_univ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f_1 : E [⋀^ι]→L[𝕜] F
m : ι → E
inst_8 : IsEmpty ι
f : E [⋀^ι]→L[𝕜] F
⊢ constOfIsEmpty 𝕜 E ι ((fun (f : E [⋀^ι]→L[𝕜] F) ↦ ((f : (a : ι → E) → F) 0 : F)) f) = f
have H : ∀ (x : ι → E),
  Eq.{wF + 1} (α := F)
    ((constOfIsEmpty 𝕜 E ι ((fun (f : E [⋀^ι]→L[𝕜] F) ↦ ((f : (a : ι → E) → F) 0 : F)) f) : (a : ι → E) → F) x : F)
    ((f : (a : ι → E) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
C : ℝ
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E
⊢ C * ∏ i : ι, ‖m i‖ ≤ max C 0 * ∏ i : ι, ‖m i‖
have hbc : C ≤ max C 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →L[𝕜] E [⋀^ι]→L[𝕜] G
v : ι → E
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear (E := fun (x : ι) ↦
              E).toMultilinearMap
          (M₁ := fun (x : ι) ↦ E).toFun
      (M₁ := fun (x : ι) ↦ E) v =
    0
have h : ∀ (x : F),
  Eq.{wG + 1} (α := G)
    (((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear (E := fun (x : ι) ↦
                    E).toMultilinearMap
                (M₁ := fun (x : ι) ↦ E).toFun
            (M₁ := fun (x : ι) ↦ E) v :
          (a : F) → G)
        x :
      G)
    ((0 : (a : F) → G) x : G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
⊢ Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM
have rcases : ∀ (val : Fintype ι), Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM
Tactic: rcases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
val : Fintype ι
⊢ Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM
have refine : Continuous (X := E →L[𝕜] F) (Y :=
  UniformConvergenceCLM (RingHom.id 𝕜) (E := F [⋀^ι]→L[𝕜] G)
    (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
    {S : Set (F [⋀^ι]→L[𝕜] G) | Bornology.IsVonNBounded 𝕜 S})
  (ContinuousLinearMap.comp (toContinuousMultilinearMapCLM 𝕜) ∘ compContinuousLinearMapCLM)
Tactic: refine UniformConvergenceCLM.isUniformInducing_postcomp (.id 𝕜)
    (toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] G) →L[𝕜] _)
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing _ |>.isInducing
    |>.continuous_iff |>.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
val : Fintype ι
⊢ Continuous (X := E →L[𝕜] F) (Y :=
    UniformConvergenceCLM (RingHom.id 𝕜) (E := F [⋀^ι]→L[𝕜] G)
      (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
      {S : Set (F [⋀^ι]→L[𝕜] G) | Bornology.IsVonNBounded 𝕜 S})
    (ContinuousLinearMap.comp (toContinuousMultilinearMapCLM 𝕜) ∘ compContinuousLinearMapCLM)
have change : Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
  (Function.comp (β :=
    ContinuousMultilinearMap.{u, v, wF, wG} 𝕜 (fun (x : ι) ↦ F) G →L[𝕜]
      ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
    (⇑(ContinuousLinearMap.precomp (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
          (toContinuousMultilinearMapCLM 𝕜)) :
      (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G) →
        F [⋀^ι]→L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
    (Function.comp (β := (i : ι) → E →L[𝕜] F)
      (⇑(ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 (fun (x : ι) ↦ E) (fun (x : ι) ↦ F)
            G) :
        (a : (i : ι) → E →L[𝕜] F) →
          ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
      fun (f : E →L[𝕜] F) (x : ι) ↦ f))
Tactic: change Continuous <|
    (toContinuousMultilinearMapCLM 𝕜 : (F [⋀^ι]→L[𝕜] G) →L[𝕜] _).precomp _ ∘
      ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜
        (fun _ : ι ↦ E) (fun _ ↦ F) G ∘
      (fun f _ ↦ f)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ Eq.{wG + 1} (α := G)
    (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                  ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                    ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
                (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
              dg :
            ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
          (a : (i : ι) → E) → G)
        v :
      G)
    (0 : G)
have trans : Eq.{wG + 1} (α := G)
  (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                  ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
              (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
            dg :
          ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
        (a : (i : ι) → E) → G)
      v :
    G)
  (∑ i : ι,
      (f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
    G)
Tactic: trans ∑ i, f fun j ↦ Function.update (fun _ ↦ g) i dg j (v j)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
trans :
  Eq.{wG + 1} (α := G)
    (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                  ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                    ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
                (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
              dg :
            ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
          (a : (i : ι) → E) → G)
        v :
      G)
    (∑ i : ι,
        (f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G)
⊢ Eq.{wG + 1} (α := G)
    (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                  ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                    ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
                (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
              dg :
            ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
          (a : (i : ι) → E) → G)
        v :
      G)
    (0 : G)
have trans₁ : Eq.{wG + 1} (α := G)
  (∑ i : ι,
    (f : (a : ι → F) → G) fun (j : ι) ↦
      ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j))
  0
Tactic: trans ∑ i, f fun j ↦ Function.update (fun _ ↦ g) i dg j (v j)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ Eq.{wG + 1} (α := G)
    (∑ i : ι,
      (f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j))
    0
have rw : HAdd.hAdd (α := G) (β := G)
    ((f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G)
    ((f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G) =
  0
Tactic: rw [← Finset.sum_add_sum_compl {a, b}, Finset.sum_pair hne, Finset.sum_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
rw :
  HAdd.hAdd (α := G) (β := G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G) =
    0
⊢ Eq.{wG + 1} (α := G)
    (∑ i : ι,
      (f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j))
    0
have rw₁ : ∀ (x : ι),
  Membership.mem (γ := Finset ι) {a, b}ᶜ x →
    Eq.{wG + 1} (α := G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) x dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G)
      (0 : G)
Tactic: rw [← Finset.sum_add_sum_compl {a, b}, Finset.sum_pair hne, Finset.sum_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ HAdd.hAdd (α := G) (β := G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G) =
    0
have h : ∀ (i : ι),
  Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a b) : (a : ι) → ι))
        i :
      F)
Tactic: convert! f.map_add_swap _ hne with i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (goal)
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a b) : (a : ι) → ι))
        i :
      F)
have h : ∀ (heq : v i = v b) (hne : i ≠ b),
  Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap i b) : (a : ι) → ι))
        i :
      F)
Tactic: rcases eq_or_ne i a with rfl | hia
Cleared hypotheses: a, heq, hne