mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
⊢ ↑q = span K (⇑P.root '' {i | P.root i ∈ ↑q})

Tactic:
by
  set Q := (q : Submodule K M)
  have hSQ : span K (P.root '' {i | P.root i ∈ Q}) ≤ Q :=
    span_le.mpr (Set.image_subset_iff.mpr fun _ h => h)
  refine le_antisymm ?_ hSQ
  set S := span K (P.root '' {i | P.root i ∈ Q})
  set T := span K (P.root '' {i | P.root i ∉ Q})
  have h_sup : S ⊔ T = ⊤ := by
    rw [← Submodule.span_union, ← Set.image_union]
    have : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = Set.univ := by ext; simp [em]
    rw [this, Set.image_univ]
    simp
  intro v hv
  obtain ⟨s, hs, t, ht, rfl⟩ := Submodule.mem_sup.mp (h_sup ▸ Submodule.mem_top (x := v))
  suffices t = 0 by rw [this, add_zero]; exact hs
  have htQ : t ∈ Q := by simpa using Q.sub_mem hv (hSQ hs)
  have h_ker : ∀ k, P.coroot' k t = 0 := by
    intro k
    by_cases hk : P.root k ∈ Q
    · refine LinearMap.mem_ker.mp (span_le.mpr ?_ ht)
      rintro _ ⟨j, hj, rfl⟩
      rw [SetLike.mem_coe, LinearMap.mem_ker, P.root_coroot'_eq_pairing, P.pairing_eq_zero_iff',
        ← P.root_coroot'_eq_pairing]
      exact LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hj hk)
    · exact LinearMap.mem_ker.mp (invtRootSubmodule.le_ker_coroot' q hk htQ)
  exact P.eq_zero_iff_forall_coroot'_eq_zero.mpr h_ker

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

Goal state before:
pp: case hr
ι : 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₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝ : ι₂
⊢ Q.root x✝ = (RootPairing.map e f g).root x✝

Tactic:
· simp [hf, RootPairing.map, RootPairing.map]

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
g g' : P.Aut
hgg' : ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : ↑(MulOpposite.unop ((coweightHom P) g)) = ↑(MulOpposite.unop ((coweightHom P) g'))
⊢ g = g'

Tactic:
rw [coweightHom_toLinearMap, coweightHom_toLinearMap] at 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
g g' : P.Aut
hgg' : ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ g = g'
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
⊢ (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_pairingIn_mem_set_of_isCrystallographic i j

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)}
⊢ (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.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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : P.coroot j ∈ span ℤ (⇑P.coroot '' ↑b.support)
⊢ ∃ f, P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i

Tactic:
rw [image_eq_range, mem_span_range_iff_exists_fun] at this

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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i, c i • P.coroot ↑i = P.coroot j
⊢ ∃ f, P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i, c i • P.coroot ↑i = P.coroot j
f : ↥b.support → ℤ
hf : ∑ i, f i • P.coroot ↑i = P.coroot j
⊢ P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑i

Tactic:
simp only [Finset.coe_sort_coe] at hf

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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
this : ∃ c, ∑ i, c i • P.coroot ↑i = P.coroot j
f : ↥b.support → ℤ
hf : ∑ i, f i • P.coroot ↑i = P.coroot j
⊢ P.coroot i = ∑ i, (t * ↑(f i)) • P.coroot ↑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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
x✝ : 0 ≤ f ∧ ∃ i, 0 i < f i
contra : f ≤ 0
h : 0 ≤ f
i : ι
hi : 0 i < f i
⊢ False

Tactic:
simp [le_antisymm contra h] at hi

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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
⊢ LinearIndependent (ι := ↑(baseOf (⇑P.root) f)) R (⇑(P.rootSpan ℚ).subtype ∘ v)

Tactic:
have h_card : Nat.card (baseOf P.root f) = finrank R M := by
    let b : Basis (baseOf P.root f) ℚ (P.rootSpan ℚ) := by
      replace this : LinearIndependent ℚ v :=
        .of_comp (P.rootSpan ℚ).subtype <| P.linearIndepOn_root_baseOf' f.toRatLinearMap hf
      exact Basis.mk this (by rw [h_span])
    rw [← RootPairing.finrank_rootSpanIn ℚ P, finrank_eq_nat_card_basis b]

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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
h_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
⊢ LinearIndependent (ι := ↑(baseOf (⇑P.root) f)) R (⇑(P.rootSpan ℚ).subtype ∘ v)
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
⊢ span ℤ (P.rootSpanMem ℤ '' ↑b.support) = ⊤

Tactic:
by
  refine Submodule.eq_top_iff'.mpr fun ⟨x, hx⟩ ↦ ?_
  rw [← SetLike.mem_coe, ← (injective_subtype (P.rootSpan ℤ)).mem_set_image, ← Submodule.map_coe]
  simpa [Submodule.map_span, ← image_comp]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
by
  rcases Classical.em (LimZero f) with h | h
  · simp [*]
  simp only [false_or, h]
  rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
  rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
  refine (le_total 0 (f i)).imp ?_ ?_ <;>
    refine fun h => ⟨K, K0, i, fun j ij => ?_⟩ <;>
    have := (hi _ ij).1 <;>
    obtain ⟨h₁, h₂⟩ := hi _ le_rfl
  · rwa [abs_of_nonneg] at this
    rw [abs_of_nonneg h] at h₁
    exact
      (le_add_iff_nonneg_right _).1
        (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)
  · rwa [abs_of_nonpos] at this
    rw [abs_of_nonpos h] at h₁
    rw [← sub_le_sub_iff_right, zero_sub]
    exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
a : α
h : -f < const a
⊢ (f + const a).Pos

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
a : α
h : -f < const a
⊢ (const a + f).Pos
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (-f + const abv f.lim).LimZero

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (const abv f.lim + -f).LimZero
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
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c

Tactic:
refine le_of_le_of_eq (Or.inr ?_) ha

Goal state after:
case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≈ a
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
⊢ Function.uncurry (flip (Pi.single i (Pi.single j r))) = Pi.single (j, i) r

Tactic:
Function.uncurry_flip,

Goal state after:
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
⊢ Function.uncurry (Pi.single i (Pi.single j r)) ∘ Prod.swap = Pi.single (j, i) r
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : StarModule R α
A : Matrix n n α
h : A.IsHermitian
k : R
hk : IsSelfAdjoint k
⊢ (k • A)ᴴ = k • A

Tactic:
conjTranspose_smul,

Goal state after:
α : Type u_1
n : Type u_4
R : Type u_5
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : StarModule R α
A : Matrix n n α
h : A.IsHermitian
k : R
hk : IsSelfAdjoint k
⊢ star k • Aᴴ = k • A
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : (k • A)ᴴ = k • A
hk : IsSelfAdjoint k
⊢ A.IsHermitian

Tactic:
conjTranspose_smul,

Goal state after:
α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : star k • Aᴴ = k • A
hk : IsSelfAdjoint k
⊢ A.IsHermitian
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⁻¹ = A ^ n * A⁻¹

Tactic:
sub_add_cancel

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⁻¹ = A ^ n * A⁻¹
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 : A.IsSymm
k : ℤ
⊢ (A ^ k).IsSymm

Tactic:
IsSymm,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A.IsSymm
k : ℤ
⊢ (A ^ k)ᵀ = A ^ k
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℕ
hd : d ≠ 0
⊢ (↑d).PosDef

Tactic:
nontriviality R
  exact .diagonal fun _ ↦ by simpa [pos_iff_ne_zero]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
⊢ (↑d).PosDef

Tactic:
nontriviality R
  exact .diagonal fun _ ↦ by simpa [pos_iff_ne_zero]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M * M ^ k * M).PosSemidef

Tactic:
simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Finite n
inst✝ : StarOrderedRing R
a : n → R
⊢ (vecMulVec a (star a)).PosSemidef

Tactic:
by
  simp [vecMulVec_eq Unit, ← conjTranspose_replicateCol, posSemidef_self_mul_conjTranspose]

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
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective fun v ↦ v ᵥ* B
⊢ (B * A * Bᴴ).PosDef

Tactic:
replace hB := star_injective.comp <| hB.comp star_injective
  simp_rw [Function.comp_def, star_vecMul, star_star] at hB
  simpa using hA.conjTranspose_mul_mul_same (B := Bᴴ) hB

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
f : End R M
inst✝² : IsDomain R
inst✝¹ : Module.Finite R M
inst✝ : IsTorsionFree R M
⊢ {μ | f.HasEigenvalue μ}.Finite

Tactic:
have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)
  refine ((minpoly R f).rootSet_finite R).subset ?_
  simp [Set.subset_def, hasEigenvalue_iff_isRoot, mem_rootSet, h]

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

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))

Tactic:
simp [algebraMap, Algebra.algebraMap]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
⊢ b.base.cartanMatrix = (reindex b.baseSupportEquiv b.baseSupportEquiv) b.A

Tactic:
suffices b.base.cartanMatrix.reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm = b.A by
    rwa [← (reindex b.baseSupportEquiv b.baseSupportEquiv).symm_apply_eq]

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
⊢ (reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm) b.base.cartanMatrix = b.A
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (X + 1 + ↑n) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)

Tactic:
add_comm,

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + (X + 1)) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 1)) = ↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1))

Tactic:
add_succ,

Goal state after:
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 0).succ) = ↑(((a - ((b + 0).succ - 1) + b).succ - 1).descFactorial (b + 0).succ)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: a b : ℕ
⊢ eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)

Tactic:
← Nat.cast_add,

Goal state after:
a b : ℕ
⊢ eval (↑(a + b)) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
eq_comm

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : 0 = g
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
⊢ 0 = g
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : g = 0
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
⊢ 0 = g

Tactic:
eq_comm

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
h_deg_le : degree 0 ≤ ↑(#s)
h_deg_eq : 0 = g
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
⊢ 0 = g
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x) = 0

Tactic:
refine sum_eq_zero fun j H => ?_

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) ((interpolate s v) r) = r i

Tactic:
by
  rw [interpolate_apply, eval_finsetSum, ← add_sum_erase _ _ hi]
  simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, mul_one, add_eq_left]
  refine sum_eq_zero fun j H => ?_
  rw [eval_basis_of_ne (mem_erase.mp H).1 hi, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case e'_4.e'_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
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ 1 + (#t - #s) = #(insert i (t \ s))

Tactic:
card_insert_of_notMem (notMem_sdiff_of_mem_right hi),

Goal state after:
case e'_4.e'_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
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ 1 + (#t - #s) = #(t \ s) + 1
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
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
⊢ ↑k.factorial * ∑ t ∈ image (fun x ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1), ∏ va ∈ t, (X - C va) =
    ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (X - C (v a))

Tactic:
eq_comm

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
⊢ ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (X - C (v a)) =
    ↑k.factorial * ∑ t ∈ image (fun x ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1), ∏ va ∈ t, (X - C va)
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ((bind₁ g).comp (bind₁ f)) (X i✝) = (bind₁ fun i ↦ (bind₁ g) (f i)) (X i✝)

Tactic:
apply bind₁_bind₁

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ f ((bind₁ g) φ) = (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ

Tactic:
bind₁,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ f ((aeval g) φ) = (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ