Physlib.SpaceAndTime.SpaceTime.Boosts

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.LorentzGroup.Boosts.Basic
public import Physlib.SpaceAndTime.SpaceTime.Basic

Boosts of space time

i. Overview

In this module we consider boosts acting on points in space time,and recover simple formulae for such applications.

Note that the material here currently assumes that the speed of light c = 1.

ii. Key results

boost_x_smul : The action of a boost in the x-direction on a point in space time.

iii. Table of contents

A. The action of a boost in the x-direction

iv. References

See e.g.

https://en.wikipedia.org/wiki/Lorentz_transformation

@[expose] public section

A. The action of a boost in the x-direction

We show that boosting in the x-direction takes (t, x, y, z) to (γ (t - β x), γ (x - β t), y, z).

lemma boost_x_smul (β : ℝ) (hβ : |β| < 1) (x : SpaceTime) :
    LorentzGroup.boost (d := 3) 0 β hβ • x =
      fun | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
          | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
          | Sum.inr 1=> x (Sum.inr 1)
          | Sum.inr 2=> x (Sum.inr 2) := byβ:ℝhβ:|β| < 1x:SpaceTime⊢ boost 0 β hβ • x = fun x_1 =>
  match x_1 with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)
  funext iβ:ℝhβ:|β| < 1x:SpaceTimei:Fin 1 ⊕ Fin 3⊢ (boost 0 β hβ • x) i =
  match i with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)
  fin_cases i«0»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  match Sum.inl ((fun i => i) ⟨0, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)«1»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  match Sum.inr ((fun i => i) ⟨0, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)«2»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  match Sum.inr ((fun i => i) ⟨1, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)«3»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  match Sum.inr ((fun i => i) ⟨2, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2) <;>«0»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  match Sum.inl ((fun i => i) ⟨0, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)«1»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  match Sum.inr ((fun i => i) ⟨0, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)«2»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  match Sum.inr ((fun i => i) ⟨1, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)«3»β:ℝhβ:|β| < 1x:SpaceTime⊢ (boost 0 β hβ • x) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  match Sum.inr ((fun i => i) ⟨2, ⋯⟩) with
  | Sum.inl 0 => γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))
  | Sum.inr 0 => γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
  | Sum.inr 1 => x (Sum.inr 1)
  | Sum.inr 2 => x (Sum.inr 2)
    simp [Lorentz.Vector.smul_eq_sum, Fin.sum_univ_three, boost_inl_0_inr_other,
      boost_inr_other_inr, boost_inr_inr_other, boost_inr_other_inl_0]All goals completed! 🐙 <;>«0»β:ℝhβ:|β| < 1x:SpaceTime⊢ γ β * x (Sum.inl 0) + -(γ β * β * x (Sum.inr 0)) = γ β * (x (Sum.inl 0) - β * x (Sum.inr 0))«1»β:ℝhβ:|β| < 1x:SpaceTime⊢ -(γ β * β * x (Sum.inl 0)) + γ β * x (Sum.inr 0) = γ β * (x (Sum.inr 0) - β * x (Sum.inl 0))
    ringAll goals completed! 🐙



lemma boost_zero_apply_time_space {d : ℕ} {β : ℝ} (hβ : |β| < 1) (c : SpeedOfLight)
    (t : Time) (x : Space d.succ) :
    ((boost (0 : Fin d.succ) β hβ)⁻¹ • (SpaceTime.toTimeAndSpace c).symm (t, x)) =
    (SpaceTime.toTimeAndSpace c).symm
    (γ β * (t.val + β /c * x 0),
    ⟨fun
      | (0 : Fin d.succ) => γ β * (x 0 + c * β * t.val)
      | ⟨Nat.succ n, ih⟩ => x ⟨Nat.succ n, ih⟩⟩) := byd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succ⊢ (boost 0 β hβ)⁻¹ • (toTimeAndSpace c).symm (t, x) =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
  funext μd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ((boost 0 β hβ)⁻¹ • (toTimeAndSpace c).symm (t, x)) μ =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
    μ
  rw [boost_inverse,d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ (boost 0 (-β) ⋯ • (toTimeAndSpace c).symm (t, x)) μ =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
    μd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ∑ j, ↑(boost 0 (-β) ⋯) μ j * (toTimeAndSpace c).symm (t, x) j =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
    μ Lorentz.Vector.smul_eq_sumd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ∑ j, ↑(boost 0 (-β) ⋯) μ j * (toTimeAndSpace c).symm (t, x) j =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
    μd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ∑ j, ↑(boost 0 (-β) ⋯) μ j * (toTimeAndSpace c).symm (t, x) j =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
    μ]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ∑ j, ↑(boost 0 (-β) ⋯) μ j * (toTimeAndSpace c).symm (t, x) j =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })
    μ
  simp only [Nat.succ_eq_add_one, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.sum_singleton, Fin.sum_univ_succ, toTimeAndSpace_symm_apply_inl,
    toTimeAndSpace_symm_apply_inr]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ↑(boost 0 (-β) ⋯) μ (Sum.inl 0) * (c.val * t.val) +
    (↑(boost 0 (-β) ⋯) μ (Sum.inr 0) * x.val 0 + ∑ i, ↑(boost 0 (-β) ⋯) μ (Sum.inr i.succ) * x.val i.succ) =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })
    μ
  match μ with
  | Sum.inl 0 =>d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inl 0) (Sum.inl 0) * (c.val * t.val) +
    (↑(boost 0 (-β) ⋯) (Sum.inl 0) (Sum.inr 0) * x.val 0 +
      ∑ i, ↑(boost 0 (-β) ⋯) (Sum.inl 0) (Sum.inr i.succ) * x.val i.succ) =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })
    (Sum.inl 0)
    simp [γ_neg]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succ⊢ γ β * (c.val * t.val) + γ β * β * x.val 0 = c.val * (γ β * (t.val + β / c.val * x.val 0))
    field_simpAll goals completed! 🐙
  | Sum.inr ⟨0, h⟩ =>d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succh:0 < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨0, h⟩) (Sum.inl 0) * (c.val * t.val) +
    (↑(boost 0 (-β) ⋯) (Sum.inr ⟨0, h⟩) (Sum.inr 0) * x.val 0 +
      ∑ i, ↑(boost 0 (-β) ⋯) (Sum.inr ⟨0, h⟩) (Sum.inr i.succ) * x.val i.succ) =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })
    (Sum.inr ⟨0, h⟩)
    simp only [toTimeAndSpace_symm_apply_inr]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succh:0 < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨0, h⟩) (Sum.inl 0) * (c.val * t.val) +
    (↑(boost 0 (-β) ⋯) (Sum.inr ⟨0, h⟩) (Sum.inr 0) * x.val 0 +
      ∑ i, ↑(boost 0 (-β) ⋯) (Sum.inr ⟨0, h⟩) (Sum.inr i.succ) * x.val i.succ) =
  γ β * (x.val 0 + c.val * β * t.val)
    simp [γ_neg]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succh:0 < d.succ⊢ γ β * β * (c.val * t.val) + γ β * x.val 0 = γ β * (x.val 0 + c.val * β * t.val)
    ringAll goals completed! 🐙
  | Sum.inr ⟨Nat.succ n, h⟩ =>d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n.succ, h⟩) (Sum.inl 0) * (c.val * t.val) +
    (↑(boost 0 (-β) ⋯) (Sum.inr ⟨n.succ, h⟩) (Sum.inr 0) * x.val 0 +
      ∑ i, ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n.succ, h⟩) (Sum.inr i.succ) * x.val i.succ) =
  (toTimeAndSpace c).symm
    ({ val := γ β * (t.val + β / c.val * x.val 0) },
      {
        val := fun x_1 =>
          match x_1 with
          | ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
          | ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })
    (Sum.inr ⟨n.succ, h⟩)
    simp only [Nat.succ_eq_add_one, Fin.isValue, boost_zero_inr_nat_succ_inl_0, zero_mul,
      boost_zero_inr_nat_succ_inr_0, zero_add, toTimeAndSpace_symm_apply_inr]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ∑ x_1, ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr x_1.succ) * x.val x_1.succ = x.val ⟨n + 1, h⟩
    rw [Finset.sum_eq_single ⟨n, byd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ n < dd:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = x.val ⟨n + 1, h⟩h₀d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ∀ b ∈ Finset.univ, b ≠ ⟨n, ⋯⟩ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr b.succ) * x.val b.succ = 0h₁d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ⟨n, ⋯⟩ ∉ Finset.univ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = 0 omegaAll goals completed! 🐙d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = x.val ⟨n + 1, h⟩h₀d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ∀ b ∈ Finset.univ, b ≠ ⟨n, ⋯⟩ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr b.succ) * x.val b.succ = 0h₁d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ⟨n, ⋯⟩ ∉ Finset.univ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = 0⟩]d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = x.val ⟨n + 1, h⟩h₀d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ∀ b ∈ Finset.univ, b ≠ ⟨n, ⋯⟩ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr b.succ) * x.val b.succ = 0h₁d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ⟨n, ⋯⟩ ∉ Finset.univ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = 0 <;>d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = x.val ⟨n + 1, h⟩h₀d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ∀ b ∈ Finset.univ, b ≠ ⟨n, ⋯⟩ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr b.succ) * x.val b.succ = 0h₁d:ℕβ:ℝhβ:|β| < 1c:SpeedOfLightt:Timex:Space d.succμ:Fin 1 ⊕ Fin d.succn:ℕh:n.succ < d.succ⊢ ⟨n, ⋯⟩ ∉ Finset.univ → ↑(boost 0 (-β) ⋯) (Sum.inr ⟨n + 1, h⟩) (Sum.inr ⟨n, ⋯⟩.succ) * x.val ⟨n, ⋯⟩.succ = 0
      simp +contextual [boost_inr_inr_other, Fin.ext_iff]All goals completed! 🐙