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

Goal state before:
pp: case 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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ P.root j - P.root i ∈ range ⇑P.root

Tactic:
]

Goal state after:
case 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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ P.root j - P.root i ∈ range ⇑P.root
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
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
this : LinearIndependent (ι := ↑(baseOf (⇑P.root) f)) ℚ v
⊢ ⊤ ≤ ⊤

Tactic:
]

Goal state after:
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 : ι
this : InvolutiveNeg ι := P.indexNeg
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (-j)]
z : ℤ
⊢ -↑(chainTopCoeff i j) ≤ z ∧ z ≤ ↑(chainBotCoeff i j) ↔ -↑(chainTopCoeff i j) ≤ z ∧ z ≤ ↑(chainBotCoeff i j)

Tactic:
]

Goal state after:
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
⊢ -∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root

Tactic:
]

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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ -∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root
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) = ⊤
b : Basis ↑(baseOf (⇑P.root) f) ℚ ↥(P.rootSpan ℚ) :=
  have this := ⋯;
  Basis.mk this ⋯
⊢ Nat.card ↑(baseOf (⇑P.root) f) = Nat.card ↑(baseOf (⇑P.root) f)

Tactic:
]

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 (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) j) ↔
    z ∈ Icc (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) j)

Tactic:
]

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) = ⊤
h_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
⊢ span R ↑(map (P.rootSpan ℚ).subtype ⊤) = ⊤

Tactic:
]

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
⊢ span R ↑(map (P.rootSpan ℚ).subtype ⊤) = ⊤
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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ f i • P.root i + f j • P.root j = P.root i - P.root j

Tactic:
]

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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ f i • P.root i + f j • P.root j = P.root i - P.root j
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 (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j)) ↔
    z ∈ Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))

Tactic:
]

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

Goal state before:
pp: case neg.inl
ι : 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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4
⊢ -P.root i ∈ range ⇑P.root

Tactic:
]

Goal state after:
case neg.inl
ι : 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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4
⊢ -P.root i ∈ range ⇑P.root
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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
]

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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ P.root i - P.root j ∈ range ⇑P.root
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_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
h_span : span R (range (⇑(P.rootSpan ℚ).subtype ∘ v)) = ⊤
⊢ Nat.card ↑(baseOf (⇑P.root) f) = Nat.card ↑(baseOf (⇑P.root) f)

Tactic:
]

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

Goal state before:
pp: case neg.inr.inl
ι : 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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : i = j
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
]

Goal state after:
case neg.inr.inl
ι : 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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : i = j
⊢ P.root i - P.root j ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ j i = 1 ∧ P.pairingIn ℤ i j = 4
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
]

Goal state after:
case neg.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
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ j i = 1 ∧ P.pairingIn ℤ i j = 4
⊢ P.root i - P.root j ∈ range ⇑P.root
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
hf' : ∀ (i : ι), f (P.root i) ≠ 0
aux :
  ∀ (i : ι),
    P.root i ∈ AddSubmonoid.closure (⇑P.root '' baseOf (⇑P.root) f) ∨
      -P.root i ∈ AddSubmonoid.closure (⇑P.root '' baseOf (⇑P.root) f)
⊢ finrank R M = finrank R M

Tactic:
]

Goal state after:
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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ ↑(chainTopCoeff ↑i ↑j) = ↑(chainTopCoeff ↑i ↑j) - ↑(chainBotCoeff ↑i ↑j)

Tactic:
]

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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ ↑(chainTopCoeff ↑i ↑j) = ↑(chainTopCoeff ↑i ↑j) - ↑(chainBotCoeff ↑i ↑j)
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
this : s ⊆ baseOf (⇑P.root) f
⊢ s.ncard ≤ s.ncard

Tactic:
]

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]
h : ∀ (x : ℕ), x ≤ chainBotCoeff i j ↔ x = 0
⊢ chainBotCoeff i j ≤ chainBotCoeff i j

Tactic:
]

Goal state after:
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
x✝ : ↥(P.rootSpan ℤ)
x : M
hx : x ∈ P.rootSpan ℤ
⊢ (P.rootSpan ℤ).subtype ⟨x, hx⟩ ∈ ↑(map (P.rootSpan ℤ).subtype (span ℤ (P.rootSpanMem ℤ '' ↑b.support)))

Tactic:
]

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
x✝ : ↥(P.rootSpan ℤ)
x : M
hx : x ∈ P.rootSpan ℤ
⊢ (P.rootSpan ℤ).subtype ⟨x, hx⟩ ∈ ↑(map (P.rootSpan ℤ).subtype (span ℤ (P.rootSpanMem ℤ '' ↑b.support)))
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 : ι
inst✝ : IsDomain R
hp : i ≠ j
hn : P.root i ≠ -P.root j
h_add : P.root i + P.root j ∉ range ⇑P.root
h_sub : P.root i - P.root j ∉ range ⇑P.root
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i j : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i + P.root j ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
⊢ P.root i ∈ ↑⟨q, hq✝⟩ ↔ P.root j ∈ ↑⟨q, hq✝⟩

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i j : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i + P.root j ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
⊢ P.root i ∈ ↑⟨q, hq✝⟩ ↔ P.root j ∈ ↑⟨q, hq✝⟩
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i j : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i + P.root j ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
this : ∀ (i j : ι), P.root i + P.root j ∈ range ⇑P.root → P.root i ∈ q → P.root j ∈ q
⊢ P.root i + P.root j ∈ range ⇑P.root

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i j : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i + P.root j ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
this : ∀ (i j : ι), P.root i + P.root j ∈ range ⇑P.root → P.root i ∈ q → P.root j ∈ q
⊢ P.root i + P.root j ∈ range ⇑P.root
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:
]

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

Tactic:
]

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: ι : 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 : ι
⊢ chainBotCoeff ((P.reflectionPerm i) i) j = 0 ↔
    ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j + P.root i ∉ range ⇑P.root

Tactic:
]

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 : ι
⊢ chainBotCoeff ((P.reflectionPerm i) i) j = 0 ↔
    ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j + P.root i ∉ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i✝ j✝ : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i✝ + P.root j✝ ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
i j k : ι
hk : P.root k = P.root i + P.root j
hi : P.root i ∈ q
hij₀ : P.pairing i j = 0
⊢ ¬(P.toLinearMap (P.root i + P.root j)) (P.coroot i) = 0

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i✝ j✝ : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i✝ + P.root j✝ ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
i j k : ι
hk : P.root k = P.root i + P.root j
hi : P.root i ∈ q
hij₀ : P.pairing i j = 0
⊢ ¬(P.toLinearMap (P.root i + P.root j)) (P.coroot i) = 0