mathlib-initiative/mathlib-tactics huggingface dataset:
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
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℕ
hn : chainBotCoeff (⇑α) β < n
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥

Tactic:
← @Nat.add_lt_add_iff_right (chainTopCoeff α β),

Goal state after:
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α : α.IsNonZero
n : ℕ
hn : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < n + chainTopCoeff (⇑α) β
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R P
inst✝ : Invertible 2
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ⅟2 • (Q₁.prod Q₂).polarBilin =
    LinearMap.compl₁₂ (⅟2 • Q₁.polarBilin) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ (⅟2 • Q₂.polarBilin) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)

Tactic:
polarBilin_prod,

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R P
inst✝ : Invertible 2
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ⅟2 •
      (LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
        LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)) =
    LinearMap.compl₁₂ (⅟2 • Q₁.polarBilin) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ (⅟2 • Q₂.polarBilin) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case a
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α : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ rootSpace H (↑(chainTopCoeff (⇑α) β') • ⇑α + ⇑β') ≠ ⊥

Tactic:
← coe_chainTop

Goal state after:
case a
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α : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ rootSpace H ⇑(chainTop (⇑α) β') ≠ ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case a
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α : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ rootSpace H (↑(chainTopCoeff (⇑α) β) • ⇑α + ⇑β) ≠ ⊥

Tactic:
← coe_chainTop

Goal state after:
case a
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α : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ rootSpace H ⇑(chainTop (⇑α) β) ≠ ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case a
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α : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ ↑(chainTopCoeff (⇑α) β) - n ≤ ↑(chainTopCoeff (⇑α) β')

Tactic:
refine ((rootSpace_zsmul_add_ne_bot_iff α β' hα _).mp ?_).1
    rw [hβ', ← add_assoc, ← add_smul, sub_add_cancel, ← coe_chainTop]
    exact (chainTop α β).2

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c✝ : ι → R
x : M := ∑ i ∈ s with 0 < c✝ i, c✝ i • v i
hx : x = ∑ i ∈ s with 0 < c✝ i, c✝ i • v i
y : M := ∑ i ∈ s with 0 < -c✝ i, -c✝ i • v i
hy : y = ∑ i ∈ s with 0 < -c✝ i, -c✝ i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : ∑ i ∈ s with 0 < c i, c i • v i = 0
i : ι
hi : i ∈ s
this : ∀ i ∈ {i ∈ s | 0 < c i}, c i * f (v i) = 0
hi' : 0 < c i
⊢ False

Tactic:
have : 0 < c i * f (v i) := mul_pos hi' (hp i)

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c✝ : ι → R
x : M := ∑ i ∈ s with 0 < c✝ i, c✝ i • v i
hx : x = ∑ i ∈ s with 0 < c✝ i, c✝ i • v i
y : M := ∑ i ∈ s with 0 < -c✝ i, -c✝ i • v i
hy : y = ∑ i ∈ s with 0 < -c✝ i, -c✝ i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : ∑ i ∈ s with 0 < c i, c i • v i = 0
i : ι
hi : i ∈ s
this✝ : ∀ i ∈ {i ∈ s | 0 < c i}, c i * f (v i) = 0
hi' : 0 < c i
this : 0 < c i * f (v i)
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
· dsimp [coweightHom] at hfg
    rw [MulOpposite.op_inj] at hfg
    set y := f.indexEquiv x with hy
    have : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y) := by
      exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)
    rw [coroot_coweightMap_apply, coroot_coweightMap_apply, Embedding.apply_eq_iff_eq, hy] at this
    rw [Equiv.symm_apply_apply] at this
    rw [this, Equiv.apply_symm_apply]

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
α✝ β✝ : Weight K (↥H) L
α β : ↥LieSubalgebra.root
⊢ ↑(↑(chainBotCoeff ⇑↑β ↑α) - ↑(chainTopCoeff ⇑↑β ↑α)) =
    (LinearMap.id ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } α))
      ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } β)

Tactic:
simp [apply_coroot_eq_cast β.1 α.1]

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
α✝ β✝ : Weight K (↥H) L
α β : ↥LieSubalgebra.root
⊢ (algebraMap ℤ K) (↑(chainBotCoeff ⇑↑β ↑α) - ↑(chainTopCoeff ⇑↑β ↑α)) = (rootSystem H).pairing α β

Tactic:
simp [apply_coroot_eq_cast β.1 α.1]

Goal state after:
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 : ι
this : InvolutiveNeg ι := P.indexNeg
z : ℤ
⊢ z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ z ∈ Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))

Tactic:
rw [P.chainCoeff_reflectionPerm_right_aux]

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

Tactic:
simpa using h'

Goal state after:
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]
k : ι
hk : P.root k = P.root j + P.root i
⊢ chainBotCoeff i k = chainBotCoeff i j + 1

Tactic:
have h' : LinearIndependent R ![P.root i, P.root k] := by simpa [hk, add_comm]

Goal state after:
ι : 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]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
⊢ chainBotCoeff i k = chainBotCoeff i j + 1
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
⊢ P.pairing i j = P.pairing j i

Tactic:
have := B.pairing_mul_eq_pairing_mul_swap j i

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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
this : P.pairing i j * (B.form (P.root j)) (P.root j) = P.pairing j i * (B.form (P.root i)) (P.root i)
⊢ P.pairing i j = P.pairing j i
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
inst✝¹ : IsDomain β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : const abv 1 ≈ const abv 0
this : ∀ ε > 0, ∃ i, ∀ (k : ℕ), i ≤ k → abv (1 - 0) < ε
h2 : 0 < abv 1
i : ℕ
hi : ∀ (k : ℕ), i ≤ k → abv (1 - 0) < abv 1
⊢ abv 1 < abv 1

Tactic:
simpa using hi _ le_rfl

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

Goal state before:
pp: x : ℝ
⊢ ∀ (a b c : ℝ), a ≤ b → a ≤ c → a ≤ b ⊓ c

Tactic:
by
    intro a b c
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    induction c using Real.ind_mk
    simp_rw [← mk_inf, mk_le]
    exact CauSeq.le_inf

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) B A *ᵥ X.vec = (A * X * Bᵀ).vec

Tactic:
ext ⟨k, l⟩
  simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]

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
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ ↑z.succ = ↑0

Tactic:
Int.ofNat_inj

Goal state after:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0
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
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ ↑z.succ = ↑0

Tactic:
Int.ofNat_inj

Goal state after:
case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0
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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (X ^ (n + 1))⁻¹ (Y ^ (n + 1))⁻¹

Tactic:
nonsing_inv_apply _ hx',

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (↑hx'.unit⁻¹ • (X ^ n.succ).adjugate) (Y ^ (n + 1))⁻¹
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
u : Mˣ
n : ℕ
⊢ ↑(u ^ ↑n) = ↑u ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]

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
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (A ^ z).det

Tactic:
rw [this, det_zero]

Goal state after:
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0
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✝¹ : Finite m
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).PosSemidef

Tactic:
by
  simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ

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

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Tactic:
have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)

Goal state after:
case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this✝ : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
this : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ (D - 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) ρ
⊢ ρ < 2 * μ

Tactic:
by
  by_contra! contra
  set N := μ • 1 - A with N_def
  have hN (i j : ι) : 0 ≤ N i j := by specialize hμ i j; aesop
  obtain ⟨v, hv, hv₀⟩ : ∃ v, N *ᵥ v = (μ - ρ) • v ∧ v ≠ 0 := by
    replace hρ : HasEigenvalue (toLin' N) (μ - ρ) := by simpa [N_def, hasEigenvalue_sub'_iff]
    simpa [hasEigenvector_iff, mulVec_transpose] using hρ.exists_hasEigenvector
  set q := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v| with q_def
  set Q := μ * ∑ i, d i * |v i| ^ 2 with Q_def
  have hq₀ : q < Q := by
    replace hv₀ : |v| ≠ 0 := by simpa
    have h₁ : 0 < ∑ j, ∑ i, |v i| * (d i * A i j) * |v j| := by
      simpa [dot_mulVec_eq_sum_sum] using hA.dotProduct_mulVec_pos hv₀
    have h₂ : Q = ∑ i, |v i| * (d i * μ) * |v i| := by
      rw [Q_def, Finset.mul_sum]; exact Finset.sum_congr rfl fun i _ ↦ by ring
    rw [q_def, N_def, dot_mulVec_eq_sum_sum]
    simpa [mul_sub, sub_mul, Matrix.one_apply, h₂]
  have hq₁ : Q ≤ q := by
    rw [Q_def, q_def, ← mulVec_mulVec, dotProduct_mulVec, dotProduct, Finset.mul_sum]
    refine Finset.sum_le_sum fun i _ ↦ ?_
    have h₀ : 0 ≤ ρ - μ := by grind [diag_pos_of_mul_diagonal_posDef A d hA hD hρ.nonempty.some]
    have h₁ : μ ≤ ρ - μ := by grind
    have h₂ : 0 ≤ d i := (hD i).le
    have h₃ : (ρ - μ) * |v i| ≤ (N *ᵥ |v|) i := by
      calc (ρ - μ) * |v i|
          = |μ - ρ| * |v i| := by rw [← abs_eq_self.mpr h₀, abs_sub_comm]
        _ = |(N *ᵥ v) i| := by simp [hv]
        _ = |∑ j, N i j * v j| := by simp [mulVec_eq_sum, mul_comm]
        _ ≤ ∑ j, |N i j * v j| := Finset.abs_sum_le_sum_abs _ _
        _ = ∑ j, N i j * |v j| := by simp [abs_eq_self.mpr (hN i _)]
        _ = (N *ᵥ |v|) i := by simp [mulVec_eq_sum, mul_comm]
    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]
  rw [← not_lt] at hq₁
  contradiction

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

Goal state before:
pp: n : ℕ
⊢ n.succ * n ! = ∏ i ∈ range (n + 1), (i + 1)

Tactic:
prod_range_succ_comm,

Goal state after:
n : ℕ
⊢ n.succ * n ! = (n + 1) * ∏ x ∈ range n, (x + 1)
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n k : ℕ
⊢ (n + k) * n.ascFactorial k = ∏ i ∈ range (k + 1), (n + i)

Tactic:
prod_range_succ_comm,

Goal state after:
n k : ℕ
⊢ (n + k) * n.ascFactorial k = (n + k) * ∏ x ∈ range k, (n + x)
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n k : ℕ
⊢ (n - k) * n.descFactorial k = ∏ i ∈ range (k + 1), (n - i)

Tactic:
prod_range_succ_comm,

Goal state after:
n k : ℕ
⊢ (n - k) * n.descFactorial k = (n - k) * ∏ x ∈ range k, (n - x)
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1

Tactic:
by
    rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]

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

Goal state before:
pp: case succ
S : Type u
inst✝ : Semiring S
n✝ : ℕ
⊢ eval 0 (ascPochhammer S (n✝ + 1)) = if n✝ + 1 = 0 then 1 else 0

Tactic:
simp [X_mul, ascPochhammer_succ_left]

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

Goal state before:
pp: a b : ℕ
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b

Tactic:
by
  rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']

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

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

Tactic:
apply_fun Polynomial.map (algebraMap ℤ R) at h
    simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_intCast] using h

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
i j : ι₁
hij : i ≠ j
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ j⁆ = 0

Tactic:
have hij' : eι i ≠ eι j := by aesop
    simp [Subtype.ext_iff, b₁.lie_e_f_ne i j hij, b₂.lie_e_f_ne _ _ hij']

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i, v i * f j ^ ↑i = 0
⊢ ∀ (j : Fin n), ∑ x, v x * f j ^ ↑x = 0

Tactic:
exact hfv

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
k : ℕ
⊢ f ^ k = (aeval f) (X ^ k %ₘ f.charpoly)

Tactic:
← aeval_eq_aeval_mod_charpoly,

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
k : ℕ
⊢ f ^ k = (aeval f) (X ^ k)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
h : coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
simp_all only [Ne, not_false_iff, zero_mul, mul_zero]

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : φ ∈ weightedHomogeneousSubmodule R w m
ψ : MvPolynomial σ R
hψ : ψ ∈ weightedHomogeneousSubmodule R w n
c : σ →₀ ℕ
hc : ∑ x ∈ antidiagonal c, coeff x.1 φ * coeff x.2 ψ ≠ 0
d e : σ →₀ ℕ
hde : (d, e) ∈ antidiagonal c
H : coeff d φ ≠ 0 → coeff e ψ = 0
h : ¬coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
simp_all only [Ne, not_false_iff, zero_mul, mul_zero]

Goal state after: