awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (β := ℝ) (fun (x_1 : ℝ) ↦ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖) univ u
hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
⊢ ∃ (z : ℝ × ℝ), IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) univ z
have inr : ∀
  (hu :
    ∀ (x_1 : ℝ),
      ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖ ≤
        ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖),
  ∃ (z : ℝ × ℝ), ∀ (x_1 : ℝ × ℝ), ‖φ x z‖ ≤ ‖φ x x_1‖
Tactic: simp only [isMinOn_univ_iff] at hu ⊢
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
x : F
u : ℝ
hc₀ : 0 < ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖
hu :
  ∀ (x_1 : ℝ),
    ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) u : F)‖ ≤
      ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) x_1 : F)‖
⊢ ∃ (z : ℝ × ℝ), ∀ (x_1 : ℝ × ℝ), ‖φ x z‖ ≤ ‖φ x x_1‖
have inr : Bornology.IsBounded (α := ℝ × ℝ) {x_1 : ℝ × ℝ | ‖φ x x_1‖ ≤ ‖φ x (0, 0)‖}
Tactic: refine (continuous_φ x).norm.exists_forall_le_of_isBounded (0, 0) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
⊢ ∃ (p : ℝ[X]), p.IsMonicOfDegree 2 ∧ Eq (α := F) ((aeval x : (a : ℝ[X]) → F) p : F) (0 : F)
have obtain : ∀ (z : ℝ × ℝ) (h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z),
  ∃ (p : ℝ[X]), p.IsMonicOfDegree 2 ∧ Eq (α := F) ((aeval x : (a : ℝ[X]) → F) p : F) (0 : F)
Tactic: obtain ⟨z, h⟩ := exists_isMinOn_norm_φ x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
⊢ ∃ (p : ℝ[X]), p.IsMonicOfDegree 2 ∧ Eq (α := F) ((aeval x : (a : ℝ[X]) → F) p : F) (0 : F)
have suffices : φ x z = 0
Tactic: suffices φ x z = 0 from ⟨_, isMonicOfDegree_sub_add_two z.1 z.2, by rwa [aeval_eq_φ]⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
⊢ φ x z = 0
have by_contra! : ∀ (H : φ x z ≠ 0), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
have rw : ‖φ x z‖ ≤
  ‖HPow.hPow (β := ℕ) x 2 - HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) +
      HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2‖
Tactic: rw [← sq_le_sq₀ M.sqrt_nonneg (norm_nonneg _), Real.sq_sqrt (norm_nonneg _), ← norm_pow,
      Commute.sub_sq <| algebraMap_eq_smul_one (A := F) r ▸ commute_algebraMap_right r x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ ‖φ x z‖ ≤
    ‖HPow.hPow (β := ℕ) x 2 - HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) +
        HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2‖
have h₁ : HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) = (2 * r, HPow.hPow (β := ℕ) r 2).1 • x
Tactic: convert! isMinOn_univ_iff.mp h (2 * r, r ^ 2) using 4
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
h₁ : HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) = (2 * r, HPow.hPow (β := ℕ) r 2).1 • x
⊢ ‖φ x z‖ ≤
    ‖HPow.hPow (β := ℕ) x 2 - HMul.hMul (β := F) (2 * x) ((algebraMap ℝ F : (a : ℝ) → F) r : F) +
        HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2‖
have h₂ : HPow.hPow (α := F) (β := ℕ) ((algebraMap ℝ F : (a : ℝ) → F) r : F) 2 =
  (algebraMap ℝ F : (a : ℝ) → F) (2 * r, HPow.hPow (β := ℕ) r 2).2
Tactic: convert! isMinOn_univ_iff.mp h (2 * r, r ^ 2) using 4
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
⊢ False
have h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
Tactic: have h' (r : ℝ) : √M ≤ ‖x - algebraMap ℝ F r‖ := by
    rw [← sq_le_sq₀ M.sqrt_nonneg (norm_nonneg _), Real.sq_sqrt (norm_nonneg _), ← norm_pow,
      Commute.sub_sq <| algebraMap_eq_smul_one (A := F) r ▸ commute_algebraMap_right r x]
    convert! isMinOn_univ_iff.mp h (2 * r, r ^ 2) using 4 <;>
      simp [two_mul, add_mul, ← commutes, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
⊢ False
have this : Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
Tactic: have := tendsto_norm_atTop_iff_cobounded.mpr <| tendsto_φ_cobounded (by positivity) h'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormedAlgebra ℝ F
inst_2 : NormOneClass F
inst_3 : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖HSub.hSub (β := F) x ((algebraMap ℝ F : (a : ℝ) → F) r : F)‖
this : Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x x_1‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ False
have this₁ : Filter.Tendsto (β := ℝ) (fun (x_1 : ℝ × ℝ) ↦ ‖φ x z‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
Tactic: simp only [norm_φ_eq_norm_φ_of_isMinOn h (norm_ne_zero_iff.mpr H)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
⊢ Algebra.IsAlgebraic ℝ F
have refine : ∀ (x : F), IsAlgebraic ℝ x
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (goal)
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
x : F
⊢ IsAlgebraic ℝ x
have obtain : ∀ (f : ℝ[X]) (hf : f.IsMonicOfDegree 2) (hfx : Eq (α := F) ((aeval x : (a : ℝ[X]) → F) f : F) (0 : F)), IsAlgebraic ℝ x
Tactic: obtain ⟨f, hf, hfx⟩ := exists_isMonicOfDegree_two_and_aeval_eq_zero x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.GelfandMazur (hypothesis)
Goal:
F : Type u_2
inst : NormedField F
inst_1 : NormedAlgebra ℝ F
⊢ Nonempty.{max 1 (u_2 + 1)} (F ≃ₐ[ℝ] ℝ) ∨ Nonempty.{max 1 (u_2 + 1)} (F ≃ₐ[ℝ] ℂ)
have this : Algebra.IsAlgebraic ℝ F
Tactic: have : Algebra.IsAlgebraic ℝ F := by
    refine ⟨fun x ↦ ?_⟩
    obtain ⟨f, hf, hfx⟩ := exists_isMonicOfDegree_two_and_aeval_eq_zero x
    exact ⟨f, hf.ne_zero, hfx⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 : Algebra ℚ 𝔸
v : m → 𝔸
⊢ exp (diagonal v) = diagonal (exp v)
have simp_rw : Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal v ^ n))
  (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
Tactic: simp_rw [exp_eq_tsum_rat, diagonal_pow, ← diagonal_smul, ← diagonal_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 : Algebra ℚ 𝔸
v : m → 𝔸
simp_rw :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal v ^ n))
    (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
⊢ exp (diagonal v) = diagonal (exp v)
have simp_rw₁ : Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal (v ^ n)))
  (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
Tactic: simp_rw [exp_eq_tsum_rat, diagonal_pow, ← diagonal_smul, ← diagonal_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 : Algebra ℚ 𝔸
v : m → 𝔸
simp_rw :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal v ^ n))
    (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
simp_rw₁ :
  Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (diagonal (v ^ n)))
    (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
⊢ exp (diagonal v) = diagonal (exp v)
have simp_rw₂ : Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), diagonal (HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
  (diagonal (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (v ^ n)))
Tactic: simp_rw [exp_eq_tsum_rat, diagonal_pow, ← diagonal_smul, ← diagonal_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
Goal:
m : Type u_1
n : Type u_2
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Ring 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
inst_7 : T2Space 𝔸
inst_8 : Algebra ℚ 𝔸
v : m → Matrix n n 𝔸
⊢ exp (blockDiagonal v) = blockDiagonal (exp v)
have simp_rw : Eq (α := Matrix (n × m) (n × m) 𝔸) (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal v ^ n_1))
  (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
Tactic: simp_rw [exp_eq_tsum_rat, ← blockDiagonal_pow, ← blockDiagonal_smul, ← blockDiagonal_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
Goal:
m : Type u_1
n : Type u_2
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Ring 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
inst_7 : T2Space 𝔸
inst_8 : Algebra ℚ 𝔸
v : m → Matrix n n 𝔸
simp_rw :
  Eq (α := Matrix (n × m) (n × m) 𝔸) (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal v ^ n_1))
    (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
⊢ exp (blockDiagonal v) = blockDiagonal (exp v)
have simp_rw₁ : Eq (α := Matrix (n × m) (n × m) 𝔸) (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal (v ^ n_1)))
  (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
Tactic: simp_rw [exp_eq_tsum_rat, ← blockDiagonal_pow, ← blockDiagonal_smul, ← blockDiagonal_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
Goal:
m : Type u_1
n : Type u_2
𝔸 : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Ring 𝔸
inst_5 : TopologicalSpace 𝔸
inst_6 : IsTopologicalRing 𝔸
inst_7 : T2Space 𝔸
inst_8 : Algebra ℚ 𝔸
v : m → Matrix n n 𝔸
simp_rw :
  Eq (α := Matrix (n × m) (n × m) 𝔸) (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal v ^ n_1))
    (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
simp_rw₁ :
  Eq (α := Matrix (n × m) (n × m) 𝔸)
    (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (blockDiagonal (v ^ n_1)))
    (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
⊢ exp (blockDiagonal v) = blockDiagonal (exp v)
have simp_rw₂ : Eq (α := Matrix (n × m) (n × m) 𝔸) (∑' (n_1 : ℕ), blockDiagonal (HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
  (blockDiagonal (∑' (n_1 : ℕ), HSMul.hSMul (α := ℚ) (↑n_1.factorial : ℚ)⁻¹ (v ^ n_1)))
Tactic: simp_rw [exp_eq_tsum_rat, ← blockDiagonal_pow, ← blockDiagonal_smul, ← blockDiagonal_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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) 𝔸
⊢ exp (blockDiagonal' (m' := n') (n' := n') v) = blockDiagonal' (m' := n') (n' := n') (exp v)
have 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)))
Tactic: simp_rw [exp_eq_tsum_rat, ← blockDiagonal'_pow, ← blockDiagonal'_smul, ← blockDiagonal'_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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)))
⊢ exp (blockDiagonal' (m' := n') (n' := n') v) = blockDiagonal' (m' := n') (n' := n') (exp v)
have 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)))
Tactic: simp_rw [exp_eq_tsum_rat, ← blockDiagonal'_pow, ← blockDiagonal'_smul, ← blockDiagonal'_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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)))
⊢ exp (blockDiagonal' (m' := n') (n' := n') v) = blockDiagonal' (m' := n') (n' := n') (exp v)
have 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)))
Tactic: simp_rw [exp_eq_tsum_rat, ← blockDiagonal'_pow, ← blockDiagonal'_smul, ← blockDiagonal'_tsum]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 𝔸
⊢ exp Aᵀ = (exp A)ᵀ
have simp_rw : Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (Aᵀ ^ n))
  (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (A ^ n))ᵀ
Tactic: simp_rw [exp_eq_tsum_rat, transpose_tsum, transpose_smul, transpose_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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))ᵀ
⊢ exp Aᵀ = (exp A)ᵀ
have simp_rw₁ : Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (Aᵀ ^ n))
  (∑' (x : ℕ), (HSMul.hSMul (α := ℚ) (↑x.factorial : ℚ)⁻¹ (A ^ x))ᵀ)
Tactic: simp_rw [exp_eq_tsum_rat, transpose_tsum, transpose_smul, transpose_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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))ᵀ)
⊢ exp Aᵀ = (exp A)ᵀ
have simp_rw₂ : Eq (α := Matrix m m 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n.factorial : ℚ)⁻¹ (Aᵀ ^ n))
  (∑' (x : ℕ), HSMul.hSMul (α := ℚ) (↑x.factorial : ℚ)⁻¹ (A ^ x)ᵀ)
Tactic: simp_rw [exp_eq_tsum_rat, transpose_tsum, transpose_smul, transpose_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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) = (exp A)⁻¹
have rw : exp (-A) = Ring.inverse (exp A)
Tactic: rw [nonsing_inv_eq_ringInverse]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 𝔸
⊢ exp (z • A) = exp A ^ z
have inl : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = HPow.hPow (β := ℤ) (exp A) (↑n : ℤ)
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 : ℤ)
⊢ exp (z • A) = exp A ^ z
have inr : ∀ (n : ℕ), exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 : ℕ
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = HPow.hPow (β := ℤ) (exp A) (↑n : ℤ)
have inl : exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = exp A ^ n
Tactic: rw [zpow_natCast, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = HPow.hPow (β := ℤ) (exp A) (↑n : ℤ)
have inl₁ : exp (n • A) = exp A ^ n
Tactic: rw [zpow_natCast, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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
⊢ exp (HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = HPow.hPow (β := ℤ) (exp A) (↑n : ℤ)
have inl₂ : exp A ^ n = exp A ^ n
Tactic: rw [zpow_natCast, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (hypothesis)
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 : ℕ
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have this : IsUnit (exp A).det
Tactic: have : IsUnit (exp A).det := (Matrix.isUnit_iff_isUnit_det _).mp (isUnit_exp _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have inr : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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 : ℤ))⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have inr₁ : exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = (exp A ^ n)⁻¹
Tactic: rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.MatrixExponential (goal)
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)⁻¹
⊢ exp (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) A) = HPow.hPow (β := ℤ) (exp A) (-(↑n : ℤ))
have inr₂ : exp (-HSMul.hSMul (α := ℤ) (↑n : ℤ) A) = (exp A ^ n)⁻¹
Tactic: rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]