mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
m : M
hm : m ∈ range ⇑P.root
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
⊢ f m ∈ range ⇑P₂.root

Tactic:
have (k : b.support) : (P.reflection k).trans f = f.trans (P₂.reflection (e k)) := by
    suffices ∀ j : b.support,
        (P.reflection k).trans f (P.root j) = f.trans (P₂.reflection (e k)) (P.root j) by
      rw [← LinearEquiv.toLinearMap_inj]
      exact b.toWeightBasis.ext fun j ↦ by simpa using this j
    intro j
    suffices P₂.pairing (e j) (e k) = P.pairing j k by simp [reflection_apply, hf, this]
    simpa only [cartanMatrixIn_def, algebraMap_pairingIn] using congr_arg (algebraMap ℤ R) (he j k)
  obtain ⟨i, rfl⟩ := hm
  apply b.induction_reflect i
  · exact fun j ⟨k, hk⟩ ↦ ⟨P₂.reflectionPerm k k, by simpa⟩
  · exact fun j hj ↦ ⟨e ⟨j, hj⟩, (hf _).symm⟩
  · intro j k ⟨l, hl⟩ hk
    replace this : f (P.reflection k (P.root j)) = (P₂.reflection (e ⟨k, hk⟩)) (f (P.root j)) := by
      simpa using LinearEquiv.congr_fun (this ⟨k, hk⟩) (P.root j)
    rw [root_reflectionPerm, this, ← hl, ← root_reflectionPerm]
    exact mem_range_self _

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
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ ∀ b ∈ univ, b ≠ 0 → (-1) ^ ↑b * W 0 b * (W.submatrix succ b.succAbove).det = 0

Tactic:
intro j _ hj0

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
j : Fin n.succ
a✝ : j ∈ univ
hj0 : j ≠ 0
⊢ (-1) ^ ↑j * W 0 j * (W.submatrix succ j.succAbove).det = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ projVandermonde v w =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
      (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))

Tactic:
simp [← Matrix.ext_iff, projVandermonde_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
u : Bool → Fin n → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun b i ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X (i, b))
hdet :
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1).mapMatrix
        (projVandermonde (fun i ↦ MvPolynomial.X (i, true)) fun i ↦ MvPolynomial.X (i, false))).det =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))
⊢ ∏ i, ∏ j > i, (v j * w i - v i * w j) =
    (MvPolynomial.eval₂Hom (Int.castRingHom R) fun x ↦ (if x.2 = true then v else w) x.1)
      (∏ i,
        ∏ i_1 > i,
          (MvPolynomial.X (i_1, true) * MvPolynomial.X (i, false) -
            MvPolynomial.X (i, true) * MvPolynomial.X (i_1, false)))

Tactic:
simp [← Matrix.ext_iff, projVandermonde_apply]

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

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
⊢ (dx ^ (k + 1)) y ∈ Submodule.comap N.subtype H.toSubmodule

Tactic:
simp only [pow_succ', Module.End.mul_apply, Submodule.mem_comap, mem_toSubmodule]

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
⊢ N.subtype (dx ((dx ^ k) y)) ∈ H
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
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v) r) / eval x 1 =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹

Tactic:
← interpolate_one hvs hs,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v) r) / eval x ((interpolate s v) 1) =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j : ι
⊢ (GradedRing.proj 𝒜 j) (r * x) ∈ I

Tactic:
classical
  rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
  apply Ideal.sum_mem
  intro k _
  obtain ⟨i, hi⟩ := hx₁
  have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) :=
    GradedMul.mul_mem (SetLike.coe_mem _) hi
  rw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]
  split_ifs
  · exact I.mul_mem_left _ hx₂
  · exact I.zero_mem

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : degree d ≠ n
⊢ coeff d φ = 0

Tactic:
rw [degree_eq_weight_one] at hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun x ↦ 1) d ≠ n
⊢ coeff d φ = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : coeff d 0 = coeff d φ
⊢ coeff d φ = 0

Tactic:
coeff_zero

Goal state after:
case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 0
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
⊢ 0 = coeff x 0

Tactic:
coeff_zero

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 = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = coeff d 0

Tactic:
coeff_zero

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
I : Ideal (MvPolynomial σ R)
h : Ideal.IsHomogeneous (weightedHomogeneousSubmodule R w) I
p : MvPolynomial σ R
⊢ p ∈ I ↔ ∀ (m : M), (weightedHomogeneousComponent w m) p ∈ I

Tactic:
by
  simp_rw [← weightedDecomposition.decompose'_apply]
  exact h.mem_iff

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
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
⊢ φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'

Tactic:
let f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) :=
    Polynomial.map (MvPolynomial.aeval X).toRingHom
  have hf : Function.Injective f := by
    simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]
    exact Polynomial.map_injective (RingHom.id _) Function.injective_id
  apply hf
  let _h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
    Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)
  let _h2 : Module.Free (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
    Module.Free.of_basis (basis (MvPolynomial ι R) bₘ)
  simp only [f, polyCharpolyAux_map_aeval, polyCharpolyAux_map_aeval]

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
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
b : Basis ι R L
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff φ.nilRank ≠ 0

Tactic:
rw [nilRank_eq_polyCharpoly_natTrailingDegree _ b]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
b : Basis ι R L
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
⊢ (lieCharpoly R M x y).natDegree = finrank R M

Tactic:
rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]

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

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (↑(MvPolynomial.aeval fun i ↦ (aeval r) (C ((b.repr y) i) * X) + (aeval r) (C ((b.repr x) i))))
      ((↑φ).polyCharpoly b) =
    charpoly (φ (r • y) + φ x)

Tactic:
map_mul,

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map
      (↑(MvPolynomial.aeval fun i ↦ (aeval r) (C ((b.repr y) i)) * (aeval r) X + (aeval r) (C ((b.repr x) i))))
      ((↑φ).polyCharpoly b) =
    charpoly (φ (r • y) + φ x)
Module: Mathlib.LinearAlgebra.Matrix.Diagonal

Goal state before:
pp: m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ (toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })

Tactic:
have hIJ : IsCompl { i : m | w i ≠ 0 } { i : m | w i = 0 } := isCompl_compl.symm
  have B₁ := iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) hIJ (Set.toFinite _)
  rw [LinearMap.rank, range_diagonal, B₁, ← @rank_fun' K]
  exact iInfKerProjEquiv K (fun _ ↦ K) hIJ.disjoint hIJ.codisjoint.top_le |>.rank_eq

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (1 • -1).det = 1

Tactic:
smul_neg,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-(1 • 1)).det = 1
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:
ext; simp; 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
⊢ ⟨{
        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:
ext; simp; 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✝ : 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:
ext; simp; 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✝ : 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:
ext; simp; 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)
⊢ {
      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:
ext; simp; abel

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 : Matrix l l R
hX_symm : X.IsSymm
hXY : X.map ⇑f = Y
⊢ ((IsLocalRing.residue R).mapMatrix A + (IsLocalRing.residue R).mapMatrix (X * C)).det ≠ 0

Tactic:
map_mul,

Goal state after:
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 : Matrix l l R
hX_symm : X.IsSymm
hXY : X.map ⇑f = Y
⊢ ((IsLocalRing.residue R).mapMatrix A +
        (IsLocalRing.residue R).mapMatrix X * (IsLocalRing.residue R).mapMatrix C).det ≠
    0
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mul_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c' : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (a✝¹ * c') = (liftAux R f) (b✝ * c')

Tactic:
| mul_right c' _ h₂ =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
⊢ x = y

Tactic:
have := (Function.Bijective.of_comp_iff (lmap (ℳ · |>.toBaseChange S))
    (by rw [← LinearEquiv.coe_trans]; exact LinearEquiv.bijective _)).1
    (decompose (M := S ⊗[R] M) fun i ↦ (ℳ i).baseChange S).bijective
  refine of_injective (β := fun i ↦ S ⊗[R] ℳ i) i <| this.injective ?_
  simpa using congr(of (fun i ↦ (ℳ i).baseChange S) i $h)

Goal state after: