awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
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)
⊢ 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₁ : ∀ (hia : i ≠ a),
  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: rcases eq_or_ne i a with rfl | hia
-- 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 : ι
hia : i ≠ a
⊢ 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 a = v i) (hne : a ≠ i),
  Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i 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 i) : (a : ι) → ι))
        i :
      F)
Tactic: rcases eq_or_ne i b with rfl | hib
Cleared hypotheses: b, heq, hne
-- 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 : ι
hia : i ≠ a
h :
  ∀ (heq : v a = v i) (hne : a ≠ i),
    Eq.{wF + 1} (α := F)
      (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i 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 i) : (a : ι) → ι))
          i :
        F)
⊢ 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₁ : ∀ (hib : 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) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a b) : (a : ι) → ι))
        i :
      F)
Tactic: rcases eq_or_ne i b with rfl | hib
-- 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
⊢ ∀ (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)
have simp : ∀ (x : ι),
  ¬x = a →
    ¬x = b →
      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: simp only [mem_compl, mem_insert, mem_singleton, not_or, and_imp]
-- 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 : ι
hia : ¬i = a
hib : ¬i = b
⊢ Eq.{wG + 1} (α := G)
    ((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)
    (0 : G)
have apply : Eq.{wF + 1} (α := F)
  (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg a : E →L[𝕜] F) : (a : E) → F) (v a) : F)
  (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg b : E →L[𝕜] F) : (a : E) → F) (v b) : F)
Tactic: apply f.map_eq_zero_of_eq _ _ hne
-- 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 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : IsEmpty ι
⊢ Eq (α := (f : F [⋀^ι]→L[𝕜] G) → (g : E →L[𝕜] F) → (E →L[𝕜] F) →L[𝕜] E [⋀^ι]→L[𝕜] G) fderivCompContinuousLinearMap 0
have h : ∀ (x : F [⋀^ι]→L[𝕜] G) (x_1 x_2 : E →L[𝕜] F) (x_3 : ι → E),
  Eq.{wG + 1} (α := G)
    ((((x.fderivCompContinuousLinearMap x_1 : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) x_2 : E [⋀^ι]→L[𝕜] G) : (a : ι → E) → G)
        x_3 :
      G)
    ((((0 x x_1 : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) x_2 : E [⋀^ι]→L[𝕜] G) : (a : ι → E) → G) x_3 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.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 →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x y : F
⊢ mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (x + y)) (C * ‖x + y‖) ⋯ =
    mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯ +
      mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) y) (C * ‖y‖) ⋯
have H₁ : ∀ (x_1 : ι → E),
  Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (x + y)) (C * ‖x + y‖) sorry : (a : ι → E) → G) x_1 : G)
    ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) sorry +
            mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) y) (C * ‖y‖) sorry :
          (a : ι → E) → G)
        x_1 :
      G)
Tactic: ext1
-- 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 →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
c : 𝕜
x : F
⊢ mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (c • x)) (C * ‖c • x‖) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯)
have H₁ : ∀ (x_1 : ι → E),
  Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (c • x)) (C * ‖c • x‖) sorry : (a : ι → E) → G) x_1 : G)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) sorry) :
          (a : ι → E) → G)
        x_1 :
      G)
Tactic: ext1
-- 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 →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x : F
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖
have rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
-- 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 →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x : F
rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖
have rw₁ : max (C * ‖x‖) 0 = max (C * ‖x‖) 0
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
-- 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 ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_9 : DecidableEq ι
m : (i : ι) → E
i : ι
x y : E
⊢ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (x + y)))
      (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (x + y) i_1‖) ⋯ =
    mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
        (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯ +
      mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i y))
        (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i y i_1‖) ⋯
have H₁ : ∀ (x_1 : ι' → F),
  Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (x + y)))
            (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (x + y) i_1‖) sorry :
          (a : ι' → F) → G)
        x_1 :
      G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) sorry +
            mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i y))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i y i_1‖) sorry :
          (a : ι' → F) → G)
        x_1 :
      G)
Tactic: ext1
-- 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 ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_9 : DecidableEq ι
m : (i : ι) → E
i : ι
c : 𝕜
x : E
⊢ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (c • x)))
      (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (c • x) i_1‖) ⋯ =
    c •
      mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
        (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯
have H₁ : ∀ (x_1 : ι' → F),
  Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (c • x)))
            (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (c • x) i_1‖) sorry :
          (a : ι' → F) → G)
        x_1 :
      G)
    ((c •
            mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) sorry :
          (a : ι' → F) → G)
        x_1 :
      G)
Tactic: ext1
-- 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 ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
⊢ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v) (C * ∏ i : ι, ‖v i‖) ⋯ = 0
have H₁ : ∀ (v' : ι' → F),
  Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v) (C * ∏ i : ι, ‖v i‖) sorry : (a : ι' → F) → G) v' : G)
    ((0 : (a : ι' → F) → G) v' : G)
Tactic: ext v'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Basic (hypothesis)
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 ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
v' : ι' → F
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v) (C * ∏ i : ι, ‖v i‖) ⋯ : (a : ι' → F) → G) v' : G)
    ((0 : (a : ι' → F) → G) v' : G)
have this : Eq (α := F [⋀^ι']→ₗ[𝕜] G) ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v : F [⋀^ι']→ₗ[𝕜] G) (0 : F [⋀^ι']→ₗ[𝕜] G)
Tactic: have : f v = 0 := by simpa using f.map_eq_zero_of_eq' v i j hv hij
-- 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 ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
⊢ ‖mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m) (C * ∏ i : ι, ‖m i‖) ⋯‖ ≤ max C 0 * ∏ i : ι, ‖m i‖
have refine : max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖
Tactic: refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
-- 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 ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
⊢ max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖
have hc : LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)
Tactic: rw [max_mul_of_nonneg, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Curry (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
g : F [⋀^Fin (n + 1)]→L[𝕜] G
f : E →L[𝕜] F
x : E
v : Fin n → E
i : Fin (n + 1)
⊢ Eq.{u_3 + 1} (α := F)
    (((fun (i : Fin (n + 1)) ↦
              ((↑((fun (x : Fin (n + 1)) ↦ f) i) :
                  LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                    ((fun (x : Fin (n + 1)) ↦ F) i)) :
                LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                  ((fun (x : Fin (n + 1)) ↦ F) i)))
            i :
          (a : (fun (x : Fin (n + 1)) ↦ E) i) → (fun (x : Fin (n + 1)) ↦ F) i)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x v i : E) :
      (fun (x : Fin (n + 1)) ↦ F) i)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ F) ((f : (a : E) → F) x)
        (fun (i : Fin n) ↦
          ((fun (i : Fin n) ↦
                  ((↑((fun (x : Fin n) ↦ f) i) :
                      LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i)
                        ((fun (x : Fin n) ↦ F) i)) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i) ((fun (x : Fin n) ↦ F) i)))
                i :
              (a : (fun (x : Fin n) ↦ E) i) → (fun (x : Fin n) ↦ F) i)
            (v i))
        i :
      F)
have zero : Eq.{u_3 + 1} (α := F)
  (((fun (i : Fin (n + 1)) ↦
            ((↑((fun (x : Fin (n + 1)) ↦ f) i) :
                LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                  ((fun (x : Fin (n + 1)) ↦ F) i)) :
              LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                ((fun (x : Fin (n + 1)) ↦ F) i)))
          0 :
        (a : (fun (x : Fin (n + 1)) ↦ E) 0) → (fun (x : Fin (n + 1)) ↦ F) 0)
      (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x v 0 : E) :
    (fun (x : Fin (n + 1)) ↦ F) 0)
  (Fin.cons (α := fun (x : Fin n.succ) ↦ F) ((f : (a : E) → F) x)
      (fun (i : Fin n) ↦
        ((fun (i : Fin n) ↦
                ((↑((fun (x : Fin n) ↦ f) i) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i) ((fun (x : Fin n) ↦ F) i)) :
                  LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i) ((fun (x : Fin n) ↦ F) i)))
              i :
            (a : (fun (x : Fin n) ↦ E) i) → (fun (x : Fin n) ↦ F) i)
          (v i))
      0 :
    F)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
⊢ Eq.{u_3 + 1} (α := F) ((alternatizeUncurryFin f : (a : Fin (n + 1) → E) → F) v : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((f : (a : E) → E [⋀^Fin n]→L[𝕜] F) (v i) : E [⋀^Fin n]→L[𝕜] F) : (a : Fin n → E) → F)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) :
            F) :
      F)
have rw : Eq.{u_3 + 1} (α := F)
  ((((sorry : (a : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] F) f : E [⋀^Fin (n + 1)]→L[𝕜] F) :
        (a : Fin (n + 1) → E) → F)
      v :
    F)
  (∑ i : Fin (n + 1),
      HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        ((((f : (a : E) → E [⋀^Fin n]→L[𝕜] F) (v i) : E [⋀^Fin n]→L[𝕜] F) : (a : Fin n → E) → F)
            (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) :
          F) :
    F)
Tactic: rw [alternatizeUncurryFin, alternatizeUncurryFinCLM]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
⊢ (alternatizeUncurryFin f).toAlternatingMap =
    AlternatingMap.alternatizeUncurryFin (toAlternatingMapLinear ∘ₗ (↑f : E →ₗ[𝕜] E [⋀^Fin n]→L[𝕜] F))
have H : ∀ (x : Fin (n + 1) → E),
  Eq.{u_3 + 1} (α := F) (((alternatizeUncurryFin f).toAlternatingMap : (a : Fin (n + 1) → E) → F) x : F)
    ((AlternatingMap.alternatizeUncurryFin (toAlternatingMapLinear ∘ₗ (↑f : E →ₗ[𝕜] E [⋀^Fin n]→L[𝕜] F)) :
          (a : Fin (n + 1) → E) → F)
        x :
      F)
Tactic: ext