internlm/Lean-Github huggingface dataset:
Theorem: fstCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: fstCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: sndCmmap_norm
Proof 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
⊢ ‖sndCmmap 𝕜 A B‖ = 1
Tactic:
apply le_antisymm
Proof 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
⊢ ‖sndCmmap 𝕜 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 ≤ ‖sndCmmap 𝕜 A B‖
Theorem: sndCmmap_norm
Proof 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
⊢ ‖sndCmmap 𝕜 A B‖ ≤ 1
Tactic:
apply (sndCmmap 𝕜 A B).op_norm_le_bound (M := 1) (by norm_num)
Proof 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), ‖(sndCmmap 𝕜 A B) m‖ ≤ 1 * Finset.univ.prod fun i => ‖m i‖
Theorem: sndCmmap_norm
Proof 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), ‖(sndCmmap 𝕜 A B) m‖ ≤ 1 * Finset.univ.prod fun i => ‖m i‖
Tactic:
intro z
Proof 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
⊢ ‖(sndCmmap 𝕜 A B) z‖ ≤ 1 * Finset.univ.prod fun i => ‖z i‖
Theorem: sndCmmap_norm
Proof 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
⊢ ‖(sndCmmap 𝕜 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]
Proof 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
⊢ ‖(sndCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Theorem: sndCmmap_norm
Proof 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
⊢ ‖(sndCmmap 𝕜 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]
Proof 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)
⊢ ‖(sndCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Theorem: sndCmmap_norm
Proof 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)
⊢ ‖(sndCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Tactic:
rw [e]
Proof 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)
⊢ ‖(sndCmmap 𝕜 A B) fun x => ((z 0).1, (z 0).2)‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Theorem: sndCmmap_norm
Proof 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)
⊢ ‖(sndCmmap 𝕜 A B) fun x => ((z 0).1, (z 0).2)‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Tactic:
rw [sndCmmap_apply]
Proof 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).2‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Theorem: sndCmmap_norm
Proof 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).2‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Tactic:
simp
Proof 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).2‖ ≤ ‖z 0‖
Theorem: sndCmmap_norm
Proof 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).2‖ ≤ ‖z 0‖
Tactic:
exact norm_snd_le (z 0)
Proof state after:
no goals
Theorem: sndCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: sndCmmap_norm
Proof 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
Proof 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)
Theorem: sndCmmap_norm
Proof 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
Proof 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)
Theorem: sndCmmap_norm
Proof 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]
Proof state after:
no goals
Theorem: sndCmmap_norm
Proof 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 ≤ ‖sndCmmap 𝕜 A B‖
Tactic:
have lo := (sndCmmap 𝕜 A B).unit_le_op_norm (fun _ ↦ (1, 1)) ?_
Proof 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 : ‖(sndCmmap 𝕜 A B) fun x => (1, 1)‖ ≤ ‖sndCmmap 𝕜 A B‖
⊢ 1 ≤ ‖sndCmmap 𝕜 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
Theorem: sndCmmap_norm
Proof 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 : ‖(sndCmmap 𝕜 A B) fun x => (1, 1)‖ ≤ ‖sndCmmap 𝕜 A B‖
⊢ 1 ≤ ‖sndCmmap 𝕜 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 [sndCmmap_apply, norm_one] at lo
Proof 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 ≤ ‖sndCmmap 𝕜 A B‖
⊢ 1 ≤ ‖sndCmmap 𝕜 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
Theorem: sndCmmap_norm
Proof 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 ≤ ‖sndCmmap 𝕜 A B‖
⊢ 1 ≤ ‖sndCmmap 𝕜 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
Proof 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
Theorem: sndCmmap_norm
Proof 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]
Proof 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
Theorem: sndCmmap_norm
Proof 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
Proof 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
Theorem: sndCmmap_norm
Proof 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]
Proof 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
Theorem: sndCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: sndCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: update_0_0
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
⊢ Function.update (fun x => z 0) 0 x = fun x_1 => x
Tactic:
apply funext
Proof state after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
⊢ ∀ (x_1 : Fin 1), Function.update (fun x => z 0) 0 x x_1 = x
Theorem: update_0_0
Proof state before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
⊢ ∀ (x_1 : Fin 1), Function.update (fun x => z 0) 0 x x_1 = x
Tactic:
intro i
Proof state after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
⊢ Function.update (fun x => z 0) 0 x i = x
Theorem: update_0_0
Proof state before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
⊢ Function.update (fun x => z 0) 0 x i = x
Tactic:
have i0 : i = 0 := by simp only [eq_iff_true_of_subsingleton]
Proof state after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x i = x
Theorem: update_0_0
Proof state before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x i = x
Tactic:
rw [i0]
Proof state after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x 0 = x
Theorem: update_0_0
Proof state before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
i0 : i = 0
⊢ Function.update (fun x => z 0) 0 x 0 = x
Tactic:
simp only [Function.update_same]
Proof state after:
no goals
Theorem: update_0_0
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
z : Fin (n + 1) → A
x : A
i : Fin 1
⊢ i = 0
Tactic:
simp only [eq_iff_true_of_subsingleton]
Proof state after:
no goals
Theorem: update_0_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
⊢ Function.update f 0 x i.succ = f i.succ
Tactic:
rw [Function.update_apply]
Proof state after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
⊢ (if i.succ = 0 then x else f i.succ) = f i.succ
Theorem: update_0_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
⊢ (if i.succ = 0 then x else f i.succ) = f i.succ
Tactic:
simp only [ite_eq_right_iff]
Proof state after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
⊢ i.succ = 0 → x = f i.succ
Theorem: update_0_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
⊢ i.succ = 0 → x = f i.succ
Tactic:
have i0 := Fin.succ_ne_zero i
Proof state after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
i0 : i.succ ≠ 0
⊢ i.succ = 0 → x = f i.succ
Theorem: update_0_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
i0 : i.succ ≠ 0
⊢ i.succ = 0 → x = f i.succ
Tactic:
intro h
Proof state after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ x = f i.succ
Theorem: update_0_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ x = f i.succ
Tactic:
exfalso
Proof state after:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ False
Theorem: update_0_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin n
i0 : i.succ ≠ 0
h : i.succ = 0
⊢ False
Tactic:
exact i0 h
Proof state after:
no goals
Theorem: update_nz_0
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ Function.update f i x 0 = f 0
Tactic:
rw [Function.update_noteq i0.symm]
Proof state after:
no goals
Theorem: update_nz_succ
Proof state before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ (fun j => Function.update f i x j.succ) = Function.update (fun j => f j.succ) (i.pred i0) x
Tactic:
apply funext
Proof state after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ ∀ (x_1 : Fin n), Function.update f i x x_1.succ = Function.update (fun j => f j.succ) (i.pred i0) x x_1
Theorem: update_nz_succ
Proof state before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ ∀ (x_1 : Fin n), Function.update f i x x_1.succ = Function.update (fun j => f j.succ) (i.pred i0) x x_1
Tactic:
intro k
Proof state after:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Theorem: update_nz_succ
Proof state before:
case h
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k
Tactic:
by_cases ki : k.succ = i
Proof state after:
case pos
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : k.succ = i
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k

case neg
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
k : Fin n
ki : ¬k.succ = i
⊢ Function.update f i x k.succ = Function.update (fun j => f j.succ) (i.pred i0) x k