mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∀ b ∈ φ.support, (b.sum fun x e ↦ e) ≤ n

Tactic:
intro d hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun x e ↦ e) ≤ n
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]
    · rw [coeff_zero]
    · rw [hp zero_coeff]; exact Ne.symm hn

Goal state after:
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 : σ → τ
h : φ.IsHomogeneous n
⊢ ∀ d ∈ φ.support, degree (mapDomain f d) = n

Tactic:
intro d hd

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ degree (mapDomain f d) = n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
⊢ (((finSuccEquiv R N) φ).coeff i).IsHomogeneous j

Tactic:
intro d hd

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) φ).coeff i) ≠ 0
⊢ (weight 1) d = j
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case pos
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 →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∈ d.support
this : ∀ i ∈ d.support, d i = 0
⊢ d i = 0

Tactic:
exact this i hi

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : (φ ^ n) x = 0
⊢ ↑((restrict φ hφV ^ n) ⟨x, ⋯⟩) = 0

Tactic:
refine .trans ?_ hx

Goal state after:
case h
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : (φ ^ n) x = 0
⊢ ↑((restrict φ hφV ^ n) ⟨x, ⋯⟩) = (φ ^ n) x
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if degree d = n then coeff d φ else 0

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if (weight fun x ↦ 1) d = n then coeff d φ else 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ (homogeneousComponent n) φ = ∑ d ∈ φ.support with degree d = n, (monomial d) (coeff d φ)

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ (homogeneousComponent n) φ = ∑ x ∈ φ.support with (weight fun x ↦ 1) x = n, (monomial x) (coeff x φ)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, degree d ≠ n
⊢ (homogeneousComponent n) φ = 0

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight fun x ↦ 1) d ≠ n
⊢ (homogeneousComponent n) φ = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e ↦ e) < n
⊢ ∀ d ∈ φ.support, degree d ≠ n

Tactic:
intro d hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e ↦ e) < n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ degree d ≠ n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ ((homogeneousComponent n) p).support = {c ∈ p.support | degree c = n}

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial σ R
⊢ ((homogeneousComponent n) p).support = {c ∈ p.support | (weight fun x ↦ 1) c = n}
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ ↦
    (DirectSum.mk (fun i ↦ ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑degree) φ.support)) fun m ↦
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩

Tactic:
degree_eq_weight_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ ↦
    (DirectSum.mk (fun i ↦ ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑(weight fun x ↦ 1)) φ.support)) fun m ↦
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩
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
⊢ -fromBlocks 1 0 0 1 = -1

Tactic:
← fromBlocks_one

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ -fromBlocks 1 0 0 1 = -fromBlocks 1 0 0 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))
⊢ (A.submatrix r ⇑(Equiv.refl n)).rank ≤ A.rank

Tactic:
rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
    show LinearMap.funLeft R R (Equiv.refl n).symm = LinearEquiv.funCongrLeft R R
      (Equiv.refl n).symm from rfl, LinearEquiv.range, Submodule.map_top]

Goal state after:
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
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
have hM : V * M * U = diagonal (fun i ↦ if i ∈ s then 1 else 0) := by
    rw [V_def, U_def, hM0, mul_assoc, mul_assoc _ (L'.map _).prod, prod_mul_reverse_inv_prod,
      mul_one, ← mul_assoc, mul_assoc _ (L.reverse.map _).prod, reverse_inv_prod_mul_prod, mul_one]
    ext
    simp only [E_def, mul_diagonal, diagonal_apply, ite_mul, one_mul, zero_mul, s_def,
      Finset.mem_filter, Finset.mem_univ, true_and, ite_not]
    split_ifs with h1 h2 <;> first | rw [← h1, h2] | rw [← h1, inv_mul_cancel₀ h2] | rfl

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0

Tactic:
← hn

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z)
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)
⊢ a ∈ twoCocycle R L M → ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆

Tactic:
intro h x y z

Goal state after:
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 : a ∈ twoCocycle R L M
x y z : L
⊢ (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
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)
x y z : ⨁ (i : ι), L i
⊢ zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ (x + y) z =
    zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ x z + zipWith (fun x x_1 y ↦ ⁅x_1, y⁆) ⋯ y z

Tactic:
by
      ext
      simp only [zipWith_apply, add_apply, add_lie]

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

Goal state before:
pp: case inr
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
⊢ χ ⁅z, a⁆ = 0

Tactic:
let U' : ℕ →o Submodule R V :=
  { toFun n := Submodule.span R {((π z)^i) v | i < n},
    monotone' i j h := Submodule.span_mono (fun _ ⟨c, hc, hw⟩ ↦ ⟨c, lt_of_lt_of_le hc h, hw⟩) }

Goal state after:
case inr
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' := ⋯ }
⊢ χ ⁅z, a⁆ = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case of
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ))
      ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N))
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm
      ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩))

Tactic:
have : (rTensor N (lof R ι (fun i ↦ ℳ i) i)) y =
        (directSumLeft R R (fun i ↦ ℳ i) N).symm ((of (fun i ↦ ℳ i ⊗[R] N) i) y) :=
      (TensorProduct.directSumLeft_symm_of R R (M₁ := fun i ↦ ℳ i) y).symm

Goal state after:
case of
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
y : ↥(ℳ i) ⊗[R] N
this :
  (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) y)
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ))
      ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N))
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩)) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm
      ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm
        ((of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) ⟨(rTensor N (ℳ i).subtype) y, ⋯⟩))
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case pos.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left✝ : 0 < (f.cycleOf x).support.card
hy : (f ^ 0) x = y
⊢ f.toList x ~r f.toList y

Tactic:
simp only [coe_one, id, pow_zero] at hy
      -- Porting note: added `IsRotated.refl`
      simp [hy, IsRotated.refl]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ ((F (r • x)).sum fun a v ↦ a • (Φ ((F f) (-a))) v) = (RingHom.id R) r • (F x).sum fun a v ↦ a • (Φ ((F f) (-a))) v

Tactic:
rw [map_smul, sum_of_support_subset _ support_smul _ (by simp), sum, Finset.smul_sum]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ ∑ x_1 ∈ (F x).support, x_1 • (Φ ((F f) (-x_1))) ((r • F x) x_1) =
    ∑ x_1 ∈ (F x).support, (RingHom.id R) r • x_1 • (Φ ((F f) (-x_1))) ((F x) x_1)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
⊢ (if f x = x then if f y = y then s else ↑(f.toList y) else ↑(f.toList x)) =
    if f y = y then if f x = x then s else ↑(f.toList x) else ↑(f.toList y)

Tactic:
split_ifs with hx hy hy <;> try rfl

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : ¬f y = y
⊢ ↑(f.toList x) = ↑(f.toList y)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
s : Cycle α
hn : s.Nodup
hs : (↑⟨s, hn⟩).formPerm ⋯ = f
hs' : ∀ (y : { s // s.Nodup }), (fun s ↦ (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩
t : Cycle α
ht : t.Nodup
ht' : t.Nontrivial
ht'' : (↑⟨t, ⋯⟩).formPerm ⋯ = f
⊢ ⟨t, ⋯⟩ = ⟨s, ⋯⟩

Tactic:
simpa using hs' ⟨t, ht⟩ ht''

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

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
let e : (k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z <| by aesop).symm

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case h.refine_1.refine_1
n p : ℕ
i : Fin n
α : Fin p → Fin n
k : Fin n
hik : i < k
hk : k ∉ Set.range α
t : Fin (p + 1) := ⨅ j ∈ {j | k < α j}, j.castSucc
t_eq : t = ⨅ j ∈ {j | k < α j}, j.castSucc
hα : (∀ (j : Fin p), i < α j) ∧ StrictMono α
j : Fin p
x : Fin (p + 1)
hjx : j.castSucc < x
h : ∀ (i : Fin p), k < α i → x ≤ i.castSucc
⊢ α j < k

Tactic:
contrapose! h
      have k_ne (j : Fin p) : k ≠ α j := fun hj ↦ hk ⟨j, hj.symm⟩
      exact ⟨j, h.lt_of_ne (k_ne _), hjx⟩

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)

Tactic:
rw [← Subtype.mk.injEq u hu v hv, ← E.basis.repr.injective.eq_iff]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ ↔ Set.EqOn u v ↑(range E.order)
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case a
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
⊢ ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯ ≤ LieSubmodule.restr I H

Tactic:
exact iSup₂_le fun α hα ↦ by
      rw [sl2SubmoduleOfRoot_eq_sup]
      refine sup_le (sup_le ?_ ?_) ?_
      · exact hα
      · apply I.rootSpace_le_of_apply_coroot_ne_zero hα
        simp [Pi.neg_apply, root_apply_coroot (H.isNonZero_coe_root α)]
      · exact I.corootSubmodule_le hα

Goal state after: