awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
⊢ Eq (α := Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
        Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
        Dual.{u_1, u_2} K ↥H) ∨
    Eq (α := Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
        Dual.{u_1, u_2} K ↥H)
      (-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
            (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
              Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
        Dual.{u_1, u_2} K ↥H)
have inr : Eq (α := Dual.{u_1, u_2} K ↥H)
  ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
      (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
        Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
    Dual.{u_1, u_2} K ↥H)
  ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
      (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
        Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
    Dual.{u_1, u_2} K ↥H)
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
⊢ Eq (α := Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
      Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
      Dual.{u_1, u_2} K ↥H)
have inr : ∀ (x : ↥H),
  Eq.{u_1 + 1} (α := K)
    ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                hα) :
            Dual.{u_1, u_2} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β
                hβ) :
            Dual.{u_1, u_2} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x : Derivation R A₁ A₁
x_1 x_2 : A₁
⊢ ⁅x, x_1 * x_2⁆ = x_1 • ⁅x, x_2⁆ + ⁅x, x_1⁆ * x_2
have simp : HMul.hMul (β := A₁) x_2 ((x : (a : A₁) → A₁) x_1 : A₁) = HMul.hMul (α := A₁) ((x : (a : A₁) → A₁) x_1 : A₁) x_2
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x x_1 : Derivation R A₁ A₁
x_2 : A₁
⊢ ⁅x, x_2 • x_1⁆ = x_2 • ⁅x, x_1⁆ + ⁅x, x_2⁆ • x_1
have H : ∀ (a : A₁),
  Eq (α := A₁) ((⁅x, x_2 • x_1⁆ : (a : A₁) → A₁) a : A₁) ((x_2 • ⁅x, x_1⁆ + ⁅x, x_2⁆ • x_1 : (a : A₁) → A₁) a : A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x x_1 : Derivation R A₁ A₁
x_2 a : A₁
⊢ Eq (α := A₁) ((⁅x, x_2 • x_1⁆ : (a : A₁) → A₁) a : A₁) ((x_2 • ⁅x, x_1⁆ + ⁅x, x_2⁆ • x_1 : (a : A₁) → A₁) a : A₁)
have H : HMul.hMul (β := A₁) x_2 ((x : (a : A₁) → A₁) ((x_1 : (a : A₁) → A₁) a : A₁) : A₁) +
      HMul.hMul (α := A₁) (β := A₁) ((x_1 : (a : A₁) → A₁) a : A₁) ((x : (a : A₁) → A₁) x_2 : A₁) -
    HMul.hMul (β := A₁) x_2 ((x_1 : (a : A₁) → A₁) ((x : (a : A₁) → A₁) a : A₁) : A₁) =
  x_2 *
      HSub.hSub (α := A₁) (β := A₁) ((x : (a : A₁) → A₁) ((x_1 : (a : A₁) → A₁) a : A₁) : A₁)
        ((x_1 : (a : A₁) → A₁) ((x : (a : A₁) → A₁) a : A₁) : A₁) +
    HMul.hMul (α := A₁) (β := A₁) ((x : (a : A₁) → A₁) x_2 : A₁) ((x_1 : (a : A₁) → A₁) a : A₁)
Tactic: simp [Derivation.commutator_apply]
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst_19 : LieRinehartRing A₁ L₁
inst_20 : LieRinehartAlgebra R A₁ L₁
x x_1 : L₁
⊢ Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
      (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
        (x + x_1))
      ⋯ =
    HAdd.hAdd (α := Derivation R A₁ A₁) (β := Derivation R A₁ A₁)
      (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
          (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x)
          ⋯ :
        Derivation R A₁ A₁)
      (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
          (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x_1)
          ⋯ :
        Derivation R A₁ A₁)
have H : ∀ (a : A₁),
  Eq (α := A₁)
    (((Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
              (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
                (x + x_1))
              sorry :
            Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
    ((HAdd.hAdd (α := Derivation R A₁ A₁) (β := Derivation R A₁ A₁)
            (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                    (a : L₁) → Module.End R A₁)
                  x)
                sorry :
              Derivation R A₁ A₁)
            (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                    (a : L₁) → Module.End R A₁)
                  x_1)
                sorry :
              Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst_19 : LieRinehartRing A₁ L₁
inst_20 : LieRinehartAlgebra R A₁ L₁
x : R
x_1 : L₁
⊢ Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
      (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
        (x • x_1))
      ⋯ =
    HSMul.hSMul (α := R) (β := Derivation R A₁ A₁) ((RingHom.id R : (a : R) → R) x : R)
      (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
          (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x_1)
          ⋯ :
        Derivation R A₁ A₁)
have H : ∀ (a : A₁),
  Eq (α := A₁)
    (((Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
              (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
                (x • x_1))
              sorry :
            Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
    ((HSMul.hSMul (α := R) (β := Derivation R A₁ A₁) ((RingHom.id R : (a : R) → R) x : R)
            (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                    (a : L₁) → Module.End R A₁)
                  x_1)
                sorry :
              Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst_19 : LieRinehartRing A₁ L₁
inst_20 : LieRinehartAlgebra R A₁ L₁
x x_1 : L₁
⊢ Eq.{u_2 + 1} (α := Derivation R A₁ A₁)
    (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
        (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
          ⁅x, x_1⁆)
        ⋯ :
      Derivation R A₁ A₁)
    (Bracket.bracket (L := Derivation R A₁ A₁)
        (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
            (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x)
            ⋯ :
          Derivation R A₁ A₁)
        (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
          (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x_1)
          ⋯) :
      Derivation R A₁ A₁)
have H : ∀ (a : A₁),
  Eq (α := A₁)
    (((Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
              (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
                ⁅x, x_1⁆)
              sorry :
            Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
    (((Bracket.bracket (L := Derivation R A₁ A₁)
              (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                  (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                      (a : L₁) → Module.End R A₁)
                    x)
                  sorry :
                Derivation R A₁ A₁)
              (Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                    (a : L₁) → Module.End R A₁)
                  x_1)
                sorry) :
            Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LieRinehartAlgebra.Defs (goal)
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst_19 : LieRinehartRing A₁ L₁
inst_20 : LieRinehartAlgebra R A₁ L₁
x : A₁
x_1 : L₁
⊢ ({
          toFun := fun (x : L₁) ↦
            Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
              (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁)
                x)
              ⋯,
          map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
        (a : L₁) → Derivation R A₁ A₁)
      (x • x_1) =
    HSMul.hSMul (α := A₁) (β := Derivation R A₁ A₁) ((AlgHom.id R A₁ : (a : A₁) → A₁) x : A₁)
      (({
              toFun := fun (x : L₁) ↦
                Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                  (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                      (a : L₁) → Module.End R A₁)
                    x)
                  ⋯,
              map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ : LieHom.{u_1, u_3, u_2} R L₁ (Derivation R A₁ A₁) } :
            (a : L₁) → Derivation R A₁ A₁)
          x_1 :
        Derivation R A₁ A₁)
have H : ∀ (a : A₁),
  Eq (α := A₁)
    (((({
                  toFun := fun (x : L₁) ↦
                    Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                      (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                          (a : L₁) → Module.End R A₁)
                        x)
                      sorry,
                  map_add' := sorry, map_smul' := sorry, map_lie' := sorry } :
                (a : L₁) → Derivation R A₁ A₁)
              (x • x_1) :
            Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
    ((HSMul.hSMul (α := A₁) (β := Derivation R A₁ A₁) ((AlgHom.id R A₁ : (a : A₁) → A₁) x : A₁)
            (({
                    toFun := fun (x : L₁) ↦
                      Derivation.mk'.{u_1, u_2, u_2} (R := R) (M := A₁)
                        (((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) :
                            (a : L₁) → Module.End R A₁)
                          x)
                        sorry,
                    map_add' := sorry, map_smul' := sorry, map_lie' := sorry : LieHom.{u_1, u_3, u_2} R L₁ (Derivation R A₁ A₁) } :
                  (a : L₁) → Derivation R A₁ A₁)
                x_1 :
              Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : ℕ
⊢ E.mkSol init (n + E.order) = ∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + (↑i : ℕ))
have rw : Eq.{u_1 + 1} (α := R)
  (if h : n + E.order < E.order then init ⟨n + E.order, h⟩
  else
    ∑ k : Fin E.order,
      have x := sorry;
      E.coeffs k * E.mkSol init (n + E.order - E.order + (↑k : ℕ)))
  (∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + (↑i : ℕ)))
Tactic: rw [mkSol]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : Fin E.order
⊢ E.mkSol init (↑n : ℕ) = init n
have rw : (if h : (↑n : ℕ) < E.order then init ⟨(↑n : ℕ), h⟩
  else
    ∑ k : Fin E.order,
      have x := sorry;
      E.coeffs k * E.mkSol init ((↑n : ℕ) - E.order + (↑k : ℕ))) =
  init n
Tactic: rw [mkSol]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
⊢ u n = E.mkSol init n
have rw : u n =
  if h : n < E.order then init ⟨n, h⟩
  else
    ∑ k : Fin E.order,
      have x := sorry;
      E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))
Tactic: rw [mkSol]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k : Fin E.order,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))
have pos : ∀ (h' : n < E.order), u n = init ⟨n, h'⟩
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
pos : ∀ (h' : n < E.order), u n = init ⟨n, h'⟩
⊢ u n =
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k : Fin E.order,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))
have neg : ∀ (h' : ¬n < E.order),
  u n =
    ∑ k : Fin E.order,
      have x := sorry;
      E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
h' : ¬n < E.order
⊢ u n = ∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))
have neg : Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, E.coeffs i * u (n - E.order + (↑i : ℕ)))
  (∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ)))
Tactic: rw [← tsub_add_cancel_of_le (le_of_not_gt h'), h (n - E.order)]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
h' : ¬n < E.order
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, E.coeffs i * u (n - E.order + (↑i : ℕ)))
    (∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ)))
have neg : ∀ (k : Fin E.order),
  E.coeffs k * u (n - E.order + (↑k : ℕ)) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ))
Tactic: congr with k
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.coeffs k * u (n - E.order + (↑k : ℕ)) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ))
have neg : E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ)) =
  E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ))
Tactic: rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
a : R
u : ℕ → R
hu : Membership.mem (γ := Set (ℕ → R)) {u : ℕ → R | E.IsSolution u} u
n : ℕ
⊢ (a • u) (n + E.order) = ∑ i : Fin E.order, E.coeffs i * (a • u) (n + (↑i : ℕ))
have simp : Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, a * (E.coeffs i * u (n + (↑i : ℕ))))
  (∑ x : Fin E.order, E.coeffs x * (a * u (n + (↑x : ℕ))))
Tactic: simp [hu n, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
⊢ (fun (x : Fin E.order) ↦ (↑(u + v) : ℕ → R) (↑x : ℕ)) =
    HAdd.hAdd (α := Fin E.order → R) (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) fun (x : Fin E.order) ↦
      (↑v : ℕ → R) (↑x : ℕ)
have h : ∀ (x : Fin E.order),
  (↑(u + v) : ℕ → R) (↑x : ℕ) =
    HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R) (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ))
      (fun (x : Fin E.order) ↦ (↑v : ℕ → R) (↑x : ℕ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
⊢ (fun (x : Fin E.order) ↦ (↑(a • u) : ℕ → R) (↑x : ℕ)) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) a : R) fun (x : Fin E.order) ↦
      (↑u : ℕ → R) (↑x : ℕ)
have h : ∀ (x : Fin E.order),
  (↑(a • u) : ℕ → R) (↑x : ℕ) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) a : R)
      (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
⊢ (fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) ⋯)
      ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u) =
    u
have a : ∀ (n : ℕ),
  (↑((fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) sorry)
            ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u)) :
        ℕ → R)
      n =
    (↑u : ℕ → R) n
Tactic: ext n