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

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    ∑ i_1, P.pairingIn S i i_1 • P.coroot i_1 + ∑ x, -(P.pairingIn S i x • P.coroot x) +
      ∑ x, P.pairingIn S i x • (P.toLinearMap (P.root i)) (P.coroot x) • P.coroot i

Tactic:
← sub_eq_iff_eq_add,

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i -
      ∑ x, P.pairingIn S i x • (P.toLinearMap (P.root i)) (P.coroot x) • P.coroot i =
    ∑ i_1, P.pairingIn S i i_1 • P.coroot i_1 + ∑ x, -(P.pairingIn S i x • P.coroot x)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
⊢ finrank S ↥(P.PolarizationIn S).range = finrank S ↥(P.corootSpan S)

Tactic:
apply (Submodule.finrank_mono (P.range_polarizationIn_le_span_coroot S)).antisymm
  have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
  have : Module.IsTorsionFree S N := .trans_faithfulSMul S R N
  have h_ne : ∏ i, (P.RootFormIn S (P.rootSpanMem S i) (P.rootSpanMem S i)) ≠ 0 := by
    refine Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_
    have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h
    rw [algebraMap_rootFormIn] at this
    apply IsAnisotropic.rootForm_root_ne_zero i this
  refine LinearMap.finrank_le_of_isSMulRegular (P.corootSpan S)
    (LinearMap.range (M₂ := N) (P.PolarizationIn S))
    (smul_right_injective N h_ne) ?_
  intro _ hx
  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun S).mp hx
  rw [← hc, Finset.smul_sum]
  simp_rw [smul_smul, mul_comm, ← smul_smul]
  exact Submodule.sum_smul_mem (LinearMap.range (P.PolarizationIn S)) c
    fun j _ ↦ prod_rootFormIn_smul_coroot_mem_range_PolarizationIn P S j

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

Goal state before:
pp: case hg₂
ι : 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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ MapsTo (⇑(sα ∘ₗ sβ ∘ₗ sα)) (range ⇑root) (range ⇑root)

Tactic:
exact (hs i).comp <| (hs j).comp (hs i)

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = ↑(chainTopCoeff (⇑α) β) * α (coroot α) + β (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))

Tactic:
root_apply_coroot hα

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = ↑(chainTopCoeff (⇑α) β) * 2 + β (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case h₂
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e✝ f : L
he : e✝ ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e✝ f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : 0 = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1 + 1)) x
e : 1 < chainTopCoeff (⇑α) 0
this : chainLength α 0 = 2 * chainTopCoeff (⇑α) 0
⊢ chainTopCoeff (⇑α) 0 + 1 < 2 * chainTopCoeff (⇑α) 0

Tactic:
two_mul,

Goal state after:
case h₂
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e✝ f : L
he : e✝ ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e✝ f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : 0 = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1 + 1)) x
e : 1 < chainTopCoeff (⇑α) 0
this : chainLength α 0 = 2 * chainTopCoeff (⇑α) 0
⊢ chainTopCoeff (⇑α) 0 + 1 < chainTopCoeff (⇑α) 0 + chainTopCoeff (⇑α) 0
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
ι₂✝ : 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₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective ⇑((↑g).comp ↑f).coweightMap

Tactic:
simp only [Hom.comp, LinearMap.coe_comp]
      exact Bijective.comp f.bijective_coweightMap g.bijective_coweightMap

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ ⨆ α, ⨆ (_ : α.IsNonZero), corootSubmodule α = H.toLieSubmodule

Tactic:
by
  suffices ⨆ α : Weight K H L, ⨆ (_ : α.IsNonZero), corootSpace α = ⊤ from
    le_antisymm (by simp) (by simp [← LieSubmodule.map_iSup, this])
  simp

Goal state after:
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 : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
h_ker : ∀ (k : ι), (P.coroot' k) t = 0
⊢ t = 0

Tactic:
exact P.eq_zero_iff_forall_coroot'_eq_zero.mpr h_ker

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
ι₂ : 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)
this : Q = RootPairing.map e f g
⊢ ⇑↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑e.symm

Tactic:
by
      ext i
      rw [LinearEquiv.coe_coe, comp_apply, ← LinearEquiv.eq_symm_apply]
      conv_lhs => rw [this]
      rfl

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

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✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
⊢ ∃ Φ, (∀ i ∈ Φ, ¬Disjoint q (R ∙ P.root i)) ∧ ∀ i ∉ Φ, q ≤ ker (P.coroot' i)

Tactic:
by
  refine ⟨{i | ¬ Disjoint q (R ∙ P.root i)}, by simp, fun i hi ↦ ?_⟩
  simp only [mem_ofPred_eq, not_not] at hi
  rw [← Submodule.mem_invtSubmodule_reflection_iff (by simp) hi]
  exact hq i

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

Tactic:
obtain ⟨n, hcn⟩ : ∃ n : ℕ, P.coxeterWeightIn ℤ i j = n := by
    have : 0 ≤ P.coxeterWeightIn ℤ i j := by
      simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j
    obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this
    exact ⟨n, by simp [hn]⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : 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]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
h' : chainBotCoeff i j = 0
⊢ n = 0

Tactic:
rw [root_sub_nsmul_mem_range_iff_le_chainBotCoeff h] at h''

Goal state after:
case pos
ι : 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]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : n ≤ chainBotCoeff i j
h' : chainBotCoeff i j = 0
⊢ n = 0
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : 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]
⊢ P.root (chainTopIdx i j) = P.root j + chainTopCoeff i j • P.root i

Tactic:
simp only [chainTopIdx, reduceDIte, h]

Goal state after:
case pos
ι : 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]
⊢ P.root (Exists.choose ⋯) = P.root j + chainTopCoeff i j • P.root i
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : Cauchy abs
⊢ { cauchy := f⁻¹ } = { cauchy := f }.inv'

Tactic:
inv'

Goal state after:
f : Cauchy abs
⊢ { cauchy := f⁻¹ } =
    match { cauchy := f } with
    | { cauchy := a } => { cauchy := a⁻¹ }
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : Cauchy abs
⊢ { cauchy := f }.inv'.cauchy = { cauchy := f }.cauchy⁻¹

Tactic:
inv'

Goal state after:
f : Cauchy abs
⊢ (match { cauchy := f } with
      | { cauchy := a } => { cauchy := a⁻¹ }).cauchy =
    { cauchy := f }.cauchy⁻¹
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]

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

Goal state before:
pp: case inl
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⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ Commute A (B ^ m)

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:
· refine SemiconjBy.zpow_right ?_ ?_ h _ <;> exact isUnit_det_of_left_inverse hB

Goal state after:
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)
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 n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
⊢ (Bᴴ * A * B).PosDef

Tactic:
refine of_dotProduct_mulVec_pos (isHermitian_conjTranspose_mul_mul _ hA.1) fun x hx => ?_

Goal state after:
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 n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
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|
⊢ False

Tactic:
set Q := μ * ∑ i, d i * |v i| ^ 2 with Q_def

Goal state after:
ι : 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
⊢ False
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
by
  rw [← mem_degreeLT] at degree_f_lt degree_g_lt
  refine eq_of_degree_sub_lt_of_eval_finset_eq _ ?_ eval_fg
  rw [← mem_degreeLT]; exact Submodule.sub_mem _ degree_f_lt degree_g_lt

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ (Lagrange.basis s v i).degree < ↑(#s)

Tactic:
rw [degree_basis hvs hi, Nat.cast_withBot, WithBot.coe_lt_coe]

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ #s - 1 < #s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ (Lagrange.basis s v i).leadingCoeff = (∏ j ∈ s.erase i, (v i - v j))⁻¹

Tactic:
have : (∏ j ∈ s.erase i, (X - C (v j))).coeff (#s - 1) = 1 := by
    simpa [hi] using (monic_prod_X_sub_C v (s.erase i)).coeff_natDegree
  simp_rw [leadingCoeff, natDegree_basis hvs hi, Lagrange.basis]
  simp [basisDivisor, Finset.prod_mul_distrib, ← map_prod, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i ↦ v i - a).det = (vandermonde v).det

Tactic:
← det_vandermonde_add v (-a)

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i ↦ v i - a).det = (vandermonde fun i ↦ v i + -a).det
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)
⊢ (⇑derivative)^[k] (∏ vj ∈ image v (s.erase i), (X - C vj)) =
    ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (image v (s.erase i)), ∏ va ∈ t, (X - C va)

Tactic:
by
        grind [iterate_derivative_prod_X_sub_C]

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

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

Tactic:
calc
    (P * A * Q).charpoly = (φ (P * A * Q)).charpoly := (charpoly_reindex ..).symm
    _ = (φ₁ P * φ₂ A * φ₃ Q).charpoly := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
    _ = A.charpoly := by rw [charpoly_mul_comm, ← mul_assoc]; simp [P, Q, φ₁, φ₂, φ₃]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' (s₁ ∪ s₂))

Tactic:
Set.image_union

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' s₁ ∪ Subtype.val '' s₂)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m})
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ ∀ (a : R), motive (C a * p) ⋯

Tactic:
refine (Submodule.span_le (p := A) |>.mpr ?_ hp).2

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous w p m
hp : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m})
A : Submodule R (MvPolynomial σ R) :=
  { carrier := {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}, add_mem' := ⋯, zero_mem' := ⋯,
    smul_mem' := ⋯ }
⊢ (fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = m} ⊆ ↑A