case refine'_1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖

case refine'_2
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖
refine' le_antisymm _ _
case refine'_1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
this :
  ∀ (f : ContinuousMultilinearMap 𝕜 (fun x => A) A), (∀ (m : Fin 0 → A), ‖↑f m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖) → ‖f‖ ≤ ‖1‖
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖
case refine'_1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖
have := fun f =>
  @op_norm_le_bound 𝕜 (Fin 0) (fun _ => A) A _ _ _ _ _ _ f _ (norm_nonneg (1 : A))
case refine'_1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
this :
  ∀ (f : ContinuousMultilinearMap 𝕜 (fun x => A) A), (∀ (m : Fin 0 → A), ‖↑f m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖) → ‖f‖ ≤ ‖1‖
⊢ ∀ (m : Fin 0 → A), ‖↑(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖
case refine'_1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
this :
  ∀ (f : ContinuousMultilinearMap 𝕜 (fun x => A) A), (∀ (m : Fin 0 → A), ‖↑f m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖) → ‖f‖ ≤ ‖1‖
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖
refine' this _ _
no goals
case refine'_1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
this :
  ∀ (f : ContinuousMultilinearMap 𝕜 (fun x => A) A), (∀ (m : Fin 0 → A), ‖↑f m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖) → ‖f‖ ≤ ‖1‖
⊢ ∀ (m : Fin 0 → A), ‖↑(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖
simp
case h.e'_3
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ = ‖↑(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun x => 1‖ / ∏ i : Fin 0, ‖1‖
case refine'_2
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖
convert ratio_le_op_norm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)
no goals
case h.e'_3
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
Ei : Fin (Nat.succ n) → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : Fintype ι'
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁹ : (i : ι') → NormedAddCommGroup (E' i)
inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)
inst✝⁷ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (Ei i)
inst✝⁶ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
A : Type u_1
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ = ‖↑(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun x => 1‖ / ∏ i : Fin 0, ‖1‖
simp