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

Goal state before:
pp: case h.left
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ ⇑(Hom.coweightMap 1) = _root_.id

Tactic:
Hom.coweightMap_one,

Goal state after:
case h.left
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ ⇑LinearMap.id = _root_.id
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case h.right
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ ⇑(Hom.coweightMap 1) = _root_.id

Tactic:
Hom.coweightMap_one,

Goal state after:
case h.right
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ ⇑LinearMap.id = _root_.id
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
i : ι
⊢ P.root i ∈ span ℤ (⇑P.root '' ↑b.support)

Tactic:
by
  have := b.root_mem_or_neg_mem i
  simp only [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid] at this
  rw [← span_span_of_tower (R := ℕ)]
  rcases this with hi | hi
  · exact subset_span hi
  · rw [← neg_mem_iff]
    exact subset_span hi

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
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
this : ∑ j, f' j • P.root ↑j = ∑ j ∈ b.support, f j • P.root j
⊢ ∑ j, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)

Tactic:
rwa [this]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
B : P.InvariantForm
len_eq : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)}

Tactic:
by
  replace len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i := by
    simp only [← (FaithfulSMul.algebraMap_injective ℤ R).eq_iff, algebraMap_pairingIn]
    exact mul_right_cancel₀ (B.ne_zero j) (len_eq ▸ B.pairing_mul_eq_pairing_mul_swap j i)
  have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
  aesop

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.pairingIn ℤ i j = 0
⊢ 0 * P.pairingIn ℤ j i = 0

Tactic:
zero_mul

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
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.pairingIn ℤ i j = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
k : ι
hk : P.root k = P.root j - P.root i
⊢ chainTopCoeff i k = chainTopCoeff i j + 1

Tactic:
let := P.indexNeg
  replace hk : P.root k = P.root j + P.root (-i) := by simpa [sub_eq_add_neg] using hk
  simpa using chainBotCoeff_of_add (by simpa) hk

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
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
contra : P.root j = -P.root i
this : InvolutiveNeg ι := P.indexNeg
⊢ False

Tactic:
replace contra : i = -j := by rw [eq_comm, neg_eq_iff_eq_neg]; simpa using contra

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✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
this : InvolutiveNeg ι := P.indexNeg
contra : i = -j
⊢ False
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.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : abv (↑f j) < ε / 2
H₂ : abv (↑g j) < ε / 2
⊢ abv (↑(f + g) j) < ε

Tactic:
simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)

Goal state after:
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
x y : β
⊢ x - y = 0 ↔ x = y

Tactic:
sub_eq_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ x = y ↔ x = y
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr.h.h
x c : ℝ
a b : CauSeq ℚ abs
h✝ : mk a < mk b
⊢ mk a + c < mk b + c

Tactic:
| _ b =>

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
⊢ const abs (↑f i) < y✝

Tactic:
refine ⟨_, half_pos K0, i, fun j ij => ?_⟩

Goal state after:
case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
⊢ K / 2 ≤ ↑(y✝ - const abs (↑f i)) j
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
⊢ μ ∉ Set.range d

Tactic:
simpa using fun i ↦ (hμ i)

Goal state after:
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
h : IsUnit A.det
n : ℕ
⊢ A ^ (↑n + 1) = A ^ ↑n * A

Tactic:
simp only [← Nat.cast_succ, pow_succ, zpow_natCast]

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
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ 0 = 0 * A

Tactic:
zero_mul

Goal state after:
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
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
⊢ eval (-r) 1 = (-1) ^ 0 * eval r 1

Tactic:
simp only [eval_one, pow_zero, mul_one]

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:
by
    rw [prodCartan, map_lieSpan]; congr; aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x f - eval x g = 0

Tactic:
sub_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x f = eval x g
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f - eval (v i) g = 0

Tactic:
sub_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f = eval (v i) g
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x - y = 0
⊢ x = y

Tactic:
sub_eq_zero

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x = y
⊢ x = y
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j

Tactic:
exact mt (hvs hi hj) hij.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
rw [← add_sum_erase _ _ hi', eval_basis_self (hvt.mono hst) hi',
        eval_interpolate_at_node _
          (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hi, sdiff_subset⟩)))
          (mem_insert_self _ _),
        mul_one, add_eq_left]

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate s v) r =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

Tactic:
by
  rw [interpolate_eq_sum_interpolate_insert_sdiff _ hvs ⟨i, mem_insert_self i {j}⟩ _,
    sum_insert (notMem_singleton.mpr hij), sum_singleton, basis_pair_left hij,
    basis_pair_right hij, sdiff_insert_insert_of_mem_of_notMem hi (notMem_singleton.mpr hij),
    sdiff_singleton_eq_erase, pair_comm,
    sdiff_insert_insert_of_mem_of_notMem hj (notMem_singleton.mpr hij.symm),
    sdiff_singleton_eq_erase]
  exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ nodal s v ≠ 0

Tactic:
apply ne_zero_of_natDegree_gt (n := 0)

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ 0 < (nodal s v).natDegree
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type u_6
x✝¹ : MvPolynomial α✝ R
x✝ : MvPolynomial β✝ R
⊢ x✝¹ <* x✝ = Function.const β✝ <$> x✝¹ <*> x✝

Tactic:
simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]; simp [rename_eq_aeval]; rfl

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

Goal state before:
pp: case h.inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
x : ↥H
K : ℕ →o Submodule R ↥H := { toFun := fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → K n = K m
y : ↥H
m : ℕ
hm : ((ad R L) ↑x ^ m) ↑y = 0
hmn : n ≤ m
⊢ ((ad R L) ↑x ^ n) ↑y = ↑(0 y)

Tactic:
· have : ∀ k : ℕ, ((ad R L) x ^ k) y = 0 ↔ y ∈ K k := by simp [K, Subtype.ext_iff, coe_ad_pow]
    rwa [this, ← hn m hmn, ← this] at hm

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
⊢ (P * A * b'.toMatrix ⇑b).charpoly = A.charpoly

Tactic:
set Q := b'.toMatrix b

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
⊢ (P * A * Q).charpoly = A.charpoly
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
m n : M
⊢ weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤ weightedHomogeneousSubmodule R w (m + n)

Tactic:
by
  classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ homogeneousHull 𝒜 I = ⨆ i, { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }

Tactic:
ext1
  rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ constantCoeff (M.toMvPolynomial i) = 0

Tactic:
by
  simp only [toMvPolynomial, ← C_mul_X_eq_monomial, map_sum, map_mul, constantCoeff_X,
    mul_zero, Finset.sum_const_zero]

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

Goal state before:
pp: 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
⊢ 0 * eval 0 F = 0

Tactic:
zero_mul

Goal state after:
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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: 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)
⊢ IsCompl V W

Tactic:
rw [hV]

Goal state after:
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)
⊢ IsCompl (⨆ n, ker (φ ^ n)) W
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✝ : Nontrivial R
⊢ (Polynomial.map (↑(bind₁ (toMvPolynomial b (Free.chooseBasis R M).end φ)))
        (charpoly.univ R (Free.ChooseBasisIndex R M))).natDegree =
    finrank R M

Tactic:
(charpoly.univ_monic _ _).natDegree_map,

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✝ : Nontrivial R
⊢ (charpoly.univ R (Free.ChooseBasisIndex R M)).natDegree = finrank R M
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
p : MvPolynomial σ R
⊢ (rename φ) ((homogeneousComponent n) p) = (homogeneousComponent n) ((rename φ) p)

Tactic:
induction p using MvPolynomial.induction_on' with

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' V'₁ : Type v'
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V'₁
inst✝ : Module K V'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ (f ∘ₗ g).rank ≤ min f.rank g.rank

Tactic:
by
  simpa only [Cardinal.lift_id] using lift_rank_comp_le g f

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

Goal state before:
pp: p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ ↑((soIndefiniteEquiv p q R hi) A) = (Pso p q R i)⁻¹ * ↑A * Pso p q R i

Tactic:
rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply]
  simp only [so', skewAdjointMatricesLieSubalgebraEquiv_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_1
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
h : fromBlocks A B C D ∈ symplecticGroup l R
h_final : fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D) (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R
⊢ Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1

Tactic:
obtain ⟨h_eq1, h_eq2, _, h_eq3⟩ := fromBlocks_inj.1 h_final

Goal state after:
case refine_1
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
h : fromBlocks A B C D ∈ symplecticGroup l R
h_final : fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D) (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R
h_eq1 : Cᵀ * A - Aᵀ * C = 0
h_eq2 : Cᵀ * B - Aᵀ * D = -1
left✝ : Dᵀ * A - Bᵀ * C = 1
h_eq3 : Dᵀ * B - Bᵀ * D = 0
⊢ Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
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
⊢ Module.rank R ↥(span R ∅) = 0

Tactic:
span_empty,

Goal state after:
case inl
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : IsEmpty n
⊢ Module.rank R ↥⊥ = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝⁴ : Fintype n
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Fintype m
inst✝ : LinearOrder m
A : Matrix m m R
B : Matrix m n R
hA : A.IsUpperTriangular
hd : ∀ (i : m), A.diag i ≠ 0
⊢ (A * B).rank = B.rank

Tactic:
have hdet : A.det ≠ 0 := by simpa [det_of_isUpperTriangular hA, Finset.prod_ne_zero_iff]
  exact rank_mul_eq_right_of_det_ne_zero A B hdet

Goal state after: