mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x : L
x✝¹ : R
x✝ : L
⊢ ⁅x, f (x✝¹ • x✝)⁆ - ⁅x✝¹ • x✝, f x⁆ - f ⁅x, x✝¹ • x✝⁆ = (RingHom.id R) x✝¹ • (⁅x, f x✝⁆ - ⁅x✝, f x⁆ - f ⁅x, x✝⁆)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x✝¹ x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝¹ + x✝, f y⁆ - ⁅y, f (x✝¹ + x✝)⁆ - f ⁅x✝¹ + x✝, y⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun y ↦ ⁅x✝¹, f y⁆ - ⁅y, f x✝¹⁆ - f ⁅x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun y ↦ ⁅x✝, f y⁆ - ⁅y, f x✝⁆ - f ⁅x✝, y⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x✝¹ : R
x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝¹ • x✝, f y⁆ - ⁅y, f (x✝¹ • x✝)⁆ - f ⁅x✝¹ • x✝, y⁆, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ • { toFun := fun y ↦ ⁅x✝, f y⁆ - ⁅y, f x✝⁆ - f ⁅x✝, y⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x : L
⊢ ({ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
          map_smul' := ⋯ }
        x)
      x =
    0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
x✝¹ x✝ : oneCochain R L M
⊢ ⟨{
        toFun := fun x ↦
          { toFun := fun y ↦ ⁅x, (x✝¹ + x✝) y⁆ - ⁅y, (x✝¹ + x✝) x⁆ - (x✝¹ + x✝) ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ },
      ⋯⟩ =
    ⟨{ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, x✝¹ y⁆ - ⁅y, x✝¹ x⁆ - x✝¹ ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
        ⋯⟩ +
      ⟨{ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, x✝ y⁆ - ⁅y, x✝ x⁆ - x✝ ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
        ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
x✝¹ : R
x✝ : oneCochain R L M
⊢ ⟨{
        toFun := fun x ↦
          { toFun := fun y ↦ ⁅x, (x✝¹ • x✝) y⁆ - ⁅y, (x✝¹ • x✝) x⁆ - (x✝¹ • x✝) ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ },
      ⋯⟩ =
    (RingHom.id R) x✝¹ •
      ⟨{ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, x✝ y⁆ - ⁅y, x✝ x⁆ - x✝ ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
        ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
⊢ ∀ (i : m), (if w i = 0 then 1 else w i) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
⊢ LinearIndependent R w'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x y : L
⊢ (((d₁₂ R L M) f) x) y = -f ⁅x, y⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x y : L
⊢ (((d₁₂ R L M) f) x) y = -f ⁅x, y⁆

Tactic:
by
  simp [trivial_lie_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
this : ∀ (a : m), diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
⊢ insert 0 (range (diagonal w).col) = insert 0 (range w')

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
⊢ insert 0 (range (diagonal w).col) = insert 0 (range w')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x y x✝¹ x✝ : L
⊢ ⁅x, (a y) (x✝¹ + x✝)⁆ - ⁅y, (a x) (x✝¹ + x✝)⁆ + ⁅x✝¹ + x✝, (a x) y⁆ - (a ⁅x, y⁆) (x✝¹ + x✝) + (a ⁅x, x✝¹ + x✝⁆) y -
      (a ⁅y, x✝¹ + x✝⁆) x =
    ⁅x, (a y) x✝¹⁆ - ⁅y, (a x) x✝¹⁆ + ⁅x✝¹, (a x) y⁆ - (a ⁅x, y⁆) x✝¹ + (a ⁅x, x✝¹⁆) y - (a ⁅y, x✝¹⁆) x +
      (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
⊢ (diagonal w).cRank = lift.{uR, um} #{ i // w i ≠ 0 }

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
⊢ (diagonal w).eRank = {i | w i ≠ 0}.encard

Tactic:
by

Goal state after:
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✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (Aᴴ * A).mulVecLin.ker = A.mulVecLin.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x y : L
x✝¹ : R
x✝ : L
⊢ ⁅x, (a y) (x✝¹ • x✝)⁆ - ⁅y, (a x) (x✝¹ • x✝)⁆ + ⁅x✝¹ • x✝, (a x) y⁆ - (a ⁅x, y⁆) (x✝¹ • x✝) + (a ⁅x, x✝¹ • x✝⁆) y -
      (a ⁅y, x✝¹ • x✝⁆) x =
    (RingHom.id R) x✝¹ • (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
this : engel K ↑v ≤ engel K x
⊢ ∀ (m : ↥E), ∃ n, ((toEnd K ↥U ↥E) (α • u + x') ^ n) m = 0

Tactic:
by

Goal state after:
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✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (Aᴴ * A).rank = A.rank

Tactic:
by

Goal state after:
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✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).rank = A.rank

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x x✝¹ x✝ : L
⊢ {
      toFun := fun z ↦
        ⁅x, (a (x✝¹ + x✝)) z⁆ - ⁅x✝¹ + x✝, (a x) z⁆ + ⁅z, (a x) (x✝¹ + x✝)⁆ - (a ⁅x, x✝¹ + x✝⁆) z +
            (a ⁅x, z⁆) (x✝¹ + x✝) -
          (a ⁅x✝¹ + x✝, z⁆) x,
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun z ↦
          ⁅x, (a x✝¹) z⁆ - ⁅x✝¹, (a x) z⁆ + ⁅z, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) z + (a ⁅x, z⁆) x✝¹ - (a ⁅x✝¹, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun z ↦ ⁅x, (a x✝) z⁆ - ⁅x✝, (a x) z⁆ + ⁅z, (a x) x✝⁆ - (a ⁅x, x✝⁆) z + (a ⁅x, z⁆) x✝ - (a ⁅x✝, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
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
⊢ (Aᵀ * A).mulVecLin.ker = A.mulVecLin.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x : L
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun z ↦
        ⁅x, (a (x✝¹ • x✝)) z⁆ - ⁅x✝¹ • x✝, (a x) z⁆ + ⁅z, (a x) (x✝¹ • x✝)⁆ - (a ⁅x, x✝¹ • x✝⁆) z +
            (a ⁅x, z⁆) (x✝¹ • x✝) -
          (a ⁅x✝¹ • x✝, z⁆) x,
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      { toFun := fun z ↦ ⁅x, (a x✝) z⁆ - ⁅x✝, (a x) z⁆ + ⁅z, (a x) x✝⁆ - (a ⁅x, x✝⁆) z + (a ⁅x, z⁆) x✝ - (a ⁅x✝, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
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
⊢ (Aᵀ * A).rank = A.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ finrank R ↥((toLin (Pi.basisFun R n) (Pi.basisFun R m)) A).dualMap.range = A.rank

Tactic:
LinearMap.finrank_range_dualMap_eq_finrank_range,

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ finrank R ↥((toLin (Pi.basisFun R n) (Pi.basisFun R m)) A).range = A.rank
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ Aᵀ.rank = A.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
⊢ A.rank = finrank R ↥(span R (range A.row))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
⊢ M.rank = Fintype.card m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x✝¹ x✝ : L
⊢ {
      toFun := fun y ↦
        {
          toFun := fun z ↦
            ⁅x✝¹ + x✝, (a y) z⁆ - ⁅y, (a (x✝¹ + x✝)) z⁆ + ⁅z, (a (x✝¹ + x✝)) y⁆ - (a ⁅x✝¹ + x✝, y⁆) z +
                (a ⁅x✝¹ + x✝, z⁆) y -
              (a ⁅y, z⁆) (x✝¹ + x✝),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝¹, (a y) z⁆ - ⁅y, (a x✝¹) z⁆ + ⁅z, (a x✝¹) y⁆ - (a ⁅x✝¹, y⁆) z + (a ⁅x✝¹, z⁆) y - (a ⁅y, z⁆) x✝¹,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ } +
      {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝, (a y) z⁆ - ⁅y, (a x✝) z⁆ + ⁅z, (a x✝) y⁆ - (a ⁅x✝, y⁆) z + (a ⁅x✝, z⁆) y - (a ⁅y, z⁆) x✝,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun y ↦
        {
          toFun := fun z ↦
            ⁅x✝¹ • x✝, (a y) z⁆ - ⁅y, (a (x✝¹ • x✝)) z⁆ + ⁅z, (a (x✝¹ • x✝)) y⁆ - (a ⁅x✝¹ • x✝, y⁆) z +
                (a ⁅x✝¹ • x✝, z⁆) y -
              (a ⁅y, z⁆) (x✝¹ • x✝),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝, (a y) z⁆ - ⁅y, (a x✝) z⁆ + ⁅z, (a x✝) y⁆ - (a ⁅x✝, y⁆) z + (a ⁅x✝, z⁆) y - (a ⁅y, z⁆) x✝,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
x✝¹ x✝ : ↥(twoCochain R L M)
⊢ {
      toFun := fun x ↦
        {
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x, ((x✝¹ + x✝) y) z⁆ - ⁅y, ((x✝¹ + x✝) x) z⁆ + ⁅z, ((x✝¹ + x✝) x) y⁆ - ((x✝¹ + x✝) ⁅x, y⁆) z +
                    ((x✝¹ + x✝) ⁅x, z⁆) y -
                  ((x✝¹ + x✝) ⁅y, z⁆) x,
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun x ↦
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x, (x✝¹ y) z⁆ - ⁅y, (x✝¹ x) z⁆ + ⁅z, (x✝¹ x) y⁆ - (x✝¹ ⁅x, y⁆) z + (x✝¹ ⁅x, z⁆) y - (x✝¹ ⁅y, z⁆) x,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ } +
      {
        toFun := fun x ↦
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x, (x✝ y) z⁆ - ⁅y, (x✝ x) z⁆ + ⁅z, (x✝ x) y⁆ - (x✝ ⁅x, y⁆) z + (x✝ ⁅x, z⁆) y - (x✝ ⁅y, z⁆) x,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ (toLin' (vecMulVec w v)).rank ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
x✝¹ : R
x✝ : ↥(twoCochain R L M)
⊢ {
      toFun := fun x ↦
        {
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x, ((x✝¹ • x✝) y) z⁆ - ⁅y, ((x✝¹ • x✝) x) z⁆ + ⁅z, ((x✝¹ • x✝) x) y⁆ - ((x✝¹ • x✝) ⁅x, y⁆) z +
                    ((x✝¹ • x✝) ⁅x, z⁆) y -
                  ((x✝¹ • x✝) ⁅y, z⁆) x,
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun x ↦
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x, (x✝ y) z⁆ - ⁅y, (x✝ x) z⁆ + ⁅z, (x✝ x) y⁆ - (x✝ ⁅x, y⁆) z + (x✝ ⁅x, z⁆) y - (x✝ ⁅y, z⁆) x,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1✝ D2✝ : Derivation R A A
a✝ : A
D1 D2 : Derivation R A A
a b : A
⊢ ⁅↑D1, ↑D2⁆ (a * b) = a • ⁅↑D1, ↑D2⁆ b + b • ⁅↑D1, ↑D2⁆ a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d : Derivation R A A
⊢ ⁅d, d⁆ = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
r : R
d e : Derivation R A A
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = ⁅x✝², x✝¹⁆ x✝ + x✝¹ (x✝² x✝)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ ∀ {a b : Derivation R A' A' × Derivation R A A},
    a ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
      b ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
        a + b ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ 0 ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ ∀ (c : R) {x : Derivation R A' A' × Derivation R A A},
    x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2} →
      c • x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ a ⁅y, ⁅z, x⁆⁆ = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
⊢ d₂₃ R L M ∘ₗ d₁₂ R L M = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x y : Derivation R A' A' × Derivation R A A
hx : x ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
hy : y ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}
⊢ ⁅x, y⁆ ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
⊢ a ∈ twoCocycle R L M ↔ (d₂₃ R L M) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: 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

Tactic:
by

Goal state after: