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

Goal state before:
pp: case inr.inr
ι : 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
inst✝ : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
h₂ : P.root i ≠ -P.root j
aux₁ :
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}

Tactic:
have aux₂ : P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4 := P.coxeterWeightIn_ne_four ℤ h₁ h₂

Goal state after:
case inr.inr
ι : 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
inst✝ : P.IsReduced
this : Module.IsReflexive R M
h₁ : i ≠ j
h₂ : P.root i ≠ -P.root j
aux₁ :
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
aux₂ : P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
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 : ι
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
h : s • P.root i = P.root i - P.root j
⊢ (s - 1) • P.root i + 1 • P.root j = 0

Tactic:
simp [sub_smul, h]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inr.inr
ι : 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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
neg : f < 0
⊢ False

Tactic:
· simpa [hij, f] using le_of_lt neg i

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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : Finite ι
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
⊢ P.pairingIn ℤ i j ≤ 0

Tactic:
by_contra! h

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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : Finite ι
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
h : 0 < P.pairingIn ℤ i j
⊢ False
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]
⊢ ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) = P.pairingIn ℤ j i

Tactic:
by
  suffices ∀ i j, LinearIndependent R ![P.root i, P.root j] →
      P.chainBotCoeff i j - P.chainTopCoeff i j ≤ P.pairingIn ℤ j i by
    refine le_antisymm (this i j h) ?_
    specialize this (P.reflectionPerm i i) j (by simpa)
    simp only [chainBotCoeff_reflectionPerm_left, chainTopCoeff_reflectionPerm_left,
      pairingIn_reflectionPerm_self_right] at this
    lia
  intro i j h
  have h₁ : P.reflection i (P.root <| P.chainBotIdx i j) =
      P.root j + (P.chainBotCoeff i j - P.pairingIn ℤ j i) • P.root i := by
    simp [reflection_apply_root, ← P.algebraMap_pairingIn ℤ]
    module
  have h₂ : P.reflection i (P.root <| P.chainBotIdx i j) ∈ range P.root := by
    rw [← root_reflectionPerm]
    exact mem_range_self _
  rw [h₁, root_add_zsmul_mem_range_iff h, mem_Icc] at h₂
  grind

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
huv : P.root i = u • P.root j + v • P.root k
l : ι
hl : 0 < g (P.coroot l)
⊢ ∃ c, ∑ x, c x • ↑x = P.root l

Tactic:
rwa [← Submodule.mem_span_iff_of_fintype, ← mem_toAddSubmonoid, span_nat_eq_addSubmonoidClosure,
      AddSubmonoid.closure_image_isAddIndecomposable_baseOf,
      AddSubmonoid.mem_closure_image_pos_iff P.root f _ (P.ne_zero _), hfg]

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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ (∑ x ∈ b.support, P.toLinearMap (f x • P.root x)) (P.coroot i) =
    ∑ x ∈ b.support, (algebraMap ℤ R) (f x • P.pairingIn ℤ x i)

Tactic:
map_zsmul,

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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ (∑ x ∈ b.support, f x • P.toLinearMap (P.root x)) (P.coroot i) =
    ∑ x ∈ b.support, f x • (algebraMap ℤ R) (P.pairingIn ℤ x i)
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
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + ↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (↑w + 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ P.root i + ↑w • P.root j ∈ range ⇑P.root

Tactic:
by
      replace hk : P.root i + (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
      simp only [natCast_zsmul, root_add_nsmul_mem_range_iff_le_chainTopCoeff hij] at hk ⊢
      lia

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✝
β : Type u_3
inst✝¹ : CommRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
a b : CauSeq β abv
n : ℕ
⊢ ↑(a * b) n = ↑(b * a) n

Tactic:
simp [mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a < b ⊓ c

Tactic:
by
  obtain ⟨⟨εb, εb0, ib, hb⟩, ⟨εc, εc0, ic, hc⟩⟩ := hb, hc
  refine ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => ?_⟩
  have := min_le_min (hb _ (sup_le_iff.mp hi).1) (hc _ (sup_le_iff.mp hi).2)
  exact this.trans_eq (min_sub_sub_right _ _ _)

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

Goal state before:
pp: case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk ((y✝² ⊔ y✝¹) ⊓ (y✝² ⊔ y✝)) = mk (y✝² ⊔ y✝¹ ⊓ y✝)

Tactic:
exact congr_arg mk (CauSeq.sup_inf_distrib_left ..).symm

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

Goal state before:
pp: f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ -x ≤ -mk f

Tactic:
← mk_neg

Goal state after:
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) -
      (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero

Tactic:
exact sub_limZero
                (by rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _)
                (by rw [← mul_assoc]; exact h₁ _ _ _)

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

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

Tactic:
← ih,

Goal state after:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ (n + 1) = A⁻¹ * A⁻¹ ^ n
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : NonUnitalSemiring R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x : m → R
A B : Matrix m n R
x' : n → R
⊢ x ⬝ᵥ A ⊙ B *ᵥ x' = (diagonal x).vec ⬝ᵥ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B *ᵥ (diagonal x').vec

Tactic:
by
  simp [diagonal, mulVec, dotProduct, Fintype.sum_prod_type]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : A⁻¹.IsHermitian
⊢ A⁻¹⁻¹.IsHermitian

Tactic:
exact IsHermitian.inv h

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

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ (A ^ k)ᴴ = A ^ k

Tactic:
conjTranspose_zpow,

Goal state after:
α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ Aᴴ ^ k = A ^ k
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
⊢ HasEigenvalue ((toLin b b) (diagonal d)) μ ↔ ∃ i, d i = μ

Tactic:
have (i : n) : HasEigenvalue (toLin b b (diagonal d)) (d i) :=
    hasEigenvalue_of_hasEigenvector <| hasEigenvector_toLin_diagonal d i b

Goal state after:
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)
⊢ HasEigenvalue ((toLin b b) (diagonal d)) μ ↔ ∃ i, d i = μ
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
hf : f ≠ 0
⊢ f = g

Tactic:
· exact eq_of_degree_sub_lt_of_eval_finset_eq s
      (lt_of_lt_of_le (degree_sub_lt_left h_deg_eq hf hlc) h_deg_le) h_eval

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ((interpolate s v) r).degree ≤ ↑(#s - 1)

Tactic:
by
  refine (degree_sum_le _ _).trans ?_
  rw [Finset.sup_le_iff]
  intro i hi
  rw [degree_mul, degree_basis hvs hi]
  by_cases hr : r i = 0
  · simpa only [hr, map_zero, degree_zero, WithBot.bot_add] using bot_le
  · rw [degree_C hr, zero_add]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
r : R
⊢ (bind₂ f) ((monomial d) r) = f r * (monomial d) 1

Tactic:
simp only [monomial_eq, map_mul, bind₂_C_right, Finsupp.prod, map_prod,
    map_pow, bind₂_X_right, C_1, one_mul]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars ⊆ φ.vars.biUnion fun i ↦ (f i).vars

Tactic:
calc (bind₁ f φ).vars
    _ = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
      rw [← map_sum, ← φ.as_sum]
    _ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars :=
      (vars_sum_subset _ _)
    _ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) := by
      simp only [bind₁_monomial]
    _ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) := ?_
    -- proof below
    _ ≤ φ.vars.biUnion fun i : σ => vars (f i) := ?_

Goal state after:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d ↦ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ⊆
    φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars

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
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
t : R
⊢ ((scalar (ChooseBasisIndex R M)) t - (toMatrix (chooseBasis R M) (chooseBasis R M)) f).det =
    ((toMatrix (chooseBasis R M) (chooseBasis R M)) ((algebraMap R (M →ₗ[R] M)) t) -
        (toMatrix (chooseBasis R M) (chooseBasis R M)) f).det

Tactic:
scalar_apply,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
t : R
⊢ ((diagonal fun x ↦ t) - (toMatrix (chooseBasis R M) (chooseBasis R M)) f).det =
    ((toMatrix (chooseBasis R M) (chooseBasis R M)) ((algebraMap R (M →ₗ[R] M)) t) -
        (toMatrix (chooseBasis R M) (chooseBasis R M)) f).det
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
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
r : K[X]
hr : (aeval ((ad K (End K M)) s)) r = (ad K (End K M)) y
⊢ (ad K (End K M)) s ∈ K[(ad K (End K M)) (φ x)]

Tactic:
simpa only [← hX_ns] using! ad_mem_adjoin_of_isSemisimple hns hn_nil hs_ss

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
⊢ (minpoly R f).coeff 0 ≠ 0

Tactic:
by
  intro h
  obtain ⟨P, hP⟩ := X_dvd_iff.2 h
  have hdegP : P.degree < (minpoly R f).degree := by
    rw [hP, mul_comm]
    refine degree_lt_degree_mul_X fun h => ?_
    rw [h, mul_zero] at hP
    exact minpoly.ne_zero (isIntegral f) hP
  have hPmonic : P.Monic := by
    suffices (minpoly R f).Monic by
      rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
    exact minpoly.monic (isIntegral f)
  have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
  simp only [hP, Module.End.mul_eq_comp, LinearMap.ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp,
    map_mul, zero_apply, Function.comp_apply] at hzero
  exact not_le.2 hdegP (minpoly.min _ _ hPmonic (LinearMap.ext hzero))

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

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

Tactic:
rw [degree_eq_weight_one] at hd
  exact IsWeightedHomogeneous.coeff_eq_zero hφ d hd

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ m * n = ∑ _i ∈ Finset.range n, m

Tactic:
simp [mul_comm]

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
m : M
⊢ ↑(((DirectSum.mk (fun i ↦ ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m ↦
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

Tactic:
by_cases hm : m ∈ Finset.image (weight w) φ.support

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∈ Finset.image (⇑(weight w)) φ.support
⊢ ↑(((DirectSum.mk (fun i ↦ ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m ↦
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weight w)) φ.support
⊢ ↑(((DirectSum.mk (fun i ↦ ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weight w)) φ.support)) fun m ↦
          ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ = 0
⊢ (eval r) (((finSuccEquiv R N) F).coeff i) = 0

Tactic:
← coeff_eval_eq_eval_coeff,

Goal state after:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ = 0
⊢ (Polynomial.map (eval r) ((finSuccEquiv R N) F)).coeff i = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hnR : ↑n ≤ #R
h : F ≠ 0
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
obtain ⟨k, f, hf, F, rfl⟩ := exists_fin_rename F

Goal state after:
R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hnR : ↑n ≤ #R
k : ℕ
f : Fin k → σ
hf : Function.Injective f
F : MvPolynomial (Fin k) R
hF : ((rename f) F).IsHomogeneous n
h : (rename f) F ≠ 0
⊢ ∃ r, (eval r) ((rename f) F) ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

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

Tactic:
rw [LinearMap.range_comp]

Goal state after:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V'
inst✝² : Module K V'
inst✝¹ : AddCommMonoid V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ Submodule.map f g.range ≤ f.range