awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
h :
  ∀ (dg : E →L[𝕜] F) (v : Fin (n + 1) → E),
    Eq.{u_4 + 1} (α := G)
      ((((f.fderivCompContinuousLinearMap g : (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G) dg :
              E [⋀^Fin (n + 1)]→L[𝕜] G) :
            (a : Fin (n + 1) → E) → G)
          v :
        G)
      ((((alternatizeUncurryFinCLM 𝕜 E G ∘SL
                    ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) :
                  (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G)
                dg :
              E [⋀^Fin (n + 1)]→L[𝕜] G) :
            (a : Fin (n + 1) → E) → G)
          v :
        G)
⊢ Eq (α := (E →L[𝕜] F) →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] G) (f.fderivCompContinuousLinearMap g)
    (alternatizeUncurryFinCLM 𝕜 E G ∘SL ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft))

Tactic:
ext dg v
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
i j : Fin (n + 1)
x :
  Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) i : E →L[𝕜] F) : (a : E) → F)
        (v i) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) i :
      F)
p :
  ∀ (j : Fin n),
    Eq.{u_3 + 1} (α := F)
      (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) (i.succAbove j) : E →L[𝕜] F) :
            (a : E) → F)
          (v (i.succAbove j)) :
        F)
      (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
          ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) (i.succAbove j) :
        F)
⊢ Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) j : E →L[𝕜] F) : (a : E) → F)
        (v j) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) j :
      F)

Tactic:
cases j using i.succAboveCases
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
⊢ Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) i : E →L[𝕜] F) : (a : E) → F)
        (v i) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) i :
      F)

Tactic:
simp [Fin.removeNth]

Premises used: Fin.removeNth
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
j : Fin n
⊢ Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) (i.succAbove j) : E →L[𝕜] F) :
          (a : E) → F)
        (v (i.succAbove j)) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) (i.succAbove j) :
      F)

Tactic:
simp [Fin.removeNth]

Premises used: Fin.removeNth
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
⊢ ∀ (i j : Fin (n + 1)),
    Eq.{u_3 + 1} (α := F)
      (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) j : E →L[𝕜] F) : (a : E) → F)
          (v j) :
        F)
      (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
          ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) j :
        F)

Tactic:
have (i j : Fin (n + 1)) :
      i.insertNth (α := fun _ ↦ E →L[𝕜] F) dg (fun _ ↦ g) j (v j) =
        i.insertNth (α := fun _ ↦ F) (dg (v i)) (g ∘ i.removeNth v) j := by
    cases j using i.succAboveCases <;> simp [Fin.removeNth]
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
this :
  ∀ (i j : Fin (n + 1)),
    Eq.{u_3 + 1} (α := F)
      (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) j : E →L[𝕜] F) : (a : E) → F)
          (v j) :
        F)
      (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
          ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) j :
        F)
⊢ Eq.{u_4 + 1} (α := G)
    ((((f.fderivCompContinuousLinearMap g : (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G) dg : E [⋀^Fin (n + 1)]→L[𝕜] G) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
    ((((alternatizeUncurryFinCLM 𝕜 E G ∘SL
                  ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) :
                (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G)
              dg :
            E [⋀^Fin (n + 1)]→L[𝕜] G) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)

Tactic:
simp [alternatizeUncurryFin_apply, ← Fin.insertNth_removeNth, Fin.removeNth_fun_const,
    ← map_insertNth, this]

Premises used: ContinuousAlternatingMap.map_insertNth, Fin.insertNth_removeNth, Fin.removeNth_fun_const, ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
f : F [⋀^Fin 0]→L[𝕜] G
⊢ Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0

Tactic:
simp [fderivCompContinuousLinearMap_of_isEmpty, ← alternatizeUncurryFinCLM_apply]

Premises used: ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
succ :
  ∀ (x y : E),
    Eq (α := E [⋀^Fin n]→L[𝕜] G)
      ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                  (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                x :
              E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
            (a : E) → E [⋀^Fin n]→L[𝕜] G)
          y :
        E [⋀^Fin n]→L[𝕜] G)
      ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                  (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                y :
              E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
            (a : E) → E [⋀^Fin n]→L[𝕜] G)
          x :
        E [⋀^Fin n]→L[𝕜] G)
⊢ Eq (α := E [⋀^Fin (n + 1 + 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0

Tactic:
rw [fderivCompContinuousLinearMap_eq_alternatizeUncurryFin,
      ContinuousLinearMap.comp_assoc,
      alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric]

Premises used: ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, ContinuousLinearMap.comp_assoc
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
x y : E
succ :
  ∀ (v : Fin n → E),
    Eq.{u_4 + 1} (α := G)
      ((((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                        (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                      x :
                    E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
                  (a : E) → E [⋀^Fin n]→L[𝕜] G)
                y :
              E [⋀^Fin n]→L[𝕜] G) :
            (a : Fin n → E) → G)
          v :
        G)
      ((((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                        (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                      y :
                    E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
                  (a : E) → E [⋀^Fin n]→L[𝕜] G)
                x :
              E [⋀^Fin n]→L[𝕜] G) :
            (a : Fin n → E) → G)
          v :
        G)
⊢ Eq (α := E [⋀^Fin n]→L[𝕜] G)
    ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
              x :
            E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
          (a : E) → E [⋀^Fin n]→L[𝕜] G)
        y :
      E [⋀^Fin n]→L[𝕜] G)
    ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
              y :
            E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
          (a : E) → E [⋀^Fin n]→L[𝕜] G)
        x :
      E [⋀^Fin n]→L[𝕜] G)

Tactic:
ext v
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
x y : E
v : Fin n → E
⊢ Eq.{u_4 + 1} (α := G)
    ((((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                      (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                    x :
                  E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
                (a : E) → E [⋀^Fin n]→L[𝕜] G)
              y :
            E [⋀^Fin n]→L[𝕜] G) :
          (a : Fin n → E) → G)
        v :
      G)
    ((((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                      (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                    y :
                  E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
                (a : E) → E [⋀^Fin n]→L[𝕜] G)
              x :
            E [⋀^Fin n]→L[𝕜] G) :
          (a : Fin n → E) → G)
        v :
      G)

Tactic:
simp [hsymm]
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 : ℕ
f : F [⋀^Fin n]→L[𝕜] G
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
zero :
  ∀ (f : F [⋀^Fin 0]→L[𝕜] G),
    Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] G)
      (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
succ :
  ∀ (n : ℕ) (f : F [⋀^Fin (n + 1)]→L[𝕜] G),
    Eq (α := E [⋀^Fin (n + 1 + 1)]→L[𝕜] G)
      (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0

Tactic:
cases n with
  | zero =>
    simp [fderivCompContinuousLinearMap_of_isEmpty, ← alternatizeUncurryFinCLM_apply]
  | succ n =>
    rw [fderivCompContinuousLinearMap_eq_alternatizeUncurryFin,
      ContinuousLinearMap.comp_assoc,
      alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric]
    intro x y
    ext v
    simp [hsymm]

Premises used: Fin.succ, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, ContinuousLinearMap.comp_assoc, ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(closedBall 0 1) : Type u_1)
x : (↑(ball 0 r) : Type u_3)
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ < r

Tactic:
simpa only [norm_smul, one_mul] using
          mul_lt_mul' (mem_closedBall_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2) (norm_nonneg _)
            one_pos

Premises used: norm_smul, mul_lt_mul', Iff.mp, mem_closedBall_zero_iff, one_pos, norm_nonneg, one_mul, mem_ball_zero_iff, Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
⊢ Continuous (Y := E) fun (p : Prod.{u_1, u_3} (↑(closedBall 0 1) : Type u_1) (↑(ball 0 r) : Type u_3)) ↦
    (↑p.1 : 𝕜) • (↑p.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(closedBall 0 1) : Type u_1)
x : (↑(closedBall 0 r) : Type u_3)
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ ≤ r

Tactic:
simpa only [norm_smul, one_mul] using
          mul_le_mul (mem_closedBall_zero_iff.1 c.2) (mem_closedBall_zero_iff.1 x.2) (norm_nonneg _)
            zero_le_one

Premises used: norm_smul, zero_le_one, mul_le_mul, Iff.mp, mem_closedBall_zero_iff, norm_nonneg, one_mul, Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
⊢ Continuous (Y := E) fun (p : Prod.{u_1, u_3} (↑(closedBall 0 1) : Type u_1) (↑(closedBall 0 r) : Type u_3)) ↦
    (↑p.1 : 𝕜) • (↑p.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
⊢ Continuous (Y := E) fun (p : Prod.{u_1, u_3} (↑(sphere 0 1) : Type u_1) (↑(ball 0 r) : Type u_3)) ↦
    (↑(inclusion (s := sphere 0 1) (t := closedBall 0 1) ⋯ p.1) : 𝕜) • (↑p.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
⊢ Continuous (Y := E) fun (p : Prod.{u_1, u_3} (↑(sphere 0 1) : Type u_1) (↑(closedBall 0 r) : Type u_3)) ↦
    (↑(inclusion (s := sphere 0 1) (t := closedBall 0 1) ⋯ p.1) : 𝕜) • (↑p.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(sphere 0 1) : Type u_1)
x : (↑(sphere 0 r) : Type u_3)
rw : ‖(↑c : 𝕜)‖ * ‖(↑x : E)‖ = r
rw₁ : 1 * ‖(↑x : E)‖ = r
rw₂ : 1 * r = r
rw₃ rw₄ : r = r
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ = r

Tactic:
rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop,
          one_mul]

Premises used: Subtype.coe_prop, norm_smul, mem_sphere_zero_iff_norm, Iff.mp, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
⊢ Continuous (Y := E) fun (p : Prod.{u_1, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 r) : Type u_3)) ↦
    (↑p.1 : 𝕜) • (↑p.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(closedBall 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2)
    (↑(closedBall 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(closedBall 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2) (↑(ball 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2) (↑(closedBall 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(closedBall 0 1) : Type u_2) (↑(ball 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 1) : Type u_2) (↑(closedBall 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 1) : Type u_2) (↑(ball 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_3} (↑(sphere 0 1) : Type u_1) (↑(sphere 0 1) : Type u_2) (↑(sphere 0 r) : Type u_3)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_2} (↑(sphere 0 1) : Type u_1) (↑(ball 0 1) : Type u_2) (↑(ball 0 1) : Type u_2)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Module.Ball.Action
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
inst_5 : NormedAlgebra 𝕜 𝕜'
inst_6 : IsScalarTower 𝕜 𝕜' E
⊢ IsScalarTower.{u_1, u_2, u_2} (↑(closedBall 0 1) : Type u_1) (↑(ball 0 1) : Type u_2) (↑(ball 0 1) : Type u_2)

Tactic:
⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val, Subtype.ext