awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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))
                ⋯ :
              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)
                  ⋯ :
                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₁) :
            (a : A₁) → A₁)
          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))
      ⋯ =
    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₁)

Tactic:
ext
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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))
              ⋯ :
            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)
                ⋯ :
              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₁) :
          (a : A₁) → A₁)
        a :
      A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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))
                ⋯ :
              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)
                  ⋯ :
                Derivation R A₁ A₁) :
            (a : A₁) → A₁)
          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))
      ⋯ =
    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₁)

Tactic:
ext
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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))
              ⋯ :
            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)
                ⋯ :
              Derivation R A₁ A₁) :
          (a : A₁) → A₁)
        a :
      A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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⁆)
                ⋯ :
              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)
                    ⋯ :
                  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₁) :
            (a : A₁) → A₁)
          a :
        A₁)
⊢ 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₁)

Tactic:
ext
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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⁆)
              ⋯ :
            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)
                  ⋯ :
                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₁) :
          (a : A₁) → A₁)
        a :
      A₁)

Tactic:
simp [Derivation.commutator_apply]

Premises used: Derivation.commutator_apply
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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)
                        ⋯,
                    map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
                  (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)
                          ⋯,
                      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₁) :
            (a : A₁) → A₁)
          a :
        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' := ⋯ } :
        (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₁)

Tactic:
ext
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
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)
                      ⋯,
                  map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } :
                (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)
                        ⋯,
                    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₁) :
          (a : A₁) → A₁)
        a :
      A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
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₁
⊢ Eq (α := A₁) ((AlgHom.id R A₁ : (a : A₁) → A₁) ⁅x_1, x⁆ : A₁)
    (Bracket.bracket (L := Derivation R A₁ 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' := ⋯ } :
              (a : L₁) → Derivation R A₁ A₁)
            x_1 :
          Derivation R A₁ A₁)
        ((AlgHom.id R A₁ : (a : A₁) → A₁) x) :
      A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : Algebra R A₁
⊢ Eq (α := Derivation R A₁ A₁ →ₗ⁅AlgHom.id R A₁⁆ Derivation R A₁ A₁) (anchor R A₁ (Derivation R A₁ A₁)) Hom.id

Tactic:
rfl

Premises used: LieRinehartAlgebra.anchor, Derivation.mk', LieRinehartAlgebra.Hom.id, LieHom.id, rfl
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : Algebra R A₁
inst_6 : LieAlgebra R L₁
inst_7 : LieRinehartRing A₁ L₁
inst_8 : LieRinehartAlgebra R A₁ L₁
l : L₁
a : A₁
⊢ ((((Hom.toLieHom (anchor R A₁ L₁) : LieHom.{u_1, u_3, u_2} R L₁ (Derivation R A₁ A₁)) : (a : L₁) → Derivation R A₁ A₁)
            l :
          Derivation R A₁ A₁) :
        (a : A₁) → A₁)
      a =
    ⁅l, a⁆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
x : ℕ
n : ℕ := x
h : ¬n < E.order
k : Fin E.order
⊢ n - E.order + (↑k : ℕ) < n

Tactic:
lia
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : ℕ
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 := ⋯;
        E.coeffs k * E.mkSol init (n + E.order - E.order + (↑k : ℕ)))
    (∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + (↑i : ℕ)))
⊢ E.mkSol init (n + E.order) = ∑ i : Fin E.order, E.coeffs i * E.mkSol init (n + (↑i : ℕ))

Tactic:
rw [mkSol]

Premises used: LinearRecurrence.mkSol
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : ℕ
⊢ 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 := ⋯;
        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:
simp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : Fin E.order
rw :
  (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 : ℕ))) =
    init n
⊢ E.mkSol init (↑n : ℕ) = init n

Tactic:
rw [mkSol]

Premises used: LinearRecurrence.mkSol
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
n : Fin E.order
⊢ (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 : ℕ))) =
    init n

Tactic:
simp only [n.is_lt, dif_pos, Fin.mk_val]

Premises used: Fin.mk_val, dif_pos, Fin.is_lt
-- Module: Mathlib.Algebra.LinearRecurrence
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 : ℕ
rw :
  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 : ℕ))
⊢ u n = E.mkSol init n

Tactic:
rw [mkSol]

Premises used: LinearRecurrence.mkSol
-- Module: Mathlib.Algebra.LinearRecurrence
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'⟩
neg :
  ∀ (h' : ¬n < E.order),
    u n =
      ∑ k : Fin E.order,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))
⊢ 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 : ℕ))

Tactic:
split_ifs with h'
-- Module: Mathlib.Algebra.LinearRecurrence
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 = init ⟨n, h'⟩

Tactic:
mod_cast heq ⟨n, h'⟩

Premises used: cast, Fin.mk, Eq.refl, Eq
-- Module: Mathlib.Algebra.LinearRecurrence
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 = init ⟨n, h'⟩

Tactic:
exact mod_cast heq ⟨n, h'⟩

Premises used: Fin.mk
-- Module: Mathlib.Algebra.LinearRecurrence
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
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 : ℕ)))
⊢ u n = ∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ))

Tactic:
rw [← tsub_add_cancel_of_le (le_of_not_gt h'), h (n - E.order)]

Premises used: HSub.hSub, le_of_not_gt, tsub_add_cancel_of_le, LinearRecurrence.order