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

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

Tactic:
by rw [rank, Matrix.range_mulVecLin]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
⊢ 0ᵀ = 0 ∧ 0ᵀ = 0 ∧ IsSymm 0

Tactic:
simp

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
⊢ 0 ∈ {c | ∀ (x : L), (c x) x = 0}

Tactic:
simp

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✝¹ x✝ : L
⊢ ⁅x, f (x✝¹ + x✝)⁆ - ⁅x✝¹ + x✝, f x⁆ - f ⁅x, x✝¹ + x✝⁆ =
    ⁅x, f x✝¹⁆ - ⁅x✝¹, f x⁆ - f ⁅x, x✝¹⁆ + (⁅x, f x✝⁆ - ⁅x✝, f x⁆ - f ⁅x, x✝⁆)

Tactic:
simp

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

Tactic:
simp

Goal state after:
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✝¹ x✝ : L
⊢ ⁅x✝², f x✝⁆ + ⁅x✝¹, f x✝⁆ - (⁅x✝, f x✝²⁆ + ⁅x✝, f x✝¹⁆) - (f ⁅x✝², x✝⁆ + f ⁅x✝¹, x✝⁆) =
    ⁅x✝², f x✝⁆ - ⁅x✝, f x✝²⁆ - f ⁅x✝², x✝⁆ + (⁅x✝¹, f x✝⁆ - ⁅x✝, f x✝¹⁆ - f ⁅x✝¹, x✝⁆)
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:
simp

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
x✝¹ x✝ : L
⊢ (↑⟨{
              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' := ⋯ },
            ⋯⟩
        x✝¹)
      x✝ =
    (↑(⟨{ 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' := ⋯ },
              ⋯⟩)
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
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
x✝¹ x✝ : L
⊢ ⁅x✝¹, x✝³ x✝⁆ + ⁅x✝¹, x✝² x✝⁆ - (⁅x✝, x✝³ x✝¹⁆ + ⁅x✝, x✝² x✝¹⁆) - (x✝³ ⁅x✝¹, x✝⁆ + x✝² ⁅x✝¹, x✝⁆) =
    ⁅x✝¹, x✝³ x✝⁆ - ⁅x✝, x✝³ x✝¹⁆ - x✝³ ⁅x✝¹, x✝⁆ + (⁅x✝¹, x✝² x✝⁆ - ⁅x✝, x✝² x✝¹⁆ - x✝² ⁅x✝¹, x✝⁆)
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:
simp

Goal state after:
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, (a y) x✝⁆ - (⁅y, (a x) x✝¹⁆ + ⁅y, (a x) x✝⁆) + (⁅x✝¹, (a x) y⁆ + ⁅x✝, (a x) y⁆) -
          ((a ⁅x, y⁆) x✝¹ + (a ⁅x, y⁆) x✝) +
        ((a ⁅x, x✝¹⁆) y + (a ⁅x, x✝⁆) y) -
      ((a ⁅y, x✝¹⁆) x + (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 +
      (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)
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:
simp

Goal state after:
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✝¹ • ⁅x, (a y) x✝⁆ - x✝¹ • ⁅y, (a x) x✝⁆ + x✝¹ • ⁅x✝, (a x) y⁆ - x✝¹ • (a ⁅x, y⁆) x✝ + x✝¹ • (a ⁅x, x✝⁆) y -
      x✝¹ • (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)
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✝¹ • ⁅x, (a y) x✝⁆ +
      (-1 • x✝¹ • ⁅y, (a x) x✝⁆ +
        (x✝¹ • ⁅x✝, (a x) y⁆ + (-1 • x✝¹ • (a ⁅x, y⁆) x✝ + (x✝¹ • (a ⁅x, x✝⁆) y + -1 • x✝¹ • (a ⁅y, x✝⁆) x)))) =
    x✝¹ •
      (⁅x, (a y) x✝⁆ +
        (-1 • ⁅y, (a x) x✝⁆ + (⁅x✝, (a x) y⁆ + (-1 • (a ⁅x, y⁆) x✝ + ((a ⁅x, x✝⁆) y + -1 • (a ⁅y, x✝⁆) x)))))

Tactic:
simp

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✝¹ 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' := ⋯ }
      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' := ⋯ } +
        {
          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' := ⋯ })
      x✝

Tactic:
simp

Goal state after:
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✝¹ x✝ : L
⊢ ⁅x, (a x✝²) x✝⁆ + ⁅x, (a x✝¹) x✝⁆ - (⁅x✝², (a x) x✝⁆ + ⁅x✝¹, (a x) x✝⁆) + (⁅x✝, (a x) x✝²⁆ + ⁅x✝, (a x) x✝¹⁆) -
          ((a ⁅x, x✝²⁆) x✝ + (a ⁅x, x✝¹⁆) x✝) +
        ((a ⁅x, x✝⁆) x✝² + (a ⁅x, x✝⁆) x✝¹) -
      ((a ⁅x✝², x✝⁆) x + (a ⁅x✝¹, x✝⁆) x) =
    ⁅x, (a x✝²) x✝⁆ - ⁅x✝², (a x) x✝⁆ + ⁅x✝, (a x) x✝²⁆ - (a ⁅x, x✝²⁆) x✝ + (a ⁅x, x✝⁆) x✝² - (a ⁅x✝², x✝⁆) x +
      (⁅x, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x) x✝⁆ + ⁅x✝, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) x✝ + (a ⁅x, x✝⁆) x✝¹ - (a ⁅x✝¹, x✝⁆) x)
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✝¹ 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' := ⋯ }
      x✝ =
    ((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' := ⋯ })
      x✝

Tactic:
simp

Goal state after:
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✝¹ x✝ : L
⊢ x✝² • ⁅x, (a x✝¹) x✝⁆ - x✝² • ⁅x✝¹, (a x) x✝⁆ + x✝² • ⁅x✝, (a x) x✝¹⁆ - x✝² • (a ⁅x, x✝¹⁆) x✝ +
        x✝² • (a ⁅x, x✝⁆) x✝¹ -
      x✝² • (a ⁅x✝¹, x✝⁆) x =
    x✝² • (⁅x, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x) x✝⁆ + ⁅x✝, (a x) x✝¹⁆ - (a ⁅x, x✝¹⁆) x✝ + (a ⁅x, x✝⁆) x✝¹ - (a ⁅x✝¹, x✝⁆) x)
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✝¹ x✝ : L
⊢ x✝² • ⁅x, (a x✝¹) x✝⁆ +
      (-1 • x✝² • ⁅x✝¹, (a x) x✝⁆ +
        (x✝² • ⁅x✝, (a x) x✝¹⁆ + (-1 • x✝² • (a ⁅x, x✝¹⁆) x✝ + (x✝² • (a ⁅x, x✝⁆) x✝¹ + -1 • x✝² • (a ⁅x✝¹, x✝⁆) x)))) =
    x✝² •
      (⁅x, (a x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (a x) x✝⁆ + (⁅x✝, (a x) x✝¹⁆ + (-1 • (a ⁅x, x✝¹⁆) x✝ + ((a ⁅x, x✝⁆) x✝¹ + -1 • (a ⁅x✝¹, x✝⁆) x)))))

Tactic:
simp

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✝¹ 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' := ⋯ }
        x✝¹)
      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' := ⋯ } +
          {
            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' := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
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✝¹ x✝ : L
⊢ ⁅x✝³, (a x✝¹) x✝⁆ + ⁅x✝², (a x✝¹) x✝⁆ - (⁅x✝¹, (a x✝³) x✝⁆ + ⁅x✝¹, (a x✝²) x✝⁆) +
            (⁅x✝, (a x✝³) x✝¹⁆ + ⁅x✝, (a x✝²) x✝¹⁆) -
          ((a ⁅x✝³, x✝¹⁆) x✝ + (a ⁅x✝², x✝¹⁆) x✝) +
        ((a ⁅x✝³, x✝⁆) x✝¹ + (a ⁅x✝², x✝⁆) x✝¹) -
      ((a ⁅x✝¹, x✝⁆) x✝³ + (a ⁅x✝¹, x✝⁆) x✝²) =
    ⁅x✝³, (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝³) x✝⁆ + ⁅x✝, (a x✝³) x✝¹⁆ - (a ⁅x✝³, x✝¹⁆) x✝ + (a ⁅x✝³, x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝³ +
      (⁅x✝², (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝²) x✝⁆ + ⁅x✝, (a x✝²) x✝¹⁆ - (a ⁅x✝², x✝¹⁆) x✝ + (a ⁅x✝², x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝²)
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✝² 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' := ⋯ }
        x✝¹)
      x✝ =
    (((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' := ⋯ })
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
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✝² x✝¹ x✝ : L
⊢ x✝³ • ⁅x✝², (a x✝¹) x✝⁆ - x✝³ • ⁅x✝¹, (a x✝²) x✝⁆ + x✝³ • ⁅x✝, (a x✝²) x✝¹⁆ - x✝³ • (a ⁅x✝², x✝¹⁆) x✝ +
        x✝³ • (a ⁅x✝², x✝⁆) x✝¹ -
      x✝³ • (a ⁅x✝¹, x✝⁆) x✝² =
    x✝³ •
      (⁅x✝², (a x✝¹) x✝⁆ - ⁅x✝¹, (a x✝²) x✝⁆ + ⁅x✝, (a x✝²) x✝¹⁆ - (a ⁅x✝², x✝¹⁆) x✝ + (a ⁅x✝², x✝⁆) x✝¹ -
        (a ⁅x✝¹, x✝⁆) x✝²)
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✝² x✝¹ x✝ : L
⊢ x✝³ • ⁅x✝², (a x✝¹) x✝⁆ +
      (-1 • x✝³ • ⁅x✝¹, (a x✝²) x✝⁆ +
        (x✝³ • ⁅x✝, (a x✝²) x✝¹⁆ +
          (-1 • x✝³ • (a ⁅x✝², x✝¹⁆) x✝ + (x✝³ • (a ⁅x✝², x✝⁆) x✝¹ + -1 • x✝³ • (a ⁅x✝¹, x✝⁆) x✝²)))) =
    x✝³ •
      (⁅x✝², (a x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (a x✝²) x✝⁆ +
          (⁅x✝, (a x✝²) x✝¹⁆ + (-1 • (a ⁅x✝², x✝¹⁆) x✝ + ((a ⁅x✝², x✝⁆) x✝¹ + -1 • (a ⁅x✝¹, x✝⁆) x✝²)))))

Tactic:
simp

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)
x✝² x✝¹ x✝ : L
⊢ (({
            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' := ⋯ }
          x✝²)
        x✝¹)
      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' := ⋯ } +
            {
              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' := ⋯ })
          x✝²)
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
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)
x✝² x✝¹ x✝ : L
⊢ ⁅x✝², (x✝⁴ x✝¹) x✝⁆ + ⁅x✝², (x✝³ x✝¹) x✝⁆ - (⁅x✝¹, (x✝⁴ x✝²) x✝⁆ + ⁅x✝¹, (x✝³ x✝²) x✝⁆) +
            (⁅x✝, (x✝⁴ x✝²) x✝¹⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆) -
          ((x✝⁴ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝¹⁆) x✝) +
        ((x✝⁴ ⁅x✝², x✝⁆) x✝¹ + (x✝³ ⁅x✝², x✝⁆) x✝¹) -
      ((x✝⁴ ⁅x✝¹, x✝⁆) x✝² + (x✝³ ⁅x✝¹, x✝⁆) x✝²) =
    ⁅x✝², (x✝⁴ x✝¹) x✝⁆ - ⁅x✝¹, (x✝⁴ x✝²) x✝⁆ + ⁅x✝, (x✝⁴ x✝²) x✝¹⁆ - (x✝⁴ ⁅x✝², x✝¹⁆) x✝ + (x✝⁴ ⁅x✝², x✝⁆) x✝¹ -
        (x✝⁴ ⁅x✝¹, x✝⁆) x✝² +
      (⁅x✝², (x✝³ x✝¹) x✝⁆ - ⁅x✝¹, (x✝³ x✝²) x✝⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆ - (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝⁆) x✝¹ -
        (x✝³ ⁅x✝¹, x✝⁆) x✝²)
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:
classical
  let el : Basis l R (l → R) := Pi.basisFun R l
  let em : Basis m R (m → R) := Pi.basisFun R m
  let en : Basis n R (n → R) := Pi.basisFun R n
  rw [Matrix.rank_eq_finrank_range_toLin A el em,
      Matrix.rank_eq_finrank_range_toLin B em en,
      ← Module.finrank_fintype_fun_eq_card R,
      ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
      add_le_add_iff_left]
  apply Submodule.finrank_mono
  rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]

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)
x✝² x✝¹ x✝ : L
⊢ (({
            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' := ⋯ }
          x✝²)
        x✝¹)
      x✝ =
    ((((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' := ⋯ })
          x✝²)
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
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)
x✝² x✝¹ x✝ : L
⊢ x✝⁴ • ⁅x✝², (x✝³ x✝¹) x✝⁆ - x✝⁴ • ⁅x✝¹, (x✝³ x✝²) x✝⁆ + x✝⁴ • ⁅x✝, (x✝³ x✝²) x✝¹⁆ - x✝⁴ • (x✝³ ⁅x✝², x✝¹⁆) x✝ +
        x✝⁴ • (x✝³ ⁅x✝², x✝⁆) x✝¹ -
      x✝⁴ • (x✝³ ⁅x✝¹, x✝⁆) x✝² =
    x✝⁴ •
      (⁅x✝², (x✝³ x✝¹) x✝⁆ - ⁅x✝¹, (x✝³ x✝²) x✝⁆ + ⁅x✝, (x✝³ x✝²) x✝¹⁆ - (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝³ ⁅x✝², x✝⁆) x✝¹ -
        (x✝³ ⁅x✝¹, x✝⁆) x✝²)
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)
x✝² x✝¹ x✝ : L
⊢ x✝⁴ • ⁅x✝², (x✝³ x✝¹) x✝⁆ +
      (-1 • x✝⁴ • ⁅x✝¹, (x✝³ x✝²) x✝⁆ +
        (x✝⁴ • ⁅x✝, (x✝³ x✝²) x✝¹⁆ +
          (-1 • x✝⁴ • (x✝³ ⁅x✝², x✝¹⁆) x✝ + (x✝⁴ • (x✝³ ⁅x✝², x✝⁆) x✝¹ + -1 • x✝⁴ • (x✝³ ⁅x✝¹, x✝⁆) x✝²)))) =
    x✝⁴ •
      (⁅x✝², (x✝³ x✝¹) x✝⁆ +
        (-1 • ⁅x✝¹, (x✝³ x✝²) x✝⁆ +
          (⁅x✝, (x✝³ x✝²) x✝¹⁆ + (-1 • (x✝³ ⁅x✝², x✝¹⁆) x✝ + ((x✝³ ⁅x✝², x✝⁆) x✝¹ + -1 • (x✝³ ⁅x✝¹, x✝⁆) x✝²)))))

Tactic:
simp

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
a : A
⊢ 0 = 0 a

Tactic:
simp

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:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: 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), (LinearMap.rTensor L ↑d) (x + y) = (LinearMap.rTensor L ↑d) x + (LinearMap.rTensor L ↑d) y

Tactic:
simp

Goal state after: