internlm/Lean-Github huggingface dataset:
Theorem: iter_approx
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z
Tactic:
have e : log (log (abs ((f' d c)^[n] (f' d c z)))) - log (log (abs z)) - (n+1) * log d =
    (log (log (abs (f' d c z))) - log (log (abs z)) - log d) +
    (log (log (abs ((f' d c)^[n] (f' d c z)))) - log (log (abs (f' d c z))) - n * log d) := by
  ring
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z
Theorem: iter_approx
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z
Tactic:
rw [e, iter_error_peel z3 cz]
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)
Theorem: iter_approx
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)
Tactic:
have le : abs z ≤ abs (f' d c z) := le_self_iter d z3 cz 1
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
le : Complex.abs z ≤ Complex.abs (f' d c z)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)
Theorem: iter_approx
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
e :
  (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
le : Complex.abs z ≤ Complex.abs (f' d c z)
⊢ |(Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
        ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)| ≤
    f_error d z + iter_error d c (f' d c z)
Tactic:
exact le_trans (abs_add _ _) (add_le_add (f_approx z3 cz)
  (h (le_trans z3 le) (le_trans cz le)))
Proof state after:
no goals
Theorem: iter_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log =
    (Complex.abs (f' d c z)).log.log - (Complex.abs z).log.log - (↑d).log +
      ((Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs (f' d c z)).log.log - ↑n * (↑d).log)
Tactic:
ring
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.toFun_eq_coe
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁸ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝⁷ : Semiring R✝
R A B : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
f : ContinuousMultilinearMap R (fun x => A) B
⊢ f.toFun = ⇑f
Tactic:
rw [MultilinearMap.toFun_eq_coe]
Proof state after:
n : ℕ
𝕜 : Type
inst✝⁸ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝⁷ : Semiring R✝
R A B : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
f : ContinuousMultilinearMap R (fun x => A) B
⊢ ⇑f.toMultilinearMap = ⇑f
Theorem: ContinuousMultilinearMap.toFun_eq_coe
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁸ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝⁷ : Semiring R✝
R A B : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
f : ContinuousMultilinearMap R (fun x => A) B
⊢ ⇑f.toMultilinearMap = ⇑f
Tactic:
simp
Proof state after:
no goals
Theorem: fstCmmap_apply
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
a : A
b : B
⊢ ((fstCmmap R A B) fun x => (a, b)) = a
Tactic:
simp only [fstCmmap, ContinuousMultilinearMap.ofSubsingleton_apply_apply,
  ContinuousLinearMap.coe_fst']
Proof state after:
no goals
Theorem: sndCmmap_apply
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
a : A
b : B
⊢ ((sndCmmap R A B) fun x => (a, b)) = b
Tactic:
simp only [sndCmmap, ContinuousMultilinearMap.ofSubsingleton_apply_apply,
  ContinuousLinearMap.coe_snd']
Proof state after:
no goals
Theorem: fstCmmap_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
⊢ ‖fstCmmap 𝕜 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
⊢ ‖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‖
Theorem: fstCmmap_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
⊢ ‖fstCmmap 𝕜 A B‖ ≤ 1
Tactic:
refine (fstCmmap 𝕜 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), ‖(fstCmmap 𝕜 A B) m‖ ≤ 1 * Finset.univ.prod fun i => ‖m i‖
Theorem: fstCmmap_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), ‖(fstCmmap 𝕜 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
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ 1 * Finset.univ.prod fun i => ‖z i‖
Theorem: fstCmmap_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
⊢ ‖(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]
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
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Theorem: fstCmmap_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
⊢ ‖(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]
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)
⊢ ‖(fstCmmap 𝕜 A B) z‖ ≤ ‖z 0‖
Theorem: fstCmmap_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)
⊢ ‖(fstCmmap 𝕜 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)
⊢ ‖(fstCmmap 𝕜 A B) fun x => ((z 0).1, (z 0).2)‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Theorem: fstCmmap_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)
⊢ ‖(fstCmmap 𝕜 A B) fun x => ((z 0).1, (z 0).2)‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Tactic:
rw [fstCmmap_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).1‖ ≤ ‖(fun x => ((z 0).1, (z 0).2)) 0‖
Theorem: fstCmmap_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).1‖ ≤ ‖(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).1‖ ≤ ‖z 0‖
Theorem: fstCmmap_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).1‖ ≤ ‖z 0‖
Tactic:
exact norm_fst_le (z 0)
Proof state after:
no goals
Theorem: fstCmmap_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: fstCmmap_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: fstCmmap_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: fstCmmap_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: fstCmmap_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 ≤ ‖fstCmmap 𝕜 A B‖
Tactic:
have lo := (fstCmmap 𝕜 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 : ‖(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
Theorem: fstCmmap_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 : ‖(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
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 ≤ ‖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
Theorem: fstCmmap_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 ≤ ‖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
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: 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
⊢ ‖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: 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), ‖(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: 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
⊢ ‖(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