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

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 j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (P.pairing i j * P.pairing j i) • P.root i = P.pairing i j • 2 • P.root j

Tactic:
rw [mul_smul, h₁]

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
⊢ chainLength (-α) β = chainLength α β

Tactic:
← chainBotCoeff_add_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
⊢ chainBotCoeff (⇑(-α)) β + chainTopCoeff (⇑(-α)) β = chainLength α β
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
⊢ chainBotCoeff (⇑(-α)) β + chainTopCoeff (⇑(-α)) β = chainLength α β

Tactic:
← chainBotCoeff_add_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
⊢ chainBotCoeff (⇑(-α)) β + chainTopCoeff (⇑(-α)) β = chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a • a • p.1 p.2 = (a * a) • p.1 p.2

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a * a • p.1 p.2 = (a * a) • p.1 p.2
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a * a • p.1 p.2 = (a * a) • p.1 p.2

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a * (a * p.1 p.2) = (a * a) • p.1 p.2
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a * (a * p.1 p.2) = (a * a) • p.1 p.2

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ a * (a * p.1 p.2) = a * a * p.1 p.2
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 (⇑α) β) - n) • ⇑α + ⇑β') ≠ ⊥

Tactic:
rw [hβ', ← add_assoc, ← add_smul, sub_add_cancel, ← 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: 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
⊢ chainLength α 0 = 2

Tactic:
← chainBotCoeff_add_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
inst✝ : Nontrivial L
hα : α.IsNonZero
⊢ chainBotCoeff (⇑α) 0 + chainTopCoeff (⇑α) 0 = 2
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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
⊢ Submonoid.closure (range (Equiv.reflection P) ∪ (range (Equiv.reflection P))⁻¹) =
    Submonoid.closure (range (Equiv.reflection P))

Tactic:
← 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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
⊢ Submonoid.closure (range (Equiv.reflection P) ∪ range (Equiv.reflection P)) =
    Submonoid.closure (range (Equiv.reflection P))
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2.one
ι : 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
w : P.Aut
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup) 1 ∈ Subgroup.closure (range P.reflection)

Tactic:
simp only [map_one, one_mem]

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

Goal state before:
pp: case refine_2.one
ι : 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
w : P.Aut
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup) 1 ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simp only [map_one, one_mem]

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

Goal state before:
pp: case refine_2.one
ι : 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
w : P.Aut
⊢ ((Equiv.indexHom P).domRestrict P.weylGroup) 1 ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
simp only [map_one, one_mem]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ ((t • s) • y) • v = t • (s • y) • v

Tactic:
smul_eq_mul,

Goal state after:
case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ ((t * s) • y) • v = t • (s • y) • v
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case weightMap
ι : 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 : M
⊢ f.weightMap x = g.weightMap x

pp: case coweightMap
ι : 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 : N
⊢ f.coweightMap x = g.coweightMap x

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
    have h := congrArg (LinearMap.comp (M₃ := Module.Dual R M) (σ₂₃ := .id R) P.flip.toPerfPair) hfg
    rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h
    have : f.weightMap = g.weightMap := by
      have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
      refine (Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
        ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))
    exact congrFun (congrArg DFunLike.coe this) x

Goal state after:
case coweightMap
ι : 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 : N
⊢ f.coweightMap x = g.coweightMap x

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
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case pos
ι : 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
k : ι
hk : P.root k ∈ Q
j : ι
hj : j ∈ {i | P.root i ∉ Q}
⊢ P.pairing j k = 0

Tactic:
P.pairing_eq_zero_iff',

Goal state after:
case pos
ι : 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
k : ι
hk : P.root k ∈ Q
j : ι
hj : j ∈ {i | P.root i ∉ Q}
⊢ P.pairing k j = 0
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_2
ι : 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
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
q' : ↥P.invtRootSubmodule := ⟨q, ⋯⟩
⊢ q = ⊤

Tactic:
replace hq' : ⊥ < q' := by simpa [q', bot_lt_iff_ne_bot, -IsSimpleOrder.bot_lt_iff_eq_top]

Goal state after:
case refine_2
ι : 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
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
q' : ↥P.invtRootSubmodule := ⟨q, ⋯⟩
hq' : ⊥ < q'
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
ht : ↑z • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * ↑z = 1
this : ↑z * ↑w = 1
⊢ z = 1 ∨ z = -1

Tactic:
norm_cast 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✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
ht : ↑z • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * ↑z = 1
this : z * w = 1
⊢ z = 1 ∨ z = -1
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
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)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
i : ι
hi : P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
x y : M
hx : x ∈ AddSubmonoid.closure (⇑P.root '' s)
hy : y ∈ AddSubmonoid.closure (⇑P.root '' s)
x✝¹ : ∃ z, f x = ↑z
x✝ : ∃ z, f y = ↑z
n : ℤ
hn : f x = ↑n
m : ℤ
hm : f y = ↑m
⊢ f (x + y) = ↑(n + m)

Tactic:
simp [hn, hm]

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
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)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
i : ι
hi : P.root (-i) ∈ AddSubmonoid.closure (⇑P.root '' s)
x y : M
hx : x ∈ AddSubmonoid.closure (⇑P.root '' s)
hy : y ∈ AddSubmonoid.closure (⇑P.root '' s)
x✝¹ : ∃ z, f x = ↑z
x✝ : ∃ z, f y = ↑z
n : ℤ
hn : f x = ↑n
m : ℤ
hm : f y = ↑m
⊢ f (x + y) = ↑(n + m)

Tactic:
simp [hn, hm]

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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₁_def : S₁ = {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
x✝ : ℤ
⊢ x✝ ∈ S₁ ↔ x✝ ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)

Tactic:
S₁_def,

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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₁_def : S₁ = {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
x✝ : ℤ
⊢ x✝ ∈ {z | P.root j + z • P.root i ∈ range ⇑P.root} ↔ x✝ ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
⊢ f1 ^ 0 ≈ f2 ^ 0

Tactic:
simp only [pow_zero, Setoid.refl]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (if h : f.LimZero then 0 else f.inv h) = f.inv hf

Tactic:
rw [dif_neg]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ (∀ (a : n) (b : m), A.vec (a, b) = B.vec (a, b)) ↔ ∀ (b : n) (a : m), A a b = B a b

Tactic:
vec

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ Aᴴ.map f = A.map f

Tactic:
h.eq

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ A.map f = A.map f
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:
h.eq

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
⊢ k • A = k • A
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, ∑ x_1, X.vec (x, x_1) * (B x k * A x_1 l) = ∑ x, ∑ x_1, X x_1 x * (B x k * A x_1 l)

Tactic:
vec

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
M : Matrix n n R
hM : M.PosDef
x : n →₀ R
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * M i j * xj

Tactic:
by obtain rfl | hx := eq_or_ne x 0 <;> simp [le_of_lt, hM.2, *]

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

Goal state before:
pp: case mpr
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
⊢ (D - Bᴴ * A⁻¹ * B).PosSemidef →
    (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x

Tactic:
refine fun h => ⟨h.1, fun x => ?_⟩

Goal state after:
case mpr
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).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
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
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + ↑q.natDegree ≤ ↑q.natDegree
⊢ False

Tactic:
norm_cast at this

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + q.natDegree ≤ q.natDegree
⊢ False
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
⊢ f.eigenspace (-q.coeff 0 / q.leadingCoeff) =
    LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0))

Tactic:
apply eigenspace_div
          rw [Ne, leadingCoeff_eq_zero_iff_deg_eq_bot, hq]
          exact WithBot.one_ne_bot

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!

Tactic:
by
  induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [prod_cons, Finset.sum_cons]
    exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

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
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp') ∨
    -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
refine hs.symm.imp (fun ⟨n, hn₀, hn⟩ ↦ ?_) (fun ⟨n, hn₀, hn⟩ ↦ ?_) <;> simpa [hn] using this n

Goal state after: