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

Goal state before:
pp: case mem
ι : 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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x u : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hu : u ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) u ∈ lieAlgebra b

Tactic:
obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
      simpa only [mem_union, mem_range, or_assoc] using hu

Goal state after:
case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : h i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (h i) ∈ lieAlgebra b

case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : e i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (e i) ∈ lieAlgebra b

case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : f i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (f i) ∈ lieAlgebra b
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 : ι
⊢ ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)

Tactic:
simp only [h, e, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
      Matrix.fromBlocks_apply₁₂, Matrix.zero_apply, zero_mul, add_zero, Finset.sum_const_zero]

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

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
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
i : ι
⊢ P.pairing i (twoShortAddLong P) = 2 * P.pairing i (short P) + 3 * P.pairing i (long P)

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
⊢ P.pairing i (twoShortAddLong P) = 2 * P.pairing i (short P) + 3 * P.pairing i (long P)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
⊢ IsNilpotent (e i)

Tactic:
classical
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : IsAddTorsionFree M := .of_isTorsionFree R M
  let := P.indexNeg
  rw [Matrix.isNilpotent_iff_forall_col]
  have case_inl (j : b.support) : (e i ^ 2).col (Sum.inl j) = 0 := by
    ext (k | k)
    · simp [e, sq, ne_neg P i, -indexNeg_neg]
    · have aux : ∀ x : ι, x ∈ Finset.univ → ¬ (x = i ∧ P.root k = P.root i + P.root x) := by
        suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
        exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩
      simp [e, sq, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux]
  rintro (j | j)
  · exact ⟨2, case_inl j⟩
  · by_cases hij : j = -i
    · use 2 + 1
      replace hij : (e i).col (Sum.inr j) = u i := by
        ext (k | k)
        · simp [e, -indexNeg_neg, Pi.single_apply, hij]
        · have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k]
          simp [e, -indexNeg_neg, hk]
      rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]
      simp [hij, case_inl i]
    use P.chainTopCoeff i j + 1
    rcases isNilpotent_e_aux i (P.chainTopCoeff i j + 1) hij with this | ⟨k, x, hk₁, -⟩
    · assumption
    exfalso
    replace hk₁ : P.root j + (P.chainTopCoeff i j + 1) • P.root i ∈ range P.root := ⟨k, hk₁⟩
    have hij' : LinearIndependent R ![P.root i, P.root j] := by
      apply IsReduced.linearIndependent P ?_ ?_
      · rintro rfl
        apply P.nsmul_notMem_range_root (n := P.chainTopCoeff i i + 2) (i := i)
        convert! hk₁ using 1
        module
      · contrapose hij
        rw [root_eq_neg_iff] at hij
        rw [hij, ← indexNeg_neg, neg_neg]
    rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁
    lia

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
i : ι
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
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
i : ι
⊢ P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
⊢ P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ↥b.support
l : ι
⊢ ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)

Tactic:
have h₁ (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra

Goal state after:
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 : ↥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)
⊢ ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
⊢ (w (Sum.inr i))⁻¹ • w = v b i

Tactic:
ext (j | j)

Goal state after:
case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ↥b.support
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)

case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ι
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)
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
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
h₁ : P.IsOrthogonal i (short P)
h₂ : P.IsOrthogonal i (long P)
⊢ False

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
h₁ : P.IsOrthogonal i (short P)
h₂ : P.IsOrthogonal i (long P)
this : Fintype ι
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case 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
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
⊢ ⁅e i, f j⁆ᵀ (Sum.inr ↑j) (Sum.inl k) = 0 (Sum.inl k)

Tactic:
Matrix.transpose_apply,

Goal state after:
case 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
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr ↑j) = 0 (Sum.inl k)
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
inst✝ : P.IsIrreducible
⊢ RightInverse (fun x ↦ Exists.choose ⋯) fun i ↦ ⟨P.root i, ⋯⟩

Tactic:
rintro ⟨x, hx⟩

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
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
x : M
hx : x ∈ (allRoots P).toFinset
⊢ (fun i ↦ ⟨P.root i, ⋯⟩) ((fun x ↦ Exists.choose ⋯) ⟨x, hx⟩) = ⟨x, hx⟩
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i : ↥b.support
⊢ ω b *ᵥ u i = u i

Tactic:
ext (j | j)

Goal state after:
case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i j : ↥b.support
⊢ (ω b *ᵥ u i) (Sum.inl j) = u i (Sum.inl j)

case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i : ↥b.support
j : ι
⊢ (ω b *ᵥ u i) (Sum.inr j) = u i (Sum.inr j)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i : ι
⊢ ω b *ᵥ v b i = v b (-i)

Tactic:
ext (j | j)

Goal state after:
case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i : ι
j : ↥b.support
⊢ (ω b *ᵥ v b i) (Sum.inl j) = v b (-i) (Sum.inl j)

case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i j : ι
⊢ (ω b *ᵥ v b i) (Sum.inr j) = v b (-i) (Sum.inr j)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case 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
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-↑i)) (Sum.inl k) = 0 (Sum.inl k)

Tactic:
Matrix.transpose_apply,

Goal state after:
case 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
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr (-↑i)) = 0 (Sum.inl k)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case 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 : ↥b.support
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ ⁅e i, f j⁆ᵀ (Sum.inr (-↑i)) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
Matrix.transpose_apply,

Goal state after:
case 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 : ↥b.support
hij : i ≠ j
this : InvolutiveNeg ι := P.indexNeg
k : ι
aux : ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = (⁅e i, f j⁆ * ω b) (Sum.inr k) (Sum.inr ↑i)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr (-↑i)) = 0 (Sum.inr k)
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: case dvd_two_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hSB : B.IsSymm
y : M
hx : B.IsReflective x
hy : B.IsReflective y
⊢ ∀ (y_1 : M), (B ((reflection ⋯) y)) ((reflection ⋯) y) ∣ 2 * (B ((reflection ⋯) y)) y_1

Tactic:
· intro z
    have hz : Module.reflection (coroot_apply_self B hx)
        (Module.reflection (coroot_apply_self B hx) z) = z := by
      exact (LinearEquiv.eq_symm_apply (Module.reflection (coroot_apply_self B hx))).mp rfl
    rw [← hz, isOrthogonal_reflection B hx hSB,
      isOrthogonal_reflection B hx hSB]
    exact hy.2 _

Goal state after: