mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case mpr
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
⊢ A *ᵥ x = 0 → Aᵀ *ᵥ A *ᵥ x = 0

Tactic:
·

Goal state after:
case mpr
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
⊢ A *ᵥ x = 0 → Aᵀ *ᵥ A *ᵥ x = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker =
    finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker

pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker =
    finrank R ↥A.mulVecLin.range + finrank R ↥A.mulVecLin.ker

Tactic:
·

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥A.mulVecLin.ker =
    finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker =
    finrank R ↥A.mulVecLin.range + finrank R ↥A.mulVecLin.ker

Tactic:
·

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker =
    finrank R ↥A.mulVecLin.range + finrank R ↥A.mulVecLin.ker
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ x ∈ couple R A A' → ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2

pp: case mpr
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2 → x ∈ couple R A A'

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ x ∈ couple R A A' → ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ a ∈ twoCocycle R L M → ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

pp: case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ (∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆) → a ∈ twoCocycle R L M

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ a ∈ twoCocycle R L M → ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2 → x ∈ couple R A A'

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2 → x ∈ couple R A A'
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝ : A
l : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝ ⊗ₜ[R] l, y⁆ =
    ⁅x✝ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l)⁆

pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y x✝¹ x✝ : A ⊗[R] L
h1 : (LinearMap.rTensor L ↑d) ⁅x✝¹, y⁆ = ⁅x✝¹, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝¹⁆
h2 : (LinearMap.rTensor L ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ + x✝, y⁆ =
    ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝ : A
l : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝ ⊗ₜ[R] l, y⁆ =
    ⁅x✝ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l)⁆
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝¹ : A
l : L
x✝ : A
l' : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ ⊗ₜ[R] l, x✝ ⊗ₜ[R] l'⁆ =
    ⁅x✝¹ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l')⁆ - ⁅x✝ ⊗ₜ[R] l', (LinearMap.rTensor L ↑d) (x✝¹ ⊗ₜ[R] l)⁆

pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝² : A
l : L
x✝¹ x✝ : A ⊗[R] L
h1 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝¹⁆ - ⁅x✝¹, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
h2 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝⁆ - ⁅x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹ + x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆ - ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆

Tactic:
·

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝¹ : A
l : L
x✝ : A
l' : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ ⊗ₜ[R] l, x✝ ⊗ₜ[R] l'⁆ =
    ⁅x✝¹ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l')⁆ - ⁅x✝ ⊗ₜ[R] l', (LinearMap.rTensor L ↑d) (x✝¹ ⊗ₜ[R] l)⁆
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝² : A
l : L
x✝¹ x✝ : A ⊗[R] L
h1 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝¹⁆ - ⁅x✝¹, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
h2 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝⁆ - ⁅x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹ + x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆ - ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆

Tactic:
·

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝² : A
l : L
x✝¹ x✝ : A ⊗[R] L
h1 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝¹⁆ - ⁅x✝¹, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
h2 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝⁆ - ⁅x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹ + x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆ - ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ (∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆) → a ∈ twoCocycle R L M

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ (∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆) → a ∈ twoCocycle R L M
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y x✝¹ x✝ : A ⊗[R] L
h1 : (LinearMap.rTensor L ↑d) ⁅x✝¹, y⁆ = ⁅x✝¹, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝¹⁆
h2 : (LinearMap.rTensor L ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ + x✝, y⁆ =
    ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y x✝¹ x✝ : A ⊗[R] L
h1 : (LinearMap.rTensor L ↑d) ⁅x✝¹, y⁆ = ⁅x✝¹, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝¹⁆
h2 : (LinearMap.rTensor L ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ + x✝, y⁆ =
    ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L),
    (LinearMap.lTensor A ↑d) ⁅x ⊗ₜ[R] y_1, y⁆ =
      ⁅x ⊗ₜ[R] y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x ⊗ₜ[R] y_1)⁆

pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x, y⁆ = ⁅x, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x⁆ →
      (LinearMap.lTensor A ↑d) ⁅y_1, y⁆ = ⁅y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y_1⁆ →
        (LinearMap.lTensor A ↑d) ⁅x + y_1, y⁆ =
          ⁅x + y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x + y_1)⁆

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L),
    (LinearMap.lTensor A ↑d) ⁅x ⊗ₜ[R] y_1, y⁆ =
      ⁅x ⊗ₜ[R] y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x ⊗ₜ[R] y_1)⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case pos
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) i = ⁅x, (lof R ι M j).toFun m⁆ i

pp: case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) i = ⁅x, (lof R ι M j).toFun m⁆ i

Tactic:
·

Goal state after:
case pos
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) i = ⁅x, (lof R ι M j).toFun m⁆ i
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x : A) (y : L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x ⊗ₜ[R] y⁆ =
      ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x ⊗ₜ[R] y)⁆ - ⁅x ⊗ₜ[R] y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x⁆ =
        ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) x⁆ - ⁅x, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
      (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
        (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x + y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x + y)⁆ - ⁅x + y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

Tactic:
·

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x : A) (y : L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x ⊗ₜ[R] y⁆ =
      ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x ⊗ₜ[R] y)⁆ - ⁅x ⊗ₜ[R] y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) i = ⁅x, (lof R ι M j).toFun m⁆ i

Tactic:
·

Goal state after:
case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) i = ⁅x, (lof R ι M j).toFun m⁆ i
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x⁆ =
        ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) x⁆ - ⁅x, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
      (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
        (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x + y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x + y)⁆ - ⁅x + y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

Tactic:
·

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x⁆ =
        ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) x⁆ - ⁅x, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
      (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
        (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x + y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x + y)⁆ - ⁅x + y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x, y⁆ = ⁅x, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x⁆ →
      (LinearMap.lTensor A ↑d) ⁅y_1, y⁆ = ⁅y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y_1⁆ →
        (LinearMap.lTensor A ↑d) ⁅x + y_1, y⁆ =
          ⁅x + y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x + y_1)⁆

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x, y⁆ = ⁅x, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x⁆ →
      (LinearMap.lTensor A ↑d) ⁅y_1, y⁆ = ⁅y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y_1⁆ →
        (LinearMap.lTensor A ↑d) ⁅x + y_1, y⁆ =
          ⁅x + y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x + y_1)⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Tactic:
obtain rfl | hik := Decidable.eq_or_ne k i

Goal state after:
case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
j : ι
y : L j
k : ι
hij : k ≠ j
x : L k
⊢ ⁅((of L k) x) k, ((of L j) y) k⁆ = 0 k

case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
j : ι
y : L j
k : ι
hij : k ≠ j
x : L k
⊢ ⁅((of L k) x) k, ((of L j) y) k⁆ = 0 k

pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Tactic:
·

Goal state after:
case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
j : ι
y : L j
k : ι
hij : k ≠ j
x : L k
⊢ ⁅((of L k) x) k, ((of L j) y) k⁆ = 0 k
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Tactic:
·

Goal state after:
case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : k ≠ i
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i : ι
x y : L i
⊢ ⁅(of L i) x, (of L i) y⁆ = if hij : i = i then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Tactic:
·

Goal state after:
case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i : ι
x y : L i
⊢ ⁅(of L i) x, (of L i) y⁆ = if hij : i = i then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Tactic:
·

Goal state after:
case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0