awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
this : 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
⊢ 0 < -((↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P)

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
suffices : 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P < 0

Tactic:
suffices 0 < Int.negOnePow (-P).natDegree * (-P).eval x by apply neg_pos.mp; simpa
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
⊢ 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)

Tactic:
zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
refine_2 : 0 ≤ (-P).leadingCoeff
⊢ 0 < (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)

Tactic:
refine zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
refine_1₂ : -eval y P = 0
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : eval y (-P) = 0
⊢ P.IsRoot y

Tactic:
rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]

Premises used: Polynomial.IsRoot, neg_eq_iff_eq_neg, Polynomial.eval_neg, neg_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
refine_2 : 0 ≤ -P.leadingCoeff
refine_2₁ : P.leadingCoeff ≤ -0
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
rwa [leadingCoeff_neg, le_neg, neg_zero]

Premises used: le_neg, neg_zero, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
apply : 0 ≤ -((↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P)
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P ≤ 0

Tactic:
apply neg_nonneg.mp

Premises used: neg_nonneg, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
⊢ 0 ≤ -((↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P)

Tactic:
simpa
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
suffices : 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)
⊢ (↑(↑(Int.negOnePow (↑P.natDegree : ℤ)) : ℤ) : ℝ) * eval x P ≤ 0

Tactic:
suffices 0 ≤ Int.negOnePow (-P).natDegree * (-P).eval x by apply neg_nonneg.mp; simpa
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)

Tactic:
zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
refine_1 : ∀ (y : ℝ) (hy : (-P).IsRoot y), P.IsRoot y
refine_2 : 0 ≤ (-P).leadingCoeff
⊢ 0 ≤ (↑(↑(Int.negOnePow (↑(-P).natDegree : ℤ)) : ℤ) : ℝ) * eval x (-P)

Tactic:
refine zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg (fun y hy => hroots y ?_) ?_

Premises used: Polynomial.zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
refine_1 : eval y P = 0
refine_1₁ : eval y P = -0
refine_1₂ : -eval y P = 0
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : eval y (-P) = 0
⊢ P.IsRoot y

Tactic:
rwa [IsRoot, ← neg_zero, ← neg_eq_iff_eq_neg, ← eval_neg]

Premises used: Polynomial.IsRoot, neg_eq_iff_eq_neg, Polynomial.eval_neg, neg_zero
-- Module: Mathlib.Analysis.Polynomial.Order
Goal:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
refine_2 : 0 ≤ -P.leadingCoeff
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : P.leadingCoeff ≤ 0
⊢ 0 ≤ (-P).leadingCoeff

Tactic:
rwa [leadingCoeff_neg, neg_nonneg]

Premises used: neg_nonneg, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Analysis.Quaternion
Goal:
a : ℍ
⊢ ⟪a, a⟫ = (normSq : (a : ℍ) → ℝ) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
a b : ℍ
⊢ ⟪a, b⟫ = (a * star b).re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
x y : ℍ
⊢ (starRingEnd ℝ : (a : ℝ) → ℝ) ⟪y, x⟫ = ⟪x, y⟫

Tactic:
simp [inner_def, mul_comm]

Premises used: Quaternion.inner_def, mul_comm
-- Module: Mathlib.Analysis.Quaternion
Goal:
x y z : ℍ
⊢ ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
simp only [inner_def, add_mul, re_add]

Premises used: add_mul, Quaternion.inner_def, Quaternion.re_add
-- Module: Mathlib.Analysis.Quaternion
Goal:
x y : ℍ
r : ℝ
simp :
  r * x.re * y.re + r * x.imI * y.imI + r * x.imJ * y.imJ + r * x.imK * y.imK =
    r * (x.re * y.re + x.imI * y.imI + x.imJ * y.imJ + x.imK * y.imK)
⊢ ⟪r • x, y⟫ = HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪x, y⟫

Tactic:
simp [inner_def]

Premises used: Quaternion.inner_def
-- Module: Mathlib.Analysis.Quaternion
Goal:
a : ℍ
rw : ⟪a, a⟫ = ‖a‖ * ‖a‖
rw₁ rw₂ : ‖a‖ * ‖a‖ = ‖a‖ * ‖a‖
⊢ (normSq : (a : ℍ) → ℝ) a = ‖a‖ * ‖a‖

Tactic:
rw [← inner_self, real_inner_self_eq_norm_mul_norm]

Premises used: Quaternion.inner_self, real_inner_self_eq_norm_mul_norm
-- Module: Mathlib.Analysis.Quaternion
Goal:
rw : √(inner ℝ (E := ℍ) 1 1) = 1
rw₁ : √((normSq : (a : ℍ) → ℝ) 1) = 1
rw₂ : √1 = 1
rw₃ rw₄ : Eq (α := ℝ) 1 1
⊢ norm (E := ℍ) 1 = 1

Tactic:
rw [norm_eq_sqrt_real_inner, inner_self, normSq.map_one, Real.sqrt_one]

Premises used: MonoidWithZeroHom.map_one, Quaternion.normSq, Quaternion.inner_self, Real.sqrt_one, norm_eq_sqrt_real_inner
-- Module: Mathlib.Analysis.Quaternion
Goal:
a : ℝ
rw : √(inner ℝ (E := ℍ) (↑a : ℍ) (↑a : ℍ)) = ‖a‖
rw₁ : √((normSq : (a : ℍ) → ℝ) (↑a : ℍ)) = ‖a‖
rw₂ : √(HPow.hPow (β := ℕ) a 2) = ‖a‖
rw₃ : |a| = ‖a‖
rw₄ rw₅ : |a| = |a|
⊢ norm (E := ℍ) (↑a : ℍ) = ‖a‖

Tactic:
rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]

Premises used: Real.sqrt_sq_eq_abs, Quaternion.inner_self, Real.norm_eq_abs, Quaternion.normSq_coe, norm_eq_sqrt_real_inner
-- Module: Mathlib.Analysis.Quaternion
Goal:
a : ℝ
⊢ nnnorm (E := ℍ) (↑a : ℍ) = ‖a‖₊

Tactic:
Subtype.ext <| norm_coe a

Premises used: Quaternion.norm_coe, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Quaternion
Goal:
a : ℍ
simp_rw : √⟪star a, star a⟫ = √⟪a, a⟫
simp_rw₁ : √((normSq : (a : ℍ) → ℝ) (star a)) = √((normSq : (a : ℍ) → ℝ) a)
⊢ ‖star a‖ = ‖a‖

Tactic:
simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]

Premises used: Quaternion.inner_self, Quaternion.normSq_star, norm_eq_sqrt_real_inner
-- Module: Mathlib.Analysis.Quaternion
Goal:
a : ℍ
⊢ ‖star a‖₊ = ‖a‖₊

Tactic:
Subtype.ext <| norm_star a

Premises used: NNReal, Subtype.ext, Quaternion.norm_star
-- Module: Mathlib.Analysis.Quaternion
Goal:
x x_1 : ℍ
⊢ √((normSq : (a : ℍ) → ℝ) (x * x_1)) = √((normSq : (a : ℍ) → ℝ) x) * √((normSq : (a : ℍ) → ℝ) x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z : ℂ
⊢ (↑z : ℍ).re = z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
z : ℂ
⊢ (↑z : ℍ).imI = z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
z : ℂ
⊢ (↑z : ℍ).imJ = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
z : ℂ
⊢ (↑z : ℍ).imK = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
a : (↑(z + w) : ℍ).re = ((↑z : ℍ) + (↑w : ℍ)).re
a₁ : (↑(z + w) : ℍ).imI = ((↑z : ℍ) + (↑w : ℍ)).imI
a₂ : (↑(z + w) : ℍ).imJ = ((↑z : ℍ) + (↑w : ℍ)).imJ
a₃ : (↑(z + w) : ℍ).imK = ((↑z : ℍ) + (↑w : ℍ)).imK
⊢ (↑(z + w) : ℍ) = (↑z : ℍ) + (↑w : ℍ)

Tactic:
ext
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z + w) : ℍ).re = ((↑z : ℍ) + (↑w : ℍ)).re

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z + w) : ℍ).imI = ((↑z : ℍ) + (↑w : ℍ)).imI

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z + w) : ℍ).imJ = ((↑z : ℍ) + (↑w : ℍ)).imJ

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z + w) : ℍ).imK = ((↑z : ℍ) + (↑w : ℍ)).imK

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
a : (↑(z * w) : ℍ).re = ((↑z : ℍ) * (↑w : ℍ)).re
a₁ : (↑(z * w) : ℍ).imI = ((↑z : ℍ) * (↑w : ℍ)).imI
a₂ : (↑(z * w) : ℍ).imJ = ((↑z : ℍ) * (↑w : ℍ)).imJ
a₃ : (↑(z * w) : ℍ).imK = ((↑z : ℍ) * (↑w : ℍ)).imK
⊢ (↑(z * w) : ℍ) = (↑z : ℍ) * (↑w : ℍ)

Tactic:
ext
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z * w) : ℍ).re = ((↑z : ℍ) * (↑w : ℍ)).re

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z * w) : ℍ).imI = ((↑z : ℍ) * (↑w : ℍ)).imI

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z * w) : ℍ).imJ = ((↑z : ℍ) * (↑w : ℍ)).imJ

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
z w : ℂ
⊢ (↑(z * w) : ℍ).imK = ((↑z : ℍ) * (↑w : ℍ)).imK

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ (↑0 : ℍ) = 0

Tactic:
rfl

Premises used: Quaternion.coeComplex, rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ (↑1 : ℍ) = 1

Tactic:
rfl

Premises used: Quaternion.coeComplex, rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
r : ℝ
z : ℂ
a : (r • (↑z : ℍ)).re = ((↑r : ℍ) * (↑z : ℍ)).re
a₁ : (r • (↑z : ℍ)).imI = ((↑r : ℍ) * (↑z : ℍ)).imI
a₂ : (r • (↑z : ℍ)).imJ = ((↑r : ℍ) * (↑z : ℍ)).imJ
a₃ : (r • (↑z : ℍ)).imK = ((↑r : ℍ) * (↑z : ℍ)).imK
⊢ r • (↑z : ℍ) = (↑r : ℍ) * (↑z : ℍ)

Tactic:
ext
-- Module: Mathlib.Analysis.Quaternion
Goal:
r : ℝ
z : ℂ
⊢ (r • (↑z : ℍ)).re = ((↑r : ℍ) * (↑z : ℍ)).re

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
r : ℝ
z : ℂ
⊢ (r • (↑z : ℍ)).imI = ((↑r : ℍ) * (↑z : ℍ)).imI

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
r : ℝ
z : ℂ
⊢ (r • (↑z : ℍ)).imJ = ((↑r : ℍ) * (↑z : ℍ)).imJ

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
r : ℝ
z : ℂ
⊢ (r • (↑z : ℍ)).imK = ((↑r : ℍ) * (↑z : ℍ)).imK

Tactic:
simp
-- Module: Mathlib.Analysis.Quaternion
Goal:
r : ℝ
⊢ (↑(↑r : ℂ) : ℍ) = (↑r : ℍ)

Tactic:
rfl

Premises used: Quaternion.coe, QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ (⇑ofComplex : (a : ℂ) → ℍ) = coeComplex

Tactic:
rfl

Premises used: Quaternion.coeComplex, rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
x : ℍ
rw :
  √(inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ)
              (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ) +
            inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ)
              (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ) +
          inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ)
            (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ) +
        inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)
          (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)) =
    √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)
⊢ norm (E := WithLp 2 (Fin 4 → ℝ)) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x) : WithLp 2 (Fin 4 → ℝ)) = ‖x‖

Tactic:
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply,
    Fin.sum_univ_four]

Premises used: Fin.sum_univ_four, Quaternion.normSq_def', Quaternion.inner_self, PiLp.inner_apply, norm_eq_sqrt_real_inner
-- Module: Mathlib.Analysis.Quaternion
Goal:
x : ℍ
simp_rw :
  √(HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 0 : ℝ) 2 +
            HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 1 : ℝ) 2 +
          HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 2 : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 3 : ℝ) 2) =
    √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)
⊢ √(inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ)
              (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 0 : ℝ) +
            inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ)
              (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 1 : ℝ) +
          inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ)
            (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 2 : ℝ) +
        inner ℝ (E := ℝ) (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)
          (WithLp.ofLp (p := 2) (WithLp.toLp 2 ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x)) 3 : ℝ)) =
    √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)

Tactic:
simp_rw [RCLike.inner_apply, starRingEnd_apply, star_trivial, ← sq]

Premises used: TrivialStar.star_trivial, sq, starRingEnd_apply, RCLike.inner_apply
-- Module: Mathlib.Analysis.Quaternion
Goal:
x : ℍ
⊢ √(HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 0 : ℝ) 2 +
            HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 1 : ℝ) 2 +
          HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 2 : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) ((equivTuple ℝ : (a : ℍ) → Fin 4 → ℝ) x 3 : ℝ) 2) =
    √(HPow.hPow (β := ℕ) x.re 2 + HPow.hPow (β := ℕ) x.imI 2 + HPow.hPow (β := ℕ) x.imJ 2 + HPow.hPow (β := ℕ) x.imK 2)

Tactic:
rfl
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (X := ℝ) (Y := ℍ) coe

Tactic:
continuous_algebraMap ℝ ℍ

Premises used: Quaternion.coe, Real, continuous_algebraMap, QuaternionAlgebra.coe, Quaternion
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (X := ℍ) (Y := ℝ) (⇑normSq : (a : ℍ) → ℝ)

Tactic:
simpa [← normSq_eq_norm_mul_self] using
    (continuous_norm.fun_mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)

Premises used: Quaternion.normSq_eq_norm_mul_self, continuous_norm, Continuous.fun_mul
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (Y := ℝ) fun (q : ℍ) ↦ q.re

Tactic:
(PiLp.continuous_apply 2 _ 0).comp linearIsometryEquivTuple.continuous

Premises used: Eq.mpr, Continuous.comp, Fin.cons, Fin.induction.go, Quaternion.linearIsometryEquivTuple, PiLp.continuous_apply, Fin.induction, Fin.cases, OfNat.ofNat, LinearIsometryEquiv.continuous, Matrix.vecCons
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (Y := ℝ) fun (q : ℍ) ↦ q.imI

Tactic:
(PiLp.continuous_apply 2 _ 1).comp linearIsometryEquivTuple.continuous

Premises used: Eq.mpr, Continuous.comp, Fin.cons, Fin.induction.go, Quaternion.linearIsometryEquivTuple, PiLp.continuous_apply, Fin.induction, Fin.cases, OfNat.ofNat, LinearIsometryEquiv.continuous, Matrix.vecCons
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (Y := ℝ) fun (q : ℍ) ↦ q.imJ

Tactic:
(PiLp.continuous_apply 2 _ 2).comp linearIsometryEquivTuple.continuous

Premises used: Eq.mpr, Continuous.comp, Fin.cons, Fin.induction.go, Quaternion.linearIsometryEquivTuple, PiLp.continuous_apply, Fin.induction, Fin.cases, OfNat.ofNat, LinearIsometryEquiv.continuous, Matrix.vecCons
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (Y := ℝ) fun (q : ℍ) ↦ q.imK

Tactic:
(PiLp.continuous_apply 2 _ 3).comp linearIsometryEquivTuple.continuous

Premises used: Eq.mpr, Continuous.comp, Fin.cons, Fin.induction.go, Quaternion.linearIsometryEquivTuple, PiLp.continuous_apply, Fin.induction, Fin.cases, OfNat.ofNat, LinearIsometryEquiv.continuous, Matrix.vecCons
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ Continuous (Y := ℍ) fun (q : ℍ) ↦ q.im

Tactic:
simpa only [← sub_re_self] using continuous_id.sub (continuous_coe.comp continuous_re)

Premises used: Continuous.comp, Quaternion.sub_re_self, continuous_id, Quaternion.continuous_coe, Continuous.sub, Quaternion.continuous_re
-- Module: Mathlib.Analysis.Quaternion
Goal:
⊢ CompleteSpace ℍ

Tactic:
haveI : IsUniformEmbedding linearIsometryEquivTuple.toLinearEquiv.toEquiv.symm :=
    linearIsometryEquivTuple.toContinuousLinearEquiv.symm.isUniformEmbedding
  (completeSpace_congr this).1 inferInstance

Premises used: ContinuousLinearEquiv.symm, completeSpace_congr, Quaternion.linearIsometryEquivTuple, inferInstance, ContinuousLinearEquiv.isUniformEmbedding, Iff.mp, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Quaternion
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
r : ℝ
h : HasSum (α := ℍ) (fun (a : α) ↦ (↑(f a) : ℍ)) (↑r : ℍ) L
⊢ HasSum f r L

Tactic:
simpa only using
    h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _ _) continuous_re

Premises used: HasSum.map, QuaternionAlgebra.reₗ, OfNat.ofNat, Neg.neg, Quaternion.continuous_re
-- Module: Mathlib.Analysis.Quaternion
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
r : ℝ
h : HasSum f r L
⊢ HasSum (α := ℍ) (fun (a : α) ↦ (↑(f a) : ℍ)) (↑r : ℍ) L

Tactic:
simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)

Premises used: HasSum.map, Real, Algebra.algebraMap, continuous_algebraMap, Quaternion
-- Module: Mathlib.Analysis.Quaternion
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
⊢ Summable (α := ℍ) (fun (a : α) ↦ (↑(f a) : ℍ)) L ↔ Summable f L

Tactic:
simpa only using
    Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from
      QuaternionAlgebra.reₗ _ _ _)
      (continuous_algebraMap _ _) continuous_re re_coe

Premises used: Real, Summable.map_iff_of_leftInverse, Algebra.algebraMap, continuous_algebraMap, QuaternionAlgebra.reₗ, Quaternion.re_coe, OfNat.ofNat, Neg.neg, Quaternion.continuous_re, Quaternion
-- Module: Mathlib.Analysis.Quaternion
Goal:
α : Type u_1
L : SummationFilter α
f : α → ℝ
⊢ Eq (α := ℍ) (∑'[L] (a : α), (↑(f a) : ℍ)) (↑(∑'[L] (a : α), f a) : ℍ)

Tactic:
(Function.LeftInverse.map_tsum f (continuous_algebraMap _ _) continuous_re re_coe).symm

Premises used: Quaternion.coe, Function.LeftInverse.map_tsum, continuous_algebraMap, QuaternionAlgebra.coe, Quaternion.re_coe, tsum, Eq.symm, Quaternion.continuous_re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ (↑x : K) = HSMul.hSMul (β := K) x 1

Tactic:
Algebra.algebraMap_eq_smul_one x

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
⊢ r • z = (↑r : K) * z

Tactic:
Algebra.smul_def r z

Premises used: Algebra.smul_def
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ K E
r : ℝ
x : E
rw : r • x = HSMul.hSMul (β := K) r 1 • x
rw₁ rw₂ : r • x = r • x
⊢ r • x = HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑r : K) x

Tactic:
rw [RCLike.ofReal_alg, smul_one_smul]

Premises used: RCLike.ofReal_alg, smul_one_smul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := (a : ℝ) → K) (⇑(algebraMap ℝ K) : (a : ℝ) → K) ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I = z

Tactic:
RCLike.re_add_im_ax z

Premises used: RCLike.re_add_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ ∀ (r : ℝ), (re : (a : K) → ℝ) (↑r : K) = r

Tactic:
RCLike.ofReal_re_ax

Premises used: RCLike.ofReal_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ ∀ (r : ℝ), Eq (α := ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ) (0 : ℝ)

Tactic:
RCLike.ofReal_im_ax

Premises used: RCLike.ofReal_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ ∀ (z w : K),
    (re : (a : K) → ℝ) (z * w) =
      HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)

Tactic:
RCLike.mul_re_ax

Premises used: RCLike.mul_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ ∀ (z w : K),
    (im : (a : K) → ℝ) (z * w) =
      HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)

Tactic:
RCLike.mul_im_ax

Premises used: RCLike.mul_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ z = w ↔
    Eq (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)

Tactic:
⟨fun h => h ▸ ⟨rfl, rfl⟩, fun ⟨h₁, h₂⟩ => re_add_im z ▸ re_add_im w ▸ h₁ ▸ h₂ ▸ rfl⟩

Premises used: RCLike.re_add_im, Eq.rec, _private.0.RCLike.ext_iff.match_1, And.intro, Iff.intro, Eq, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
hre : Eq (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
him : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
⊢ z = w

Tactic:
ext_iff.2 ⟨hre, him⟩

Premises used: Iff.mpr, RCLike.ext_iff, And.intro
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K) (↑0 : K) 0

Tactic:
algebraMap.coe_zero

Premises used: algebraMap.coe_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
map_zero re

Premises used: map_zero, RCLike.re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
map_zero im

Premises used: map_zero, RCLike.im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K) (↑1 : K) 1

Tactic:
map_one (algebraMap ℝ K)

Premises used: Real, Algebra.algebraMap, map_one
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑1 : K) : ℝ) (1 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
rw [← ofReal_one, ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.ofReal_one
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑1 : K) : ℝ) (0 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) 1 : ℝ) (0 : ℝ)

Tactic:
rw [← ofReal_one, ofReal_im]

Premises used: RCLike.ofReal_im, RCLike.ofReal_one
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Function.Injective.{1, u_1 + 1} (β := K) ofReal

Tactic:
(algebraMap ℝ K).injective

Premises used: Real, Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑z : K) (↑w : K) ↔ z = w

Tactic:
algebraMap.coe_inj _ _

Premises used: algebraMap.coe_inj