mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
⊢ ¬g.LimZero

Tactic:
simpa using show ¬LimZero (g - 0) from hg

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
i : ι
this : InvolutiveNeg ι := P.indexNeg
j : ι
x : M
⊢ (P.reflection (-j)) x = (P.reflection j) x

Tactic:
simp [reflection_apply, two_smul]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝⁵ : CommRing α
inst✝⁴ : StarRing α
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)

Tactic:
abel

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝⁵ : CommRing α
inst✝⁴ : StarRing α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
x : m → α
y : n → α
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)

Tactic:
abel

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

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)

Tactic:
← neg_add,

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-(↑k + ↑l)) = A ^ (-↑k) * A ^ (-↑l)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ QuadraticMap.PosDef Q

Tactic:
rw [← Q.toQuadraticMap_associated ℝ,
    ← (LinearMap.toMatrix₂' ℝ).left_inv (Q.associatedHom ℝ)]

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((QuadraticMap.associatedHom ℝ) Q)))).PosDef
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: case refine_1
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (a : R), ((aeval f) (C a)) x = eval μ (C a) • x

Tactic:
intro a; simp [Module.algebraMap_end_apply]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
⊢ (ascPochhammer S (n + 1)).Monic

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval x (map (algebraMap R S) ((ascPochhammer R n).comp p)) = eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p)

Tactic:
eval_map

Goal state after:
S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p) = eval₂ (algebraMap R S) x ((ascPochhammer R n).comp p)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
⊢ (ascPochhammer S (n + 1)).natDegree = n + 1

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
⊢ (descPochhammer R (n + 1)).Monic

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
have hW_eq : (W.submatrix succ succ) = .of fun i j ↦ (v (succ i) - r * w (succ i)) *
      projVandermonde (v ∘ succ) (w ∘ succ) i j := by
    ext i j
    simp only [projVandermonde_apply, val_zero, rev_zero, val_last, val_succ,
      val_castSucc, submatrix_apply, Function.comp_apply, rev_succ,
      W, r, rev_castSucc]
    simp
    ring

Goal state after:
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₁
this✝ : IsLieAbelian ↥H₁
i : ι₁
this : ⁅b₁.h' i, x⁆ = 0
⊢ ⁅(↑⟨(b₁.h i, b₂.h (eι i)), ⋯⟩).1, ↑x⁆ = 0

Tactic:
simpa [Subtype.ext_iff, Basis.h'] using this

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = (interpolate s v) r

Tactic:
by
  constructor <;> intro h
  · exact eq_interpolate_of_eval_eq _ hvs h.1 h.2
  · rw [h]
    exact ⟨degree_interpolate_lt _ hvs, fun _ hi => eval_interpolate_at_node _ hvs hi⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ (vandermonde fun i ↦ ↑↑i).det = ↑(n + 1).superFactorial

Tactic:
| succ n hn =>

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
⊢ (∃ k, (((ad R L) x - 0 • 1) ^ k) y = 0) ↔ ∃ n, ((ad R L) x ^ n) y = 0

Tactic:
by simp only [zero_smul, sub_zero]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hj : j ∈ (f i).vars
⊢ ∃ a ∈ φ.vars, j ∈ (f a).vars

Tactic:
exact ⟨i, (mem_vars_iff_mem_support _).mpr ⟨d, hd, hi⟩, hj⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
⊢ j ∈ s → IsWeightedHomogeneous w (φ j) (n j)

Tactic:
hjs

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ S, span (Subtype.val '' s₁) * span (Subtype.val '' s₂) = span (Subtype.val '' S)

Tactic:
rw [Ideal.span_mul_span']

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ S, span (Subtype.val '' s₁ * Subtype.val '' s₂) = span (Subtype.val '' S)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0

Tactic:
rw [if_neg]

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0

case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weight w) x = n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ coeff (mapDomain f d) ((rename f) φ) ≠ 0

Tactic:
· rwa [coeff_rename_mapDomain f hf]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ∀ b ∈ DFinsupp.support x, b ≠ m → (weightedHomogeneousComponent w m) ↑(x b) = 0

Tactic:
intro n _ hmn
    exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
hF₀ : F ≠ 0
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
j : ℕ
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hF : F.IsHomogeneous ((finSuccEquiv R N) F).natDegree
hnR : ↑((finSuccEquiv R N) F).natDegree ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < ((finSuccEquiv R N) F).natDegree + 1
hin✝ : i ≤ ((finSuccEquiv R N) F).natDegree
hFn : ((finSuccEquiv R N) F).coeff ((finSuccEquiv R N) F).natDegree = 0
hin : i < ((finSuccEquiv R N) F).natDegree
hj : i + (j + 1) = ((finSuccEquiv R N) F).natDegree
⊢ (finSuccEquiv R N) F ≠ 0

Tactic:
simpa using! (finSuccEquiv R N).injective.ne hF₀

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ = φ

Tactic:
by
  ext1 d
  suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by
    simpa [coeff_sum, coeff_homogeneousComponent]
  exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
hp : p.IsHomogeneous n
⊢ (homogeneousComponent n) p = p

Tactic:
simp [homogeneousComponent_of_mem hp]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ (φ.polyCharpoly (chooseBasis R L)).coeff (Fintype.card ι) ≠ 0

Tactic:
← Module.finrank_eq_card_basis b,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ (φ.polyCharpoly (chooseBasis R L)).coeff (finrank R M) ≠ 0
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 : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ ∈ symplecticGroup l R
⊢ A ∈ symplecticGroup l R

Tactic:
simpa using transpose_mem hA

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

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : DecidableEq n
inst✝ : StrongRankCondition R
⊢ finrank R ↥⊤ = Fintype.card n

Tactic:
finrank_top,

Goal state after:
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : DecidableEq n
inst✝ : StrongRankCondition R
⊢ finrank R (n → R) = Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case inl
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : IsEmpty n
⊢ cRank 0 = 0

Tactic:
rw [cRank, range_eq_empty, span_empty, rank_bot]

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, 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✝⁆)

Tactic:
abel

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✝¹, 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✝⁆)

Tactic:
abel

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
⊢ ⁅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

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

Tactic:
abel

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

Tactic:
abel

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
⊢ ⁅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✝²)

Tactic:
abel

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
⊢ ⁅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✝²)

Tactic:
abel

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

Tactic:
abel

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
this : a ⁅y, ⁅z, x⁆⁆ = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆
⊢ ⁅x, ⁅y, a z⁆⁆ - ⁅x, ⁅z, a y⁆⁆ - -⁅x, a ⁅z, y⁆⁆ - (⁅y, ⁅x, a z⁆⁆ - ⁅y, ⁅z, a x⁆⁆ - -⁅y, a ⁅z, x⁆⁆) +
            (⁅z, ⁅x, a y⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - -⁅z, a ⁅y, x⁆⁆) -
          (⁅x, ⁅y, a z⁆⁆ - ⁅y, ⁅x, a z⁆⁆ - -⁅z, a ⁅y, x⁆⁆ - (-a ⁅x, ⁅z, y⁆⁆ - -(a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆))) +
        (⁅x, ⁅z, a y⁆⁆ - ⁅z, ⁅x, a y⁆⁆ - -⁅y, a ⁅z, x⁆⁆ - (a ⁅x, ⁅z, y⁆⁆ - -a ⁅z, ⁅y, x⁆⁆)) -
      (⁅y, ⁅z, a x⁆⁆ - ⁅z, ⁅y, a x⁆⁆ - -⁅x, a ⁅z, y⁆⁆ - (a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆ - a ⁅z, ⁅y, x⁆⁆)) =
    0

Tactic:
abel

Goal state after:
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)
h : (d₂₃ R L M) a = 0
x y z : L
this : -(a ⁅x, y⁆) z + (a ⁅x, z⁆) y = (a ⁅y, z⁆) x
⊢ -(-(a ⁅x, y⁆) z + (a ⁅x, z⁆) y) = (a ⁅x, y⁆) z + -(a ⁅x, z⁆) y

Tactic:
abel

Goal state after:
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)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
x y z : L
⊢ -(a ⁅x, y⁆) z + -(a y) ⁅x, z⁆ - -((a ⁅x, y⁆) z + (a y) ⁅x, z⁆) = 0

Tactic:
abel

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
x✝³ x✝² : Derivation R A A
z x✝¹ x✝ : A ⊗[R] L
hx :
  (LinearMap.rTensor L ⁅↑x✝³, ↑x✝²⁆) x✝¹ =
    (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝¹) -
      (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝¹)
hy :
  (LinearMap.rTensor L ⁅↑x✝³, ↑x✝²⁆) x✝ =
    (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝) -
      (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝)
⊢ (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝¹) -
        (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝¹) +
      ((LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝) -
        (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝)) =
    (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝¹) +
        (LinearMap.rTensor L ↑x✝³) ((LinearMap.rTensor L ↑x✝²) x✝) -
      ((LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝¹) +
        (LinearMap.rTensor L ↑x✝²) ((LinearMap.rTensor L ↑x✝³) x✝))

Tactic:
abel

Goal state after: