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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
⊢ mk (if h : f.LimZero then 0 else f.inv h) = mk (if h : g.LimZero then 0 else g.inv h)

Tactic:
· have hg := mt this.2 hf
        simp only [hf, dite_false, hg]
        have If : mk (inv f hf) * mk f = 1 := mk_eq.2 (inv_mul_cancel hf)
        have Ig : mk (inv g hg) * mk g = 1 := mk_eq.2 (inv_mul_cancel hg)
        have Ig' : mk g * mk (inv g hg) = 1 := mk_eq.2 (mul_inv_cancel hg)
        rw [mk_eq.2 fg, ← Ig] at If
        rw [← mul_one (mk (inv f hf)), ← Ig', ← mul_assoc, If, mul_assoc, Ig', mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
⊢ a ⊔ b ≈ b

Tactic:
intro _ _
    refine ⟨i, fun j hj => ?_⟩
    dsimp
    rw [← max_sub_sub_right]
    rwa [sub_self, max_eq_right, abs_zero]
    rw [sub_nonpos, ← sub_nonneg]
    exact ε0.le.trans (h _ hj)

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

Goal state before:
pp: x : ℝ
⊢ ∀ (a : ℝ), a ≠ 0 → a * a⁻¹ = 1

Tactic:
rintro ⟨a⟩ h
    rw [mul_comm]
    simp only [← ofCauchy_inv, ← ofCauchy_mul, ← ofCauchy_one, ← ofCauchy_zero,
      Ne, ofCauchy.injEq] at *
    exact CauSeq.Completion.inv_mul_cancel h

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

Tactic:
obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))

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
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero R
i : m
j : n
r : R
⊢ (single i j r).vec = Pi.single (j, i) r

Tactic:
by
  rw [single_eq_of_single_single, vec_of, Function.uncurry_flip, Pi.uncurry_single_single]
  exact Pi.single_comp_equiv (Equiv.prodComm _ _) _ _

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
e : m → n
he : Function.Injective e
⊢ (M.submatrix e e).PosDef

Tactic:
refine ⟨hM.1.submatrix _, fun x hx ↦ ?_⟩
  simpa [Finsupp.sum_mapDomain_index, add_mul, mul_add] using
    hM.2 <| Finsupp.mapDomain_injective he |>.ne_iff' Finsupp.mapDomain_zero |>.2 hx

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

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
⊢ (↑(inl R L₁ L₂)).range = (↑(snd R L₁ L₂)).ker

Tactic:
exact LinearMap.range_inl R L₁ L₂

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| descPochhammer ℤ (n + 1) * (X - 1 - (↑n).comp (X - 1))

Tactic:
natCast_comp

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| descPochhammer ℤ (n + 1) * (X - 1 - ↑n)
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
i j : ι
h : i ≠ j
⊢ ∃ x ∈ p, (f (Sum.inr ⟨(i, j), h⟩)) x ≠ 0

Tactic:
obtain ⟨k, hk, hk'⟩ : ∃ k ∈ b.support, P.pairingIn ℤ i k ≠ P.pairingIn ℤ j k := by
      contrapose! h
      apply b.injective_pairingIn
      aesop
    simpa [f, sub_eq_zero] using ⟨fun i ↦ P.pairingIn ℤ i k, subset_span ⟨⟨k, hk⟩, rfl⟩, by simpa⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (X - 1 - (↑n).comp (X - 1)) * (descPochhammer ℤ n).comp (X - 1) = (X - (↑n + 1)) * (descPochhammer ℤ n).comp (X - 1)

Tactic:
natCast_comp

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (X - 1 - ↑n) * (descPochhammer ℤ n).comp (X - 1) = (X - (↑n + 1)) * (descPochhammer ℤ n).comp (X - 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) * ↑b ! = eval (↑(a - (b - 1))) (ascPochhammer K b)

Tactic:
← cast_mul,

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b * b !) = eval (↑(a - (b - 1))) (ascPochhammer K b)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b) * ↑b ! = eval (↑a) (descPochhammer K b)

Tactic:
← cast_mul,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.choose b * b !) = eval (↑a) (descPochhammer K b)
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₂
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

Tactic:
simp only [union_assoc]

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₂
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
    lieSpan R (↥(prod eι b₁ b₂)) (range (prodH eι b₁ b₂) ∪ (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
⊢ _root_.IsNilpotent (φ x)

Tactic:
obtain ⟨n, hn_adj, s, hns, hn_nil, hs_ss, hX_ns⟩ := (φ x).exists_isNilpotent_isSemisimple

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hns : s ∈ K[φ x]
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
⊢ _root_.IsNilpotent (φ x)
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
hn : ((ad R L) x ^ n) z = 0
ij : ℕ × ℕ
hij : ij ∈ Finset.antidiagonal (m + n)
⊢ m ≤ ij.1 ∨ n ≤ ij.2

Tactic:
rw [Finset.mem_antidiagonal] at hij; lia

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₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
f : ↥H₁ × ↥H₂ →ₗ[K] ↥(prodCartan eι b₁ b₂) := { toFun := fun x ↦ ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
x y : ↥H₁ × ↥H₂
h : f x = f y
⊢ x = y

Tactic:
simpa [Prod.ext_iff, f] using h

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 := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
rw [← Submodule.map_le_iff_le_comap]

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
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
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 := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
rw [← Submodule.map_le_iff_le_comap]

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
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
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:
by
    simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]; simp [rename_eq_aeval]; rfl

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

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

pp: case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : ¬i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

Tactic:
· rw [h, hr, decompose_zero, zero_apply, ZeroMemClass.coe_zero]

Goal state after:
case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : ¬i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 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
⊢ [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < ker φ,
      ∃ m, m ≠ 0 ∧ φ m = 0].TFAE

Tactic:
tfae_have 1 ↔ 2 := Module.End.hasEigenvalue_iff_isRoot
  tfae_have 2 → 3 := by
    obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ
    simp only [IsRoot.def, constantCoeff_apply, coeff_zero_eq_eval_zero, hF, eval_mul]
    intro h; rw [h, zero_mul]
  tfae_have 3 → 4 := by
    rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff,
      constantCoeff_apply, charpoly]
    intro h; rw [h, mul_zero]
  tfae_have 4 → 5 := bot_lt_ker_of_det_eq_zero
  tfae_have 5 → 6 := by
    contrapose!
    simp only [not_bot_lt_iff, eq_bot_iff]
    intro h x
    simp only [mem_ker, Submodule.mem_bot]
    contrapose!
    apply h
  tfae_have 6 → 1
  | ⟨x, h1, h2⟩ => by
    apply Module.End.hasEigenvalue_of_hasEigenvector ⟨_, h1⟩
    simpa only [Module.End.eigenspace_zero, mem_ker] using h2
  tfae_finish

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
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weight w)) φ.support
⊢ (weightedHomogeneousComponent w i) φ = 0

Tactic:
by
  apply weightedHomogeneousComponent_eq_zero'
  simp only [Finset.mem_image, mem_support_iff, ne_eq, not_exists, not_and] at hi
  exact fun m hm ↦ hi m (mem_support_iff.mp hm)

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

Tactic:
charpoly.univ_natDegree,

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
⊢ Fintype.card (Free.ChooseBasisIndex R M) = finrank R M
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)
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
⊢ F.charpoly.natTrailingDegree = finrank K ↥V

Tactic:
apply ((charpoly_nilpotent_tfae F).out 2 3).mp

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 := ⋯
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⋯
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := ⋯
G : ↥W →ₗ[K] ↥W := ⋯
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := ⋯
e : (↥V × ↥W) ≃ₗ[K] M := ⋯
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := ⋯
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := ⋯
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := ⋯
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
⊢ ∀ (m : ↥V), ∃ n, (F ^ n) m = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
⊢ (rename φ) ((homogeneousComponent n) ((monomial d) c)) = (homogeneousComponent n) ((rename φ) ((monomial d) c))

Tactic:
rename_monomial,

Goal state after:
case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
τ : Type u_5
φ : σ → τ
n : ℕ
d : σ →₀ ℕ
c : R
⊢ (rename φ) ((homogeneousComponent n) ((monomial d) c)) = (homogeneousComponent n) ((monomial (mapDomain φ d)) c)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ : ∀ (r : ChooseBasisIndex R L → R), (eval r) ((polyCharpoly (?m.208 r) b).coeff φ.nilRank) = 0
⊢ False

Tactic:
apply polyCharpoly_coeff_nilRank_ne_zero φ b

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := ⋯
bₘ : Basis (ChooseBasisIndex R M) R M := ⋯
n : ℕ := ⋯
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ : ∀ (r : ChooseBasisIndex R L → R), (eval r) ((polyCharpoly (?m.208 r) b).coeff φ.nilRank) = 0
⊢ (φ.polyCharpoly b).coeff φ.nilRank = 0
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
⊢ c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s

Tactic:
have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg

Goal state after:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
⊢ c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s
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✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ (A * B).rank = B.rank

Tactic:
by
  rw [rank, rank, mulVecLin_mul, LinearMap.range_comp,
    ← (Submodule.equivMapOfInjective A.mulVecLin
      (mulVec_injective_of_det_mem_nonZeroDivisors hA) _).finrank_eq]

Goal state after:
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
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, r ≤ s.card ∧ ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0

Tactic:
let t := (constantCoeff ψ).roots.toFinset
    -- We show that `t` has cardinality at most `finrank K L - r`.
    have ht : t.card ≤ finrank K L - r := by
      refine (Multiset.toFinset_card_le _).trans ?_
      refine (card_roots' _).trans ?_
      rw [constantCoeff_apply]
      -- Indeed, `constantCoeff ψ` has degree at most `finrank K Q = finrank K L - r`.
      apply lieCharpoly_coeff_natDegree
      suffices finrank K Q + r = finrank K L by rw [← this, zero_add, Nat.add_sub_cancel]
      apply Submodule.finrank_quotient_add_finrank
    -- Hence there exists a subset of size `≥ r` in the complement of `t`,
    -- and `constantCoeff ψ` takes non-zero values on all of this subset.
    obtain ⟨s, hs⟩ := exists_finset_le_card K _ hLK
    use s \ t
    refine ⟨?_, ?_⟩
    · refine le_trans ?_ (Finset.le_card_sdiff _ _)
      omega
    · intro α hα
      simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] at hα
      exact hα.2 hψ

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
a : ↥(twoCochain R L M)
x y : L
x✝¹ : R
x✝ : L
⊢ ⁅x, (a y) (x✝¹ • x✝)⁆ - ⁅y, (a x) (x✝¹ • x✝)⁆ + ⁅x✝¹ • x✝, (a x) y⁆ - (a ⁅x, y⁆) (x✝¹ • x✝) + (a ⁅x, x✝¹ • x✝⁆) y -
      (a ⁅y, x✝¹ • x✝⁆) x =
    (RingHom.id R) x✝¹ • (⁅x, (a y) x✝⁆ - ⁅y, (a x) x✝⁆ + ⁅x✝, (a x) y⁆ - (a ⁅x, y⁆) x✝ + (a ⁅x, x✝⁆) y - (a ⁅y, x✝⁆) x)

Tactic:
by simp; abel_nf; simp

Goal state after: