awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
n' : m → Type u_3
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : (i : m) → Fintype (n' i)
inst_3 : (i : m) → DecidableEq (n' i)
inst_4 : Ring 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
inst_7 : T2Space 𝔸
inst_8 : Algebra ℚ 𝔸
v : (i : m) → Matrix.{u_3, u_3, u_5} (n' i) (n' i) 𝔸
simp_rw :
  Eq (α := Matrix ((i : m) × n' i) ((i : m) × n' i) 𝔸)
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (blockDiagonal' (m' := n') (n' := n') v ^ n))
    (blockDiagonal' (m' := n') (n' := n') (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
simp_rw₁ :
  Eq (α := Matrix ((i : m) × n' i) ((i : m) × n' i) 𝔸)
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (blockDiagonal' (m' := n') (n' := n') (v ^ n)))
    (blockDiagonal' (m' := n') (n' := n') (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
simp_rw₂ :
  Eq (α := Matrix ((i : m) × n' i) ((i : m) × n' i) 𝔸)
    (∑' (n : ℕ), blockDiagonal' (m' := n') (n' := n') (HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
    (blockDiagonal' (m' := n') (n' := n') (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
⊢ exp (blockDiagonal' (m' := n') (n' := n') v) = blockDiagonal' (m' := n') (n' := n') (exp v)

Tactic:
simp_rw [exp_eq_tsum_rat, ← blockDiagonal'_pow, ← blockDiagonal'_smul, ← blockDiagonal'_tsum]

Premises used: NormedSpace.exp_eq_tsum_rat, Matrix.blockDiagonal'_tsum, Matrix.blockDiagonal'_smul, Matrix.blockDiagonal'_pow
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Ring 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : T2Space 𝔸
inst_6 : StarRing 𝔸
inst_7 : ContinuousStar 𝔸
A : Matrix m m 𝔸
⊢ exp Aᴴ = (exp A)ᴴ

Tactic:
(star_exp A).symm

Premises used: NormedSpace.star_exp, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Ring 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : T2Space 𝔸
inst_6 : StarRing 𝔸
inst_7 : ContinuousStar 𝔸
A : Matrix m m 𝔸
h : A.IsHermitian
⊢ (NormedSpace.exp A).IsHermitian

Tactic:
(exp_conjTranspose _).symm.trans <| congr_arg _ h

Premises used: Matrix.exp_conjTranspose, congr_arg, Matrix.IsHermitian, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
α : Type u_4
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Ring 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : T2Space 𝔸
inst_6 : LinearOrder α
inst_7 : Algebra ℚ 𝔸
M : Matrix m m 𝔸
b : m → α
hM : M.BlockTriangular b
⊢ (NormedSpace.exp M).BlockTriangular b

Tactic:
exp_mem (s := blockTriangularSubalgebra ℚ _ b) isClosed_setOf_blockTriangular hM

Premises used: Set.Mem, setOf, NormedSpace.exp_mem, Matrix.BlockTriangular, isClosed_setOf_blockTriangular
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
inst_6 : T2Space 𝔸
A : Matrix m m 𝔸
simp_rw :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (Aᵀ ^ n))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (A ^ n))ᵀ
simp_rw₁ :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (Aᵀ ^ n))
    (∑' (x : ℕ), (HSMul.hSMul (α := ℚ) (↑x.factorial : ℚ)⁻¹ (A ^ x))ᵀ)
simp_rw₂ :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (Aᵀ ^ n))
    (∑' (x : ℕ), HSMul.hSMul (α := ℚ) (↑x.factorial : ℚ)⁻¹ (A ^ x)ᵀ)
⊢ exp Aᵀ = (exp A)ᵀ

Tactic:
simp_rw [exp_eq_tsum_rat, transpose_tsum, transpose_smul, transpose_pow]

Premises used: Matrix.transpose_tsum, Matrix.transpose_pow, Matrix.transpose_smul, NormedSpace.exp_eq_tsum_rat
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
inst_6 : T2Space 𝔸
A : Matrix m m 𝔸
h : A.IsSymm
⊢ (NormedSpace.exp A).IsSymm

Tactic:
(exp_transpose _).symm.trans <| congr_arg _ h

Premises used: Matrix.exp_transpose, congr_arg, Matrix.IsSymm, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
⊢ exp (A + B) = exp A * exp B

Tactic:
open scoped Norms.Operator in exp_add_of_commute h

Premises used: Matrix, instTopologicalSpaceMatrix._aux_1, NormedSpace.exp_add_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
ι : Type u_6
s : Finset ι
f : ι → Matrix m m 𝔸
h : (↑s : Set ι).Pairwise (Commute on f)
⊢ Eq (α := Matrix m m 𝔸) (exp (∑ i ∈ s, f i)) (s.noncommProd (fun (i : ι) ↦ exp (f i)) ⋯)

Tactic:
open scoped Norms.Operator in exp_sum_of_commute s f h

Premises used: instTopologicalSpaceMatrix._aux_1, NormedSpace.exp_sum_of_commute
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
⊢ exp (n • A) = exp A ^ n

Tactic:
open scoped Norms.Operator in exp_nsmul n A

Premises used: NormedSpace.exp_nsmul, instTopologicalSpaceMatrix._aux_1
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ IsUnit (exp A)

Tactic:
open scoped Norms.Operator in isUnit_exp A

Premises used: instTopologicalSpaceMatrix._aux_1, NormedSpace.isUnit_exp
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
⊢ exp ((↑U : Matrix m m 𝔸) * A * (↑U⁻¹ : Matrix m m 𝔸)) = (↑U : Matrix m m 𝔸) * exp A * (↑U⁻¹ : Matrix m m 𝔸)

Tactic:
open scoped Norms.Operator in exp_units_conj U A

Premises used: instTopologicalSpaceMatrix._aux_1, NormedSpace.exp_units_conj
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
U : (Matrix m m 𝔸)ˣ
A : Matrix m m 𝔸
⊢ exp ((↑U⁻¹ : Matrix m m 𝔸) * A * (↑U : Matrix m m 𝔸)) = (↑U⁻¹ : Matrix m m 𝔸) * exp A * (↑U : Matrix m m 𝔸)

Tactic:
exp_units_conj U⁻¹ A

Premises used: Inv.inv, Matrix.exp_units_conj
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
rw : exp (-A) = Ring.inverse (exp A)
⊢ exp (-A) = (exp A)⁻¹

Tactic:
rw [nonsing_inv_eq_ringInverse]

Premises used: Matrix.nonsing_inv_eq_ringInverse
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp (-A) = Ring.inverse (exp A)

Tactic:
(Ring.inverse_exp A).symm

Premises used: instTopologicalSpaceMatrix._aux_1, Eq.symm, Ring.inverse_exp
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp (-A) = Ring.inverse (exp A)

Tactic:
exact (Ring.inverse_exp A).symm
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp (-A) = Ring.inverse (exp A)

Tactic:
open scoped Norms.Operator in exact (Ring.inverse_exp A).symm
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
z : ℤ
A : Matrix m m 𝔸
inl : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = HPow.hPow (β := ℤ) (exp A) (↑n : ℤ)
inr : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
⊢ exp (z • A) = exp A ^ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
inl : exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = exp A ^ n
inl₁ : exp (n • A) = exp A ^ n
inl₂ inl₃ : exp A ^ n = exp A ^ n
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = HPow.hPow (β := ℤ) (exp A) (↑n : ℤ)

Tactic:
rw [zpow_natCast, natCast_zsmul, exp_nsmul]

Premises used: zpow_natCast, Matrix.exp_nsmul, natCast_zsmul
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ IsUnit (exp A).det

Tactic:
have : IsUnit (exp A).det := (Matrix.isUnit_iff_isUnit_det _).mp (isUnit_exp _)
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp A).det
inr : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (HPow.hPow (β := ℤ) (exp A) (↑n : ℤ))⁻¹
inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (exp A ^ n)⁻¹
inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = (exp A ^ n)⁻¹
inr₃ : (exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A))⁻¹ = (exp A ^ n)⁻¹
inr₄ : (exp (n • A))⁻¹ = (exp A ^ n)⁻¹
inr₅ inr₆ : (exp A ^ n)⁻¹ = (exp A ^ n)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))

Tactic:
rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]

Premises used: zpow_natCast, neg_smul, Matrix.exp_neg, Matrix.exp_nsmul, Matrix.zpow_neg, natCast_zsmul
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
U A : Matrix m m 𝔸
hy : IsUnit U
u : (Matrix m m 𝔸)ˣ
hu : (↑u : Matrix m m 𝔸) = U
⊢ exp ((↑u : Matrix m m 𝔸) * A * (↑u : Matrix m m 𝔸)⁻¹) = (↑u : Matrix m m 𝔸) * exp A * (↑u : Matrix m m 𝔸)⁻¹

Tactic:
simpa only [Matrix.coe_units_inv] using exp_units_conj u A

Premises used: Matrix.coe_units_inv, Matrix.exp_units_conj
-- Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Goal:
m : Type u_1
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NormedCommRing 𝔸
inst_3 : NormedAlgebra ℚ 𝔸
inst_4 : CompleteSpace 𝔸
U A : Matrix m m 𝔸
hy : IsUnit U
u : (Matrix m m 𝔸)ˣ
hu : (↑u : Matrix m m 𝔸) = U
⊢ exp ((↑u : Matrix m m 𝔸)⁻¹ * A * (↑u : Matrix m m 𝔸)) = (↑u : Matrix m m 𝔸)⁻¹ * exp A * (↑u : Matrix m m 𝔸)

Tactic:
simpa only [Matrix.coe_units_inv] using exp_units_conj' u A

Premises used: Matrix.coe_units_inv, Matrix.exp_units_conj'
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
r : ℝ
⊢ Eq (α := ℍ) (exp (↑r : ℍ)) (↑(exp r) : ℍ)

Tactic:
(map_exp (algebraMap ℝ ℍ[ℝ]) (continuous_algebraMap _ _) _).symm

Premises used: Quaternion.coe, Real, Algebra.algebraMap, NormedSpace.map_exp, continuous_algebraMap, QuaternionAlgebra.coe, Eq.symm, Quaternion
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
rw :
  HSMul.hSMul (α := ℝ) (↑(2 * n)! : ℝ)⁻¹ (q ^ (2 * n)) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)
⊢ Eq (α := ℍ) ((expSeries ℝ ℍ (2 * n) : (a : (i : Fin (2 * n)) → ℍ) → ℍ) fun (x : Fin (2 * n)) ↦ q)
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)

Tactic:
rw [expSeries_apply_eq]

Premises used: NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
⊢ HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)

Tactic:
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
rw : k⁻¹ • HPow.hPow (β := ℕ) q 2 ^ n = k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
rw₁ rw₂ :
  k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
    k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n
⊢ k⁻¹ • q ^ (2 * n) = k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n

Tactic:
rw [pow_mul, hq2]

Premises used: pow_mul
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
    HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)

Tactic:
?_
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / k) : ℍ)

Tactic:
?_
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_1 :
  k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
    HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
calc_2 :
  HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / k) : ℍ)
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n)! : ℝ)⁻¹ (q ^ (2 * n)) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / (↑(2 * n)! : ℝ)) : ℍ)

Tactic:
calc
    k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]
    _ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_
    _ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_

Premises used: Norm.norm, HMul.hMul, Quaternion.normSq, HDiv.hDiv, HPow.hPow, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_1 :
  HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n = (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)
⊢ k⁻¹ • HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n =
    HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_1 :
  HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n =
    (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ)
⊢ HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n = (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ)

Tactic:
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq]

Premises used: Quaternion.normSq_eq_norm_mul_self, sq, pow_mul, neg_pow
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_1 :
  HPow.hPow (α := ℍ) (-1) n * HMul.hMul (α := ℍ) (↑‖q‖ : ℍ) (↑‖q‖ : ℍ) ^ n =
    HPow.hPow (α := ℍ) (-1) n * HMul.hMul (α := ℍ) (↑‖q‖ : ℍ) (↑‖q‖ : ℍ) ^ n
⊢ HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n =
    (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ HPow.hPow (α := ℍ) (-1) n * HMul.hMul (α := ℍ) (↑‖q‖ : ℍ) (↑‖q‖ : ℍ) ^ n =
    HPow.hPow (α := ℍ) (-1) n * HMul.hMul (α := ℍ) (↑‖q‖ : ℍ) (↑‖q‖ : ℍ) ^ n

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_2 :
  HMul.hMul (α := ℍ) (↑k⁻¹ : ℍ) (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)
⊢ HSMul.hSMul (β := ℍ) k⁻¹ (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) / k) : ℍ)

Tactic:
rw [← coe_mul_eq_smul, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Quaternion.coe_mul_eq_smul
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
calc_2 :
  Eq (α := ℍ) (↑(k⁻¹ * ((↑(Int.negSucc 0 ^ n) : ℝ) * ‖q‖ ^ (2 * n))) : ℍ)
    (↑((↑(Int.negSucc 0 ^ n) : ℝ) * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)
⊢ HMul.hMul (α := ℍ) (↑k⁻¹ : ℍ) (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) : ℍ) =
    (↑(HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
k : ℝ := (↑(2 * n)! : ℝ)
⊢ Eq (α := ℍ) (↑(k⁻¹ * ((↑(Int.negSucc 0 ^ n) : ℝ) * ‖q‖ ^ (2 * n))) : ℍ)
    (↑((↑(Int.negSucc 0 ^ n) : ℝ) * ‖q‖ ^ (2 * n) * k⁻¹) : ℍ)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
rw :
  HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
⊢ ((expSeries ℝ ℍ (2 * n + 1) : (a : (i : Fin (2 * n + 1)) → ℍ) → ℍ) fun (x : Fin (2 * n + 1)) ↦ q) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q

Tactic:
rw [expSeries_apply_eq]

Premises used: NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
inl :
  ∀ (hq : Eq (α := ℝ) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0) 0),
    HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (HPow.hPow (α := ℍ) 0 (2 * n + 1)) =
      HSMul.hSMul (β := ℍ)
        (HPow.hPow (α := ℝ) (-1) n * norm (E := ℍ) 0 ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / norm (E := ℍ) 0) 0
inr :
  ∀ (hq0 : q ≠ 0),
    HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
      (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q

Tactic:
obtain rfl | hq0 := eq_or_ne q 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
n : ℕ
hq : Eq (α := ℝ) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0) 0
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (HPow.hPow (α := ℍ) 0 (2 * n + 1)) =
    HSMul.hSMul (β := ℍ)
      (HPow.hPow (α := ℝ) (-1) n * norm (E := ℍ) 0 ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / norm (E := ℍ) 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
⊢ HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)

Tactic:
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
⊢ ‖q‖ ≠ 0

Tactic:
have hqn := norm_ne_zero_iff.mpr hq0
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
rw : k⁻¹ • (q ^ (2 * n) * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
rw₁ : k⁻¹ • (HPow.hPow (β := ℕ) q 2 ^ n * q) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
rw₂ rw₃ :
  k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
    k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)
⊢ k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q)

Tactic:
rw [pow_succ, pow_mul, hq2]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
⊢ k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
    k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q

Tactic:
?_
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
⊢ k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
?_
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr :
  k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
    k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
inr₁ :
  k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
⊢ HSMul.hSMul (α := ℝ) (↑(2 * n + 1)! : ℝ)⁻¹ (q ^ (2 * n + 1)) =
    (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n + 1) / (↑(2 * n + 1)! : ℝ) / ‖q‖) • q

Tactic:
calc
    k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) := by rw [pow_succ, pow_mul, hq2]
    _ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_
    _ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_

Premises used: Quaternion.coe, Norm.norm, HMul.hMul, Quaternion.normSq, HDiv.hDiv, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr :
  HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q
⊢ k⁻¹ • (HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q) =
    k⁻¹ • (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q

Tactic:
congr 1
-- Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Goal:
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : HPow.hPow (β := ℕ) q 2 = -(↑((normSq : (a : ℍ) → ℝ) q) : ℍ)
hqn : ‖q‖ ≠ 0
k : ℝ := (↑(2 * n + 1)! : ℝ)
inr :
  HPow.hPow (α := ℍ) (-1) n * HPow.hPow (α := ℍ) (↑(‖q‖ * ‖q‖) : ℍ) n * q =
    (↑(HPow.hPow (α := ℝ) (-1) n * (‖q‖ * ‖q‖) ^ n) : ℍ) * q
⊢ HPow.hPow (α := ℍ) (-(↑((normSq : (a : ℍ) → ℝ) q) : ℍ) : ℍ) n * q = (HPow.hPow (α := ℝ) (-1) n * ‖q‖ ^ (2 * n)) • q

Tactic:
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]

Premises used: Quaternion.normSq_eq_norm_mul_self, sq, pow_mul, Quaternion.coe_mul_eq_smul, neg_pow