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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']

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

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosSemidef
x : m →₀ R
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * (A + B) i j * xj

Tactic:
simpa [mul_add, add_mul] using add_nonneg (hA.2 x) (hB.2 x)

Goal state after:
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
P : RootPairing ι R M N
b : P.Base
inst✝¹ : P.IsCrystallographic
inst✝ : CharZero R
i j : ↥b.support
⊢ cartanMatrixIn ℤ b i j = 0 ↔ P.pairing ↑i ↑j = 0

Tactic:
cartanMatrixIn_def,

Goal state after:
ι : 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✝¹ : P.IsCrystallographic
inst✝ : CharZero R
i j : ↥b.support
⊢ P.pairingIn ℤ ↑i ↑j = 0 ↔ P.pairing ↑i ↑j = 0
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
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ cartanMatrixIn ℤ b i j = -↑(chainTopCoeff ↑j ↑i)

Tactic:
cartanMatrixIn_def,

Goal state after:
ι : 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✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ P.pairingIn ℤ ↑i ↑j = -↑(chainTopCoeff ↑j ↑i)
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 ((ascPochhammer S n).comp (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)

Tactic:
by
  rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]

Goal state after:
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₂
⊢ ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})

Tactic:
prodCartan,

Goal state after:
ι₁ : 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₂
⊢ ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (lieSpan R ↥(prod eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
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₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
⊢ ∀ x ∈ {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}, ∀ y ∈ {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}, ⁅x, y⁆ = 0

Tactic:
simp [b₁.lie_h_h, b₂.lie_h_h]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: case hy
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodF eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

Tactic:
exact subset_lieSpan <| mem_union_right _ <| mem_range_self i

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: 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)
      (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).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
RingHom.map_det

Goal state after:
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).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₂
hy : (prodSymmEquiv eι b₁ b₂).symm y ∈ LieSubalgebra.map (prodSymmEquiv eι b₁ b₂).symm.toLieHom (prodCartan eι b₁ b₂)
⊢ (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁

Tactic:
prodCartan,

Goal state after:
ι₁ : 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₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    LieSubalgebra.map (prodSymmEquiv eι b₁ b₂).symm.toLieHom
      (lieSpan R ↥(prod eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
⊢ (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁
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
hy : ⁅y, x⁆ ∈ engel R x
⊢ y ∈ engel R x

Tactic:
← lie_skew,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hy : -⁅x, y⁆ ∈ engel R x
⊢ y ∈ engel R x
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
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
n : L
hn : ⁅n, x⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H

Tactic:
← lie_skew,

Goal state after:
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
n : L
hn : ⁅n, x⁆ ∈ H
⊢ -⁅n, x⁆ ∈ H
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
⊢ (φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars) ⊆ φ.vars.biUnion fun i ↦ (f i).vars

Tactic:
· intro j
    simp_rw [Finset.mem_biUnion]
    rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
    exact ⟨i, (mem_vars_iff_mem_support _).mpr ⟨d, hd, hi⟩, hj⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) = (LinearMap.toMatrix b b) φ

Tactic:
ext i j : 1

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
i j : ChooseBasisIndex R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) i j = (LinearMap.toMatrix b b) φ i j
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
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝ : DecidableEq M
d : σ →₀ ℕ
⊢ coeff d ((weightedHomogeneousComponent w n) φ) = if (weight w) d = n then coeff d φ else 0

Tactic:
by
  simp [weightedHomogeneousComponent, MvPolynomial, coeff, Finsupp.filter_apply]

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
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (∑ x ∈ Finite.toFinset ⋯, if (weight w) d = x then coeff d φ else 0) = coeff d φ

Tactic:
Finset.sum_eq_single (weight w d)

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = coeff d φ

case h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ b ∈ Finite.toFinset ⋯, b ≠ (weight w) d → (if (weight w) d = b then coeff d φ else 0) = 0

case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ Finite.toFinset ⋯ → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0
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
h : φ ≠ 0
⊢ φ.totalDegree = n

Tactic:
apply le_antisymm hφ.totalDegree_le

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ n ≤ φ.totalDegree
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
tfae_3_to_1 : (∀ (m : M), ∃ n, (φ ^ n) m = 0) → IsNilpotent φ
⊢ charpoly φ = X ^ (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree

Tactic:
φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
tfae_3_to_1 : (∀ (m : M), ∃ n, (φ ^ n) m = 0) → IsNilpotent φ
⊢ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree ↔ (charpoly φ).natTrailingDegree = (charpoly φ).natDegree
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
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : ¬m = n
⊢ 0 = coeff x 0

Tactic:
· simp only [coeff_zero]

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

Goal state before:
pp: case e_f.hC
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
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ ∀ (r : R),
    ((↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
          (MvPolynomial.map (algebraMap R A)))
        (C r) =
      ((MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))) (C r)

pp: case e_f.hX
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
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ ∀ (i : ιM × ιM),
    ((↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
          (MvPolynomial.map (algebraMap R A)))
        (X i) =
      ((MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))) (X i)

Tactic:
· intro r
    simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_C, bind₁_C_right]

Goal state after:
case e_f.hX
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
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ ∀ (i : ιM × ιM),
    ((↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
          (MvPolynomial.map (algebraMap R A)))
        (X i) =
      ((MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))) (X i)
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
i j : ℕ
hij : i + j = finrank R M
inst✝ : Nontrivial R
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j

Tactic:
rw [finrank_eq_card_chooseBasisIndex] at hij

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
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j
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
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ (↑(bind₁ (toMvPolynomial b (Free.chooseBasis R M).end φ))
        ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff i)).IsHomogeneous
    (1 * j)

Tactic:
apply (charpoly.univ_coeff_isHomogeneous _ _ _ _ hij).eval₂

Goal state after:
case hf
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
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (r : R), ((algebraMap R (MvPolynomial ι R)) r).IsHomogeneous 0

case hg
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
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Free.chooseBasis R M).end φ i).IsHomogeneous 1
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R r) A.mulVecLin.range) ≤ finrank R ↥A.mulVecLin.range

Tactic:
exact Submodule.finrank_map_le _ _

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ a (⁅⁅y, z⁆, x⁆ + ⁅z, ⁅y, x⁆⁆) = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆

Tactic:
← lie_skew,

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 : oneCochain R L M
x y z : L
this : ∀ (a : oneCochain R L M) (x : L), ((d₁₂ R L M) a) x = ↑((d₁₂ R L M) a) x
⊢ a (-⁅x, ⁅y, z⁆⁆ + ⁅z, ⁅y, x⁆⁆) = a ⁅x, ⁅z, y⁆⁆ + a ⁅z, ⁅y, x⁆⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ ({ toFun := single j, map_add' := ⋯ } ⁅x, m⁆) i = ⁅x, ({ toFun := single j, map_add' := ⋯ } m) i⁆

Tactic:
AddHom.coe_mk

Goal state after:
case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ (single j ⁅x, m⁆) i = ⁅x, (single j m) i⁆
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
obtain ⟨x, hx⟩ := exists_isRegular_of_finrank_le_card K L h

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ ∃ x, (engel K x).IsCartanSubalgebra
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
⊢ Function.Injective ⇑(inl ψ)

Tactic:
by intro; simp [inl]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
hn : 2 ≤ [].length
⊢ [].formPerm.IsCycle

Tactic:
norm_num at hn

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
hl : [x].Nodup
hn : 2 ≤ [x].length
⊢ [x].formPerm.IsCycle

Tactic:
norm_num at hn

Goal state after:
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
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
x : V
hx : x ∈ U
⊢ ⁅⁅z, a⁆, x⁆ = ⁅z, ⁅a, x⁆⁆ - ⁅a, ⁅z, x⁆⁆

Tactic:
simp only [leibniz_lie z a, add_sub_cancel_right]

Goal state after: