mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case «0».«1»
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
⊢ ↑A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
aesop

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

Goal state before:
pp: case «1».«0»
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
⊢ ↑A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
aesop

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

Goal state before:
pp: case «1».«1»
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
⊢ ↑A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
aesop

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝⁴ : Unique m
inst✝³ : Unique n
inst✝² : Semiring A
inst✝¹ : CommSemiring R
inst✝ : Algebra R A
r : R
⊢ uniqueRingEquiv.toFun ((algebraMap R (Matrix m m A)) r) = (algebraMap R A) r

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → Semiring (A i)
inst✝⁵ : Algebra R' R
inst✝⁴ : (i : ι) → Algebra R (A i)
inst✝³ : (i : ι) → Algebra R' (A i)
inst✝² : ∀ (i : ι), IsScalarTower R' R (A i)
S : Type u_5
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : MultilinearMap R A S
one : f 1 = 1
mul : ∀ (x y : (i : ι) → A i), f (x * y) = f x * f y
⊢ (LinearMap.mul R (⨂[R] (i : ι), A i)).compr₂ (lift f) = (LinearMap.mul R S ∘ₗ lift f).compl₂ (lift f)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
x : { v // v ≠ 0 } ⊕ Unit
⊢ (fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val (fun x ↦ 0) x) = x

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
x : V
⊢ Sum.elim Subtype.val (fun x ↦ 0) ((fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) x) = x

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
⊢ ∃ g, g • D = E ∧ g • D' = E'

Tactic:
by
      obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹
      use ⟨g * h, by simp [hdet]⟩
      simp [specialLinearGroup_smul_def, toLinearEquiv_eq_coe, mul_smul, gD, hD, gE, hE]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
f : SpecialLinearGroup R V
⊢ (fun a ↦ ↑a) ((fun g ↦ ⟨e ≪≫ₗ ↑g ≪≫ₗ e.symm, ⋯⟩) ((fun f ↦ ⟨e.symm ≪≫ₗ ↑f ≪≫ₗ e, ⋯⟩) f)) = (fun a ↦ ↑a) f

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
⊢ (fun a ↦ ↑a) ((fun f ↦ ⟨e.symm ≪≫ₗ ↑f ≪≫ₗ e, ⋯⟩) ((fun g ↦ ⟨e ≪≫ₗ ↑g ≪≫ₗ e.symm, ⋯⟩) g)) = (fun a ↦ ↑a) g

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
f g : SpecialLinearGroup R V
⊢ (fun a ↦ ↑a) ⟨e.symm ≪≫ₗ ↑(f * g) ≪≫ₗ e, ⋯⟩ = (fun a ↦ ↑a) (⟨e.symm ≪≫ₗ ↑f ≪≫ₗ e, ⋯⟩ * ⟨e.symm ≪≫ₗ ↑g ≪≫ₗ e, ⋯⟩)

Tactic:
aesop

Goal state after:
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 : ι
a✝ : i ∈ univ
⊢ 0 ≤ w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
by_cases hi : i ∈ s

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)

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: 𝕜 : 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
⊢ w i * (x i * x i) ≤ 0

Tactic:
by_cases hi : i ∈ s

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

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.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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
x✝¹ : ↥b.support
x✝ : ↥b.support ⊕ ι
⊢ (Matrix.diagLinearMap (↥b.support ⊕ ι) R R)
      (Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑x✝¹))) x✝ =
    (⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i) x✝¹ x✝

Tactic:
aesop

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

Goal state before:
pp: ι : 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
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairingIn ℤ i k ≤ -2
hk' : P.root i ≠ -P.root k
aux : P.pairingIn ℤ i k = -2 → ¬P.pairingIn ℤ k i = -2
this :
  (P.pairingIn ℤ i k, P.pairingIn ℤ k i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
⊢ P.pairingIn ℤ k i = -1

Tactic:
aesop

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

Goal state before:
pp: ι : 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 j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
hk : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hkj : -k = i
⊢ P.root k = -P.root i

Tactic:
aesop

Goal state after:
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 : ι
⊢ ∑ a₁,
        Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inr k) (Sum.inl a₁) *
          Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl a₁) (Sum.inr l) +
      ∑ a₂, Matrix.of (fun i j ↦ if i = -j then 1 else 0) k a₂ * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑i)) a₂ l =
    ∑ a₁,
        (-Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i))) (Sum.inr k) (Sum.inl a₁) *
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl a₁) (Sum.inr l) +
      ∑ a₂,
        (-Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i))) (Sum.inr k) (Sum.inr a₂) *
          Matrix.of (fun i j ↦ if i = -j then 1 else 0) a₂ l

Tactic:
aesop

Goal state after:
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✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ -k →
      (if P.root b_1 = P.root ↑i + P.root l then (if -k = b_1 then 1 else 0) * (↑(chainBotCoeff (↑i) l) + 1)
        else (if -k = b_1 then 1 else 0) * 0) =
        0

Tactic:
aesop

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

Goal state before:
pp: case refine_1
ι : 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
inst✝⁴ : P.IsReduced
inst✝³ : P.IsIrreducible
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
h : ∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3
i j : ι
hij : ¬P.pairingIn ℤ ((P.reflectionPerm i) i) j = -3
this :
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
⊢ P.pairingIn ℤ i j = -2 ∨
    P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2

Tactic:
aesop

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

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✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainBotCoeff i j) + ↑(chainTopCoeff i j) ≤ 2

Tactic:
chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h

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✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : LinearIndependent R ![P.root i, P.root j]
⊢ P.pairingIn ℤ (chainTopIdx i j) i ≤ 2
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : LinearIndependent R ![P.root i, P.root j]
this : P.pairingIn ℤ (chainTopIdx i j) i ∈ {-2, -1, 0, 1, 2}
⊢ P.pairingIn ℤ (chainTopIdx i j) i ≤ 2

Tactic:
aesop

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

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✝⁷ : IsDomain R
inst✝⁶ : CharZero 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✝ : Fintype ι
i j k : ↥b.support
l : ι
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ l →
      Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) k b_1 *
          Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inr b_1) (Sum.inr l) =
        0

Tactic:
aesop

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

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.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
this :
  (P.pairingIn ℤ (long P) (short P), P.pairingIn ℤ (short P) (long P)) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
⊢ P.pairingIn ℤ (short P) (long P) = -1

Tactic:
aesop

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

Goal state before:
pp: case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero 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✝ : Fintype ι
i j k : ↥b.support
l : ι
⊢ ∑ a₁,
        Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inl k) (Sum.inl a₁) *
          Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) a₁ l -
      (∑ a₁,
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
              (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
              (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
              (Sum.inl k) (Sum.inl a₁) *
            0 +
        if l ∈ Finset.univ then
          Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) k l *
            Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inr l) (Sum.inr l)
        else 0) =
    (b.cartanMatrix i j •
        Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
          (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
          (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0))
      (Sum.inl k) (Sum.inr l)

Tactic:
aesop

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

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero 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✝ : Fintype ι
i j : ↥b.support
k : ι
l : ↥b.support
⊢ ⁅Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)),
        Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
          (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
          (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)⁆
      (Sum.inr k) (Sum.inl l) =
    (b.cartanMatrix i j •
        Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
          (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
          (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0))
      (Sum.inr k) (Sum.inl l)

Tactic:
aesop

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

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✝⁷ : IsDomain R
inst✝⁶ : CharZero 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✝ : Fintype ι
i j : ↥b.support
k l : ι
⊢ ∀ x ∈ Finset.univ,
    x ∉ {k, l} →
      ((if P.root x = P.root ↑i + P.root l then
            Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) l) + 1)
          else 0) -
          if P.root k = P.root ↑i + P.root x then
            (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x l
          else 0) =
        0

Tactic:
aesop

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

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✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
h_lin_ind_y : LinearIndependent R ![P.root ↑i, P.root y]
hx' : chainBotCoeff (↑i) k = chainBotCoeff (↑i) x + 1
hy' : chainTopCoeff (↑i) k = chainTopCoeff (↑i) y + 1
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ x →
      (if P.root k = P.root ↑i + P.root b_1 then (↑(chainBotCoeff (↑i) b_1) + 1) * (↑(chainTopCoeff (↑i) k) + 1)
        else 0) =
        0

Tactic:
aesop

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

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✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
h_lin_ind_y : LinearIndependent R ![P.root ↑i, P.root y]
hx' : chainBotCoeff (↑i) k = chainBotCoeff (↑i) x + 1
hy' : chainTopCoeff (↑i) k = chainTopCoeff (↑i) y + 1
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ y →
      (if P.root k = P.root b_1 - P.root ↑i then (↑(chainTopCoeff (↑i) b_1) + 1) * (↑(chainBotCoeff (↑i) k) + 1)
        else 0) =
        0

Tactic:
aesop

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

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✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l x : ι
⊢ ¬(P.root x = P.root l - P.root ↑i ∧ k = i ∧ x = -↑i)

Tactic:
simp only [not_and]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l x : ι
⊢ P.root x = P.root l - P.root ↑i → k = i → ¬x = -↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

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✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
h₁ : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ k = i ∧ x = -↑i)
x : ι
⊢ ¬(P.root x = P.root ↑i + P.root l ∧ k = i ∧ x = ↑i)

Tactic:
simp only [not_and]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
h₁ : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ k = i ∧ x = -↑i)
x : ι
⊢ P.root x = P.root ↑i + P.root l → k = i → ¬x = ↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

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✝⁸ : IsDomain R
inst✝⁷ : CharZero 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✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hx : ∀ (x : ι), ¬(P.root x = P.root ↑i + P.root l ∧ P.root ↑i = P.root x - P.root ↑i)
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ i →
      (if True then
          ↑|b.cartanMatrix i b_1| *
            Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = ↑i then 1 else 0)
              (Matrix.of fun i' j ↦ if i' = -↑i then ↑|b.cartanMatrix i j| else 0)
              (Matrix.of fun i' j ↦ if P.root i' = P.root j - P.root ↑i then ↑(chainTopCoeff (↑i) j) + 1 else 0)
              (Sum.inl b_1) (Sum.inr l)
        else 0) =
        0

Tactic:
aesop

Goal state after: