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
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)

Tactic:
abel_nf

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✝⁆ +
      (-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)))))
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✝⁆ - 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)

Tactic:
abel_nf

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✝⁆ +
      (-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)))))
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✝⁆ - 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✝²)

Tactic:
abel_nf

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✝⁆ +
      (-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✝²)))))
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✝⁆ - 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✝²)

Tactic:
abel_nf

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✝⁆ +
      (-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✝²)))))
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
  ext a x y z
  have (a : oneCochain R L M) (x : L) : d₁₂ R L M a x = (d₁₂ R L M a).val x := rfl
  simp only [LinearMap.comp_apply, d₂₃_apply, LinearMap.zero_apply, this,
    d₁₂_apply_coe_apply_apply R L M, lie_sub, lie_lie]
  rw [leibniz_lie y x, leibniz_lie z x, leibniz_lie z y]
  have : a ⁅y, ⁅z, x⁆⁆ = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆ := by
    rw [congr_arg a (leibniz_lie y z x), ← lie_skew, ← lie_skew z y, lie_neg, map_add]
  simp only [lie_lie, sub_add_cancel, map_sub, ← lie_skew x y, ← lie_skew x z, ← lie_skew y z,
    lie_neg, map_neg, this]
  abel

Goal state after:
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
h1 :
  (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, x✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ - ⁅x✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆
h2 :
  (LinearMap.lTensor A ↑d) ⁅x✝¹ ⊗ₜ[R] y✝¹, y✝⁆ =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ - ⁅y✝, (LinearMap.lTensor A ↑d) (x✝¹ ⊗ₜ[R] y✝¹)⁆
⊢ ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ - ⁅x✝, x✝¹ ⊗ₜ[R] d y✝¹⁆ +
      (⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ - ⁅y✝, x✝¹ ⊗ₜ[R] d y✝¹⁆) =
    ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) x✝⁆ + ⁅x✝¹ ⊗ₜ[R] y✝¹, (LinearMap.lTensor A ↑d) y✝⁆ -
      (⁅x✝, x✝¹ ⊗ₜ[R] d y✝¹⁆ + ⁅y✝, x✝¹ ⊗ₜ[R] d y✝¹⁆)

Tactic:
abel_nf

Goal state after:
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 x✝ y✝ : A ⊗[R] L
h1 : (LinearMap.lTensor A ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x✝⁆
h2 : (LinearMap.lTensor A ↑d) ⁅y✝, y⁆ = ⁅y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y✝⁆
⊢ ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x✝⁆ +
      (⁅y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y✝⁆) =
    ⁅x✝, (LinearMap.lTensor A ↑d) y⁆ + ⁅y✝, (LinearMap.lTensor A ↑d) y⁆ -
      (⁅y, (LinearMap.lTensor A ↑d) x✝⁆ + ⁅y, (LinearMap.lTensor A ↑d) y✝⁆)

Tactic:
abel_nf

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

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ (toModule R ι L' fun i ↦ ↑(f i)) (((LieAlgebra.ad R (⨁ (i : ι), L i)) x) y) =
    ((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x)) ((toModule R ι L' fun i ↦ ↑(f i)) y)

Tactic:
← LinearMap.comp_apply,

Goal state after:
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ ((toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) x) y =
    ((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x)) ((toModule R ι L' fun i ↦ ↑(f i)) y)
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f') (((LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) x) =
    ((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y))) ((toModule R ι L' f') x)

Tactic:
← LinearMap.comp_apply,

Goal state after:
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (toModule R ι L' f' ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) x =
    ((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y))) ((toModule R ι L' f') x)
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
⊢ A'ᵀ * C' = C'ᵀ * A'

Tactic:
by
      change f.mapMatrix Aᵀ * f.mapMatrix C = f.mapMatrix Cᵀ * f.mapMatrix A
      rw [← map_mul, (fromBlocks_mem_iff.1 hA).1, map_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
Y : Matrix l l k
hY_symm : Y.IsSymm
hY_det : IsUnit (A' + Y * C')
⊢ ∃ X, X.IsSymm ∧ X.map ⇑f = Y

Tactic:
by
    choose s hs using @IsLocalRing.residue_surjective R _ _
    exact ⟨Y.map s, hY_symm.map s, Matrix.ext fun i j ↦ hs (Y i j)⟩

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
        rw [map_mul] at this; simp [LieRing.of_associative_ring_bracket, ← this]

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a + b) (a + c)

Tactic:
by
  rw [add_comm _ b, add_comm _ c]; exact h.add_right _

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

Goal state before:
pp: R : Type u
X : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X ((t • 1) • a) (t • b)

Tactic:
← smul_one_smul R t b

Goal state after:
R : Type u
X : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X ((t • 1) • a) ((t • 1) • b)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
w : A
x : V
hx : x ∈ (⨆ k, U' k).carrier
⊢ ⁅w, x⁆ ∈ (⨆ k, U' k).carrier

Tactic:
show ⁅w, x⁆ = (T χ w) x + χ w • x by simp

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
w : A
x : V
hx : x ∈ (⨆ k, U' k).carrier
⊢ (T χ w) x + χ w • x ∈ (⨆ k, U' k).carrier
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : (x :: y :: l).formPerm w ≠ w
this : w ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x w

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem this

Goal state after:
case h.right
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
tail_ih✝ : ∀ (x : α), (x :: l).Nodup → 2 ≤ (x :: l).length → (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw : (x :: y :: l).formPerm (x :: y :: l)[k] ≠ (x :: y :: l)[k]
this : (x :: y :: l)[k] ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x (x :: y :: l)[k]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support.card ≤ n

Tactic:
rw [← support_cycleOf_eq_nil_iff] at hx

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : (p.cycleOf x).support = ∅
⊢ (p.cycleOf x).support.card ≤ n
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - ⁅s ⁅z, y⁆, s x⁆ - (⁅s y, ⁅s x, s z⁆⁆ + ⁅s y, s ⁅z, x⁆⁆) +
            (⁅s y, ⁅s x, s z⁆⁆ - ⁅s x, ⁅s y, s z⁆⁆ - ⁅s z, s ⁅x, y⁆⁆) -
          (-⁅s z, s ⁅x, y⁆⁆ - (-s ⁅x, ⁅z, y⁆⁆ + s ⁅y, ⁅z, x⁆⁆)) +
        (⁅s y, s ⁅z, x⁆⁆ - s ⁅y, ⁅z, x⁆⁆) -
      (-⁅s ⁅z, y⁆, s x⁆ - s ⁅x, ⁅z, y⁆⁆) =
    0

Tactic:
abel_nf

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
simp only [coe_bracket_of_module, lie_smul]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : S.pairing δ γ = 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

Tactic:
S.reflectionPerm_eq_of_pairing_eq_zero hp

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : S.pairing δ γ = 0
⊢ rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_1
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(d ⟨p, ⋯⟩) ≠ ⊥

Tactic:
Ne,

Goal state after:
case refine_1
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ¬↑(d ⟨p, ⋯⟩) = ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ x * (spanSingleton R₁⁰ x)⁻¹ = 1

Tactic:
rw [spanSingleton_inv, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ hx, spanSingleton_one]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
μ : Weight K (↥H) L
hμ : μ.IsNonZero
⊢ b ∈ Weight.ker

Tactic:
have hμ_root : μ ∈ H.root := by simpa [LieSubalgebra.root] using hμ
    by_cases hμI : (⟨μ, hμ_root⟩ : H.root) ∈ I.rootSet
    · exact hspan_compl_roots_vanish ⟨μ, hμ_root⟩ hμI hb
    · exact I.root_apply_eq_zero_of_notMem_rootSet hbI hμI

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
P'' : Type u_4
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
I✝ J : FractionalIdeal S P
g✝ : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
⊢ map (↑g.symm) (map (↑g) I) = I

Tactic:
rw [← map_comp, AlgEquiv.symm_comp, map_id]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
⊢ P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥

Tactic:
Ne,

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : ¬(Multiset.map asIdeal Z).prod = ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
⊢ P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥