mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ (-1) ^ (ixb * iya + (ixb * iza + iyb * iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    (-1) ^ (iyb * iza + ixb * (iya + iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))

Tactic:
mul_add

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ (-1) ^ (ixb * iya + (ixb * iza + iyb * iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    (-1) ^ (iyb * iza + (ixb * iya + ixb * iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case e'_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
this : ∀ (r : R) (x : M ⧸ L.goursatFst), e (r • x) = r • e x
e_1✝ :
  AddSubgroup ((M ⧸ L.goursatFst) × N ⧸ L.goursatSnd) =
    AddSubgroup ((M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
v : (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd
⊢ v.2 = ↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } v.1 ↔
    v ∈ e.toAddMonoidHom.graph

Tactic:
Eq.comm

Goal state after:
case e'_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
this : ∀ (r : R) (x : M ⧸ L.goursatFst), e (r • x) = r • e x
e_1✝ :
  AddSubgroup ((M ⧸ L.goursatFst) × N ⧸ L.goursatSnd) =
    AddSubgroup ((M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
v : (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd
⊢ ↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } v.1 = v.2 ↔
    v ∈ e.toAddMonoidHom.graph
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i

Tactic:
let : Fintype ι' := .ofFinite ι'

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
h : A i ≠ 0
⊢ ∃ c, A.IsLeadingEntry i c

Tactic:
obtain ⟨c, hc, hmin⟩ := wellFounded_lt.has_min {j | A i j ≠ 0} <| Function.ne_iff.mp h

Goal state after:
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
h : A i ≠ 0
c : n
hc : c ∈ {j | A i j ≠ 0}
hmin : ∀ x ∈ {j | A i j ≠ 0}, ¬x < c
⊢ ∃ c, A.IsLeadingEntry i c
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
by
  rw [isTotallyUnimodular_iff]
  constructor
  · intro hA ι _ _ f g
    specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
    rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA
  · intro hA k f g
    specialize hA (ULift (Fin k)) (f ∘ Equiv.ulift) (g ∘ Equiv.ulift)
    rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
| ((-1) ^ (↑i₀ + ↑j₀) * ∑ c, M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
    ∑ i, ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det

Tactic:
enter [

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
| ((-1) ^ (↑i₀ + ↑j₀) * ∑ c, M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
    ∑ i, ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
⊢ IsUnit (↑M)ᵀ.det

Tactic:
have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b

Goal state after:
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this : Invertible ((Pi.basisFun 𝔽 (Fin n)).toMatrix ⇑b)
⊢ IsUnit (↑M)ᵀ.det
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
⊢ T ^ (-n) • A ∈ reps m

Tactic:
have h3 := Int.emod_lt_abs (A.1 0 1) hd

Goal state after:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : ↑A 0 1 % ↑A 1 1 < |↑A 1 1|
⊢ T ^ (-n) • A ∈ reps m
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ reduce A ∈ reps m

Tactic:
simp only [reps, Fin.isValue, reduce_of_not_pos h h1, Int.ediv_neg, neg_neg, smul_def, ←
        mul_assoc, S_mul_S_eq, neg_mul, one_mul, coe_T_zpow, mul_neg, cons_mul, Nat.succ_eq_add_one,
        Nat.reduceAdd, empty_mul, Equiv.symm_apply_apply, neg_of, neg_cons, neg_empty,
        Set.mem_ofPred_eq, of_apply, cons_val', Pi.neg_apply, vecMul, cons_dotProduct, vecHead,
        vecTail, Function.comp_apply, Fin.succ_zero_eq_one, h, mul_zero, dotProduct_of_isEmpty,
        add_zero, zero_mul, neg_zero, empty_val', cons_val_fin_one, cons_val_one, cons_val_zero,
        lt_neg, neg_add_rev, zero_add, le_add_neg_iff_add_le, ← le_neg, abs_neg, true_and]

Goal state after:
case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0 ∧ -↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ -↑A 0 1 ∧ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
⊢ Fintype.card n • (1 ᵥ* 1 ⬝ᵥ 1) = ↑(Fintype.card n) ^ 2

Tactic:
simp [dotProduct, pow_two]

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

Goal state before:
pp: case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ diagonal A.diag i i = A i i

Tactic:
rw [diagonal_apply_eq, diag]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
⊢ ∃ p, 0 < p.length

Tactic:
obtain ⟨p, hp_pos⟩ := hA.connected j i

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
p : Path j i
hp_pos : 0 < p.length
⊢ ∃ p, 0 < p.length
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
⊢ A = 1

Tactic:
have := Int.mul_eq_one_iff_eq_one_or_neg_one.mp (A_c_eq_zero a1)
  ext i j
  fin_cases i <;> fin_cases j <;> aesop

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ swap R i j * swap R i j = 1

Tactic:
simp only [swap]

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
⊢ a = b

Tactic:
let P (r : ℕ) : Prop := ∀ f g : Fin r → n, (A.submatrix f g).IsDetpBalanced a b

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
⊢ a = b
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂) = Q₁.tmul Q₂

Tactic:
by
  refine (QuadraticMap.associated_rightInverse R).injective ?_
  ext m₁ m₂ m₁' m₂'
  simp only [associated_tmul, QuadraticMap.associated_comp]
  exact mul_comm _ _

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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
⊢ False

Tactic:
replace h₂ : P.root k = P.root i + P.root j := by rwa [contra, sub_eq_iff_eq_add] at h₂
    replace h₃ : P.root n = 2 • P.root i := by rw [h₃, h₂]; abel
    exact P.nsmul_notMem_range_root ⟨_, h₃⟩

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ↥b.support
⊢ ⁅e i, ⁅f i, u j⁆⁆ = |b.cartanMatrix i j| • u i

Tactic:
ext (k | k)

Goal state after:
case 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 ι
i j k : ↥b.support
⊢ ⁅e i, ⁅f i, u j⁆⁆ (Sum.inl k) = (|b.cartanMatrix i j| • u i) (Sum.inl k)

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✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ↥b.support
k : ι
⊢ ⁅e i, ⁅f i, u j⁆⁆ (Sum.inr k) = (|b.cartanMatrix i j| • u i) (Sum.inr k)
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ↥b.support
⊢ ⁅e i, u j⁆ = |b.cartanMatrix i j| • v b ↑i

Tactic:
ext (k | k)

Goal state after:
case 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 ι
i j k : ↥b.support
⊢ ⁅e i, u j⁆ (Sum.inl k) = (|b.cartanMatrix i j| • v b ↑i) (Sum.inl k)

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✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ↥b.support
k : ι
⊢ ⁅e i, u j⁆ (Sum.inr k) = (|b.cartanMatrix i j| • v b ↑i) (Sum.inr k)
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * ⁅x, y⁆ * ω b = ⁅ω b * x * ω b, ω b * y * ω b⁆

Tactic:
simp only [Ring.lie_def]

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * (x * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
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
⊢ P.pairing (long P) (short P) = -3

Tactic:
rw [← P.algebraMap_pairingIn ℤ, pairingIn_long_short]
  simp

Goal state after:
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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
⊢ (e i ^ 2).col (Sum.inl j) = 0

Tactic:
ext (k | k)

Goal state after:
case inl
ι : 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j k : ↥b.support
⊢ (e i ^ 2).col (Sum.inl j) (Sum.inl k) = 0 (Sum.inl k)

case inr
ι : 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
⊢ (e i ^ 2).col (Sum.inl j) (Sum.inr k) = 0 (Sum.inr 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
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ ∃ c, ∑ i, c i • ![shortRoot P, longRoot P] i = x

Tactic:
← Fintype.linearCombination_apply

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
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ ∃ c, (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) c = x
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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : j = -↑i
⊢ (e i).col (Sum.inr j) = u i

Tactic:
ext (k | k)

Goal state after:
case inl
ι : 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : j = -↑i
k : ↥b.support
⊢ (e i).col (Sum.inr j) (Sum.inl k) = u i (Sum.inl k)

case inr
ι : 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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : j = -↑i
k : ι
⊢ (e i).col (Sum.inr j) (Sum.inr k) = u i (Sum.inr k)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : 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 ι
B : P.InvariantForm
⊢ 2 * ((B.form (P.root i)) (shortRoot P) + (B.form (P.root i)) (longRoot P)) =
    2 * (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
mul_add

Goal state after:
case calc_2
ι : 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 ι
B : P.InvariantForm
⊢ 2 * (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P)