mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case mp
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0) →
    ∀ i ∉ {i | w i = 0}, v i = 0

pp: case mpr
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∀ i ∉ {i | w i = 0}, v i = 0) →
    ∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0

Tactic:
·

Goal state after:
case mp
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0) →
    ∀ i ∉ {i | w i = 0}, v i = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case mpr
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∀ i ∉ {i | w i = 0}, v i = 0) →
    ∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0

Tactic:
·

Goal state after:
case mpr
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∀ i ∉ {i | w i = 0}, v i = 0) →
    ∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
j : ℕ
⊢ (∃ V, Module.finrank R ↥V = j ∧ (restrict Q V).PosDef) ↔ ∃ V, Module.finrank R ↥V = j ∧ (restrict Q' V).PosDef

pp: case e'_4
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
⊢ Module.finrank R M = Module.finrank R M'

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
j : ℕ
⊢ (∃ V, Module.finrank R ↥V = j ∧ (restrict Q V).PosDef) ↔ ∃ V, Module.finrank R ↥V = j ∧ (restrict Q' V).PosDef
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case e'_4
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
⊢ Module.finrank R M = Module.finrank R M'

Tactic:
·

Goal state after:
case e'_4
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
⊢ Module.finrank R M = Module.finrank R M'
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case h
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ ∀ i ∈ univ, 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

pp: case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ ∃ i ∈ univ, 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
·

Goal state after:
case h
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ ∀ i ∈ univ, 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case pos
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
i : ι
a✝ : i ∈ univ
hi : i ∈ s
⊢ 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

pp: case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
i : ι
a✝ : i ∈ univ
hi : i ∈ s
⊢ 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ ∃ i ∈ univ, 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
·

Goal state after:
case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ ∃ i ∈ univ, 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case pos
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∈ s
⊢ w i * (x i * x i) ≤ 0

pp: case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ w i * (x i * x i) ≤ 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∈ s
⊢ w i * (x i * x i) ≤ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ w i * (x i * x i) ≤ 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, w i ≤ 0
x : ι → 𝕜
hx : x ∈ Pi.spanSubset 𝕜 s
i : ι
a✝ : i ∈ univ
hi : i ∉ s
⊢ w i * (x i * x i) ≤ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p : Set ι := {i | 0 < w i}
m : Set ι := {i | w i ≤ 0}
this✝¹ : p.ncard + m.ncard = Nat.card ι
this✝ : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w)
this : sigPos (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι
⊢ sigPos (weightedSumSquares 𝕜 w) = p.ncard

Tactic:
by lia

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

Goal state before:
pp: case e'_2
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ -weightedSumSquares 𝕜 w = weightedSumSquares 𝕜 (-w)

pp: case e'_3
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0} = {i | 0 < (-w) i}

Tactic:
·

Goal state after:
case e'_2
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ -weightedSumSquares 𝕜 w = weightedSumSquares 𝕜 (-w)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case e'_3
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0} = {i | 0 < (-w) i}

Tactic:
·

Goal state after:
case e'_3
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0} = {i | 0 < (-w) i}
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ({i | w i < 0} ∪ {i | w i = 0}).ncard = {i | w i ≤ 0}.ncard

pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | w i < 0} {i | w i = 0}

Tactic:
·

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ({i | w i < 0} ∪ {i | w i = 0}).ncard = {i | w i ≤ 0}.ncard
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | w i < 0} {i | w i = 0}

Tactic:
·

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | w i < 0} {i | w i = 0}
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ({i | 0 < w i} ∪ {i | w i ≤ 0}).ncard = Set.univ.ncard

pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | 0 < w i} {i | w i ≤ 0}

Tactic:
·

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ({i | 0 < w i} ∪ {i | w i ≤ 0}).ncard = Set.univ.ncard
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | 0 < w i} {i | w i ≤ 0}

Tactic:
·

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | 0 < w i} {i | w i ≤ 0}
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:

Tactic:
{i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard
  _ = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard := by
    rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
    · congr! 1
      ext
      grind
    · grind [disjoint_iff_ne]
  _ = Set.univ.ncard := by
    rw [← Set.ncard_union_eq]
    · congr! 1
      ext
      grind [le_iff_lt_or_eq]
    · grind [disjoint_iff_ne]
  _ = Nat.card ι := Set.ncard_univ _

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : 0 < P.pairingIn ℤ j k
⊢ P.root k - P.root j ∈ range ⇑P.root

pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
⊢ P.root k - P.root j ∈ range ⇑P.root

Tactic:
·

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : 0 < P.pairingIn ℤ j k
⊢ P.root k - P.root j ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ω b * ω b = 1

Tactic:
ext (k | k) (l | l)

Goal state after:
case inl.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
b : P.Base
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
k l : ↥b.support
⊢ (ω b * ω b) (Sum.inl k) (Sum.inl l) = 1 (Sum.inl k) (Sum.inl l)

case inl.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
b : P.Base
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
k : ↥b.support
l : ι
⊢ (ω b * ω b) (Sum.inl k) (Sum.inr l) = 1 (Sum.inl k) (Sum.inr l)

case 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
b : P.Base
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
k : ι
l : ↥b.support
⊢ (ω b * ω b) (Sum.inr k) (Sum.inl l) = 1 (Sum.inr k) (Sum.inl l)

case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
k l : ι
⊢ (ω b * ω b) (Sum.inr k) (Sum.inr l) = 1 (Sum.inr k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
⊢ ω b * h i = -h i * ω b

Tactic:
ext (k | k) (l | l)

Goal state after:
case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k l : ↥b.support
⊢ (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)

case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k : ↥b.support
l : ι
⊢ (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)

case 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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k : ι
l : ↥b.support
⊢ (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)

case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k l : ↥b.support
⊢ (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)

pp: case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k : ↥b.support
l : ι
⊢ (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)

pp: case 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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k : ι
l : ↥b.support
⊢ (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
·

Goal state after:
case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k l : ↥b.support
⊢ (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k : ↥b.support
l : ι
⊢ (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)

pp: case 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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k : ι
l : ↥b.support
⊢ (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
·

Goal state after:
case inl.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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i k : ↥b.support
l : ι
⊢ (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case 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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k : ι
l : ↥b.support
⊢ (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
·

Goal state after:
case 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✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k : ι
l : ↥b.support
⊢ (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
·

Goal state after:
case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)