mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x : M × M
⊢ (dualProd R M)
      (((associated Q ∘ₗ LinearMap.fst R M M + associated Q ∘ₗ LinearMap.snd R M M).prod
            (LinearMap.fst R M M - LinearMap.snd R M M)).toFun
        x) =
    (prod Q (-Q)) x

Tactic:
by
    dsimp only [QuadraticMap.associated, QuadraticMap.associatedHom]
    dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe,
      LinearMap.coe_toAddHom, LinearMap.prod_apply, Function.prod_apply, LinearMap.add_apply,
      LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply,
      LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, QuadraticMap.prod_apply]
    simp only [neg_apply, polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat,
      polar_comm _ x.1 x.2, smul_sub, Module.End.smul_def, sub_add_sub_cancel,
      ← sub_eq_add_neg (Q x.1) (Q x.2)]
    rw [← map_sub (⅟2 : Module.End R R), ← mul_sub, ← Module.End.smul_def]
    simp only [Module.End.smul_def, half_moduleEnd_apply_eq_half_smul, smul_eq_mul,
      invOf_mul_cancel_left']

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

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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range = Subgroup.closure (range P.reflection)

Tactic:
refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
  · rintro - ⟨i, rfl⟩
    simp only [MonoidHom.domRestrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image,
      SetLike.mem_coe]
    use Equiv.reflection P i
    exact ⟨reflection_mem_weylGroup P i, Equiv.reflection_weightEquiv P i⟩
  · rintro fg ⟨⟨w, hw⟩, rfl⟩
    induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.weightHom P).domRestrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | inv_mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [Equiv.reflection_inv, MonoidHom.domRestrict_apply, Equiv.weightHom_apply,
        Equiv.reflection_weightEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using! Subgroup.mul_mem _ h₁ h₂

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r✝ : k[G]
m : RestrictScalars k k[G] M
r : k
f : k[G]
⊢ ((ofModule M).asAlgebraHom f) m =
      (RestrictScalars.addEquiv k k[G] M).symm (f • (RestrictScalars.addEquiv k k[G] M) m) →
    ((ofModule M).asAlgebraHom (r • f)) m =
      (RestrictScalars.addEquiv k k[G] M).symm ((r • f) • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
w

Goal state after:
case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r✝ : k[G]
m : RestrictScalars k k[G] M
r : k
f : k[G]
w :
  ((ofModule M).asAlgebraHom f) m = (RestrictScalars.addEquiv k k[G] M).symm (f • (RestrictScalars.addEquiv k k[G] M) m)
⊢ ((ofModule M).asAlgebraHom (r • f)) m =
    (RestrictScalars.addEquiv k k[G] M).symm ((r • f) • (RestrictScalars.addEquiv k k[G] M) m)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
q : Submodule K N
h : ¬q.dualAnnihilator = ⊤ → Submodule.map (↑P.toPerfPair.symm) q.dualAnnihilator = ⊥
stab : ∀ (i : ι), q ∈ invtSubmodule ↑(P.coreflection i)
ne_bot : q.dualAnnihilator ≠ ⊤
⊢ q = ⊤

Tactic:
simpa using h ne_bot

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

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
i : ι
x : M
⊢ (↑(reflection P i)⁻¹).weightMap x = (↑(reflection P i)).weightMap x

Tactic:
simp [← weightEquiv_apply]

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
⊢ P.coxeterWeightIn ℤ i j = 0

Tactic:
by rw [coxeterWeightIn, h, zero_mul]

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

Goal state before:
pp: R₂ : Type u_3
inst✝² : CommRing R₂
n : Type u_5
inst✝¹ : Fintype n
J A : Matrix n n R₂
inst✝ : DecidableEq n
⊢ A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A

Tactic:
by
  simp only [mem_skewAdjointMatricesSubmodule]

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

Goal state before:
pp: case pos
ι : 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
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ↑m < n
⊢ ∑ m' ≤ m, P.root (Fin.snoc f k m') ∈ range ⇑P.root

Tactic:
have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl

Goal state after:
case pos
ι : 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
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ↑m < n
this : m = ⟨↑m, hm⟩.castSucc
⊢ ∑ m' ≤ m, P.root (Fin.snoc f k m') ∈ range ⇑P.root
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: case pos
α : 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:
simp [hf, this.1 hf]

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

Goal state before:
pp: x a : ℝ
⊢ -a + a = 0

Tactic:
apply ext_cauchy; simp [cauchy_add, cauchy_neg, cauchy_zero]

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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
hg₀ : ∀ (i : ι), g (P.coroot i) ≠ 0
hg : ∀ (i : ι), 0 < g (P.coroot i) ↔ 0 < f (P.root i)
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' baseOf ⇑P.root ↑f) ∨
    -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' baseOf ⇑P.root ↑f)

Tactic:
P.baseOf_root_eq_baseOf_coroot f hf₀ g hg₀ (fun i ↦ (hg i).symm)

Goal state after:
ι : 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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
hg₀ : ∀ (i : ι), g (P.coroot i) ≠ 0
hg : ∀ (i : ι), 0 < g (P.coroot i) ↔ 0 < f (P.root i)
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' baseOf ⇑P.coroot ↑g) ∨
    -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' baseOf ⇑P.coroot ↑g)
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
⊢ ∑ i, u i * w i ≤ ∑ i, v i * w i

Tactic:
gcongr <;> apply_rules

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

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
⊢ ∑ i, w i * u i ≤ ∑ i, w i * v i

Tactic:
gcongr <;> apply_rules

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

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

Tactic:
exact Setoid.symm (CauSeq.inf_eq_left hc)

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 + 1) = (A ^ n)⁻¹

Tactic:
neg_add_cancel_right,

Goal state after:
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) = (A ^ n)⁻¹
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * A ^ (-↑n - 1)

Tactic:
zpow_sub_one ha,

Goal state after:
case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * (A ^ (-↑n) * A⁻¹)
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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)

Tactic:
cases m

Goal state after:
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)

case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
i : ι
x✝ : i ∈ Finset.univ
h₀ : 0 ≤ ρ - μ
h₁ : μ ≤ ρ - μ
h₂ : 0 ≤ d i
h₃ : (ρ - μ) * |v i| ≤ (N *ᵥ |v|) i
⊢ μ * (d i * |v i| ^ 2) ≤ (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i

Tactic:
calc μ * (d i * |v i| ^ 2)
        = μ * |v i| * (d i * |v i|) := by ring
      _ ≤ (ρ - μ) * |v i| * (d i * |v i|) := by gcongr
      _ ≤ (N *ᵥ |v|) i * (d i * |v i|) := by gcongr
      _ = (N *ᵥ |v|) i * (diagonal d *ᵥ |v|) i := by simp [mulVec_eq_sum, diagonal_apply, mul_comm]
      _ = (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i := by simp [mulVec_eq_sum, vecMul_eq_sum, mul_comm]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0

Tactic:
simp_rw [← Int.emod_add_emod n]

Goal state after:
k : ℕ
n : ℤ
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
⊢ ∀ (k : ι), q ∈ invtSubmodule ↑(P.reflection k)

Tactic:
← b.forall_mem_support_invtSubmodule_iff

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
⊢ ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
⊢ (ascPochhammer S (n + 1)).Monic

Tactic:
have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1

Goal state after:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (ascPochhammer S (n + 1)).Monic
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
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 ∈ s
hs : 1 ≤ #s
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)

Tactic:
have hst' : #s ≤ #t := card_le_card hst

Goal state after:
case refine_1
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 ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
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
H : ∑ j ∈ s, eval (v i) (Lagrange.basis s v j) = 1
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i

Tactic:
rw [← mul_one (r i), ← H, mul_sum]

Goal state after:
case neg
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
H : ∑ j ∈ s, eval (v i) (Lagrange.basis s v j) = 1
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) =
    ∑ i_1 ∈ s, r i * eval (v i) (Lagrange.basis s v i_1)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ ⟨x, ⋯⟩ ∈ derivedSeries R (↥DI) 1

Tactic:
rwa [derivedSeries_eq_derivedSeriesOfIdeal_comap, mem_comap]

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

Goal state before:
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 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : ¬j = 0
⊢ ↑(((decompose 𝒜) x) j) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)

Tactic:
· exact AddSubmonoid.mem_iSup_of_mem j <| AddSubmonoid.mem_iSup_of_mem (pos_of_ne_zero hj₀) <|
      Subtype.prop _

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
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
h : ((toMatrix (chooseBasis K M) (chooseBasis K M)) φ).charpoly.coeff 0 = 0
⊢ (-1) ^ Fintype.card (ChooseBasisIndex K M) * ((toMatrix (chooseBasis K M) (chooseBasis K M)) φ).charpoly.coeff 0 = 0

Tactic:
rw [h, mul_zero]

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
ιM : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup L
inst✝¹⁰ : Module R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
φ : L →ₗ[R] End R M
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ιM
inst✝⁵ : DecidableEq ι
inst✝⁴ : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module.Finite A (A ⊗[R] M)
inst✝ : Free A (A ⊗[R] M)
x : ι → A
⊢ Polynomial.map (aeval x).toRingHom (φ.polyCharpolyAux b bₘ) =
    ((tensorProduct R A M M ∘ₗ baseChange A φ) ((basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly

Tactic:
rw [← polyCharpolyAux_map_eval (tensorProduct R A M M ∘ₗ baseChange A φ) _ (basis A bₘ),
    polyCharpolyAux_baseChange, Polynomial.map_map]
  congr
  exact DFunLike.ext _ _ fun f ↦ (MvPolynomial.eval_map (algebraMap R A) x f).symm

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
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
hf : Function.Injective f
_h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
  Finite.of_basis (basis (MvPolynomial ι R) bₘ)
_h2 : Free (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) := Free.of_basis (basis (MvPolynomial ι R) bₘ)
⊢ f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')

Tactic:
simp only [f, polyCharpolyAux_map_aeval, polyCharpolyAux_map_aeval]

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
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpoly (basis A b) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)

Tactic:
unfold polyCharpoly
  rw [← φ.polyCharpolyAux_baseChange]
  apply polyCharpolyAux_basisIndep

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
x : L
⊢ Polynomial.map (eval ⇑(b.repr x)) (φ.polyCharpoly b) = charpoly (φ x)

Tactic:
by
  rw [polyCharpoly, polyCharpolyAux_map_eq_charpoly]

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
this : Polynomial.map (evalRingHom 1) χ = X ^ r
⊢ Ex ≤ Ey

Tactic:
χ,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
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
this : Polynomial.map (evalRingHom 1) (lieCharpoly K (↥E) x' u) = X ^ r
⊢ Ex ≤ Ey