Theorem: fstCmmap_norm (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fstCmmap 𝕜 A B‖ = 1
Tactic:
apply le_antisymm
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fstCmmap 𝕜 A B‖ ≤ 1

case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 1 ≤ ‖fstCmmap 𝕜 A B‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fstCmmap 𝕜 A B‖ ≤ 1
Tactic:
refine (fstCmmap 𝕜 A B).op_norm_le_bound (M := 1) (by norm_num) ?_
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ∀ (m : Fin 1 → A × B), ‖(fstCmmap 𝕜 A B) m‖ ≤ 1 * Finset.univ.prod fun i => ‖m i‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ∀ (m : Fin 1 → A × B), ‖(fstCmmap 𝕜 A B) m‖ ≤ 1 * Finset.univ.prod fun i => ‖m i‖
Tactic:
intro z
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ 1 * Finset.univ.prod fun i => ‖z i‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ 1 * Finset.univ.prod fun i => ‖z i‖
Tactic:
simp only [Finset.univ_unique, Fin.default_eq_zero, Finset.prod_singleton, one_mul]
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ ‖z 0‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Tactic:
have e : z = (fun _ ↦ ((z 0).1, (z 0).2)) := by apply funext; intro i; rw [Fin.eq_zero i]
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ ‖z 0‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Tactic:
rw [e]
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(fstCmmap 𝕜 A B) fun x => ((z 0).1, (z 0).2)‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(fstCmmap 𝕜 A B) fun x => ((z 0).1, (z 0).2)‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Tactic:
rw [fstCmmap_apply]
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(z 0).1‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(z 0).1‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Tactic:
simp
State after:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(z 0).1‖ ≤ ‖z 0‖

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
e : z = fun x => ((z 0).1, (z 0).2)
⊢ ‖(z 0).1‖ ≤ ‖z 0‖
Tactic:
exact norm_fst_le (z 0)
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ z = fun x => ((z 0).1, (z 0).2)
Tactic:
apply funext
State after:
case h
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ ∀ (x : Fin 1), z x = ((z 0).1, (z 0).2)

State before:
case h
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
⊢ ∀ (x : Fin 1), z x = ((z 0).1, (z 0).2)
Tactic:
intro i
State after:
case h
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
i : Fin 1
⊢ z i = ((z 0).1, (z 0).2)

State before:
case h
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
z : Fin 1 → A × B
i : Fin 1
⊢ z i = ((z 0).1, (z 0).2)
Tactic:
rw [Fin.eq_zero i]
State after:
no goals

State before:
case a
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 1 ≤ ‖fstCmmap 𝕜 A B‖
Tactic:
have lo := (fstCmmap 𝕜 A B).unit_le_op_norm (fun _ ↦ (1, 1)) ?_
State after:
case a.refine_2
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
lo : ‖(fstCmmap 𝕜 A B) fun x => (1, 1)‖ ≤ ‖fstCmmap 𝕜 A B‖
⊢ 1 ≤ ‖fstCmmap 𝕜 A B‖

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fun x => (1, 1)‖ ≤ 1

State before:
case a.refine_2
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
lo : ‖(fstCmmap 𝕜 A B) fun x => (1, 1)‖ ≤ ‖fstCmmap 𝕜 A B‖
⊢ 1 ≤ ‖fstCmmap 𝕜 A B‖

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fun x => (1, 1)‖ ≤ 1
Tactic:
rw [fstCmmap_apply, norm_one] at lo
State after:
case a.refine_2
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
lo : 1 ≤ ‖fstCmmap 𝕜 A B‖
⊢ 1 ≤ ‖fstCmmap 𝕜 A B‖

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fun x => (1, 1)‖ ≤ 1

State before:
case a.refine_2
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
lo : 1 ≤ ‖fstCmmap 𝕜 A B‖
⊢ 1 ≤ ‖fstCmmap 𝕜 A B‖

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fun x => (1, 1)‖ ≤ 1
Tactic:
assumption
State after:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fun x => (1, 1)‖ ≤ 1

State before:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ‖fun x => (1, 1)‖ ≤ 1
Tactic:
rw [pi_norm_le_iff_of_nonneg]
State after:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ∀ (i : Fin 1), ‖(1, 1)‖ ≤ 1

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1

State before:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ ∀ (i : Fin 1), ‖(1, 1)‖ ≤ 1

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1
Tactic:
intro i
State after:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
i : Fin 1
⊢ ‖(1, 1)‖ ≤ 1

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1

State before:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
i : Fin 1
⊢ ‖(1, 1)‖ ≤ 1

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1
Tactic:
simp only [Prod.norm_def, norm_one, max_eq_right]
State after:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
i : Fin 1
⊢ max 1 1 ≤ 1

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1

State before:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
i : Fin 1
⊢ max 1 1 ≤ 1

case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1
Tactic:
repeat norm_num
State after:
no goals

State before:
case a.refine_1
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
inst✝³ : NormOneClass A
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : NormOneClass B
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals