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

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
f : Fin k → m ⊕ m'
g : Fin k → n
hf : Function.Injective f
⊢ Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
hg

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
f : Fin k → m ⊕ m'
g : Fin k → n
hf : Function.Injective f
hg : Function.Injective g
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition

Goal state before:
pp: m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = #{i | cert.pivot i ≠ ⊤}

Tactic:
rw [← cert.isPivotedBy.rank_eq,
    cert.L.rank_mul_eq_right_of_isLowerTriangular _ cert.L_lowerTriangular cert.L_diag_ne_zero]
  exact (A.rank_submatrix cert.σ (.refl _)).symm

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

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
⊢ ∃ j s, replicateRow m' 0 x✝ = Pi.single j ↑s

Tactic:
inhabit n

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
⊢ ∃ j s, replicateRow m' 0 x✝ = Pi.single j ↑s
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B * (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ = ↑(Fintype.card (m × n)) • 1

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩

Goal state after:
case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B * (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ * kroneckerMap (fun x1 x2 ↦ x1 * x2) A B = ↑(Fintype.card (m × n)) • 1

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩

Goal state after:
case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ * kroneckerMap (fun x1 x2 ↦ x1 * x2) A B) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
have : Infinite (ℙ k V) := by rwa [this]

Goal state after:
case inl.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this✝ : Infinite (ℙ k V) ↔ Infinite V
this : Infinite (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬Independent f

Tactic:
by
  rw [dependent_iff, independent_iff]

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

Goal state before:
pp: case refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.finrank K ↥(Subspace.submodule M) ≤ 2

Tactic:
· exact Module.finrank_le_of_rank_le hM1

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
v✝ : V
h✝ : v✝ ≠ 0
⊢ Projectivization.mk K v✝ h✝ ∈ projectivization s ↔ (Projectivization.mk K v✝ h✝).submodule ≤ s

Tactic:
mk_mem_projectivization_iff,

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
v✝ : V
h✝ : v✝ ≠ 0
⊢ v✝ ∈ s ↔ (Projectivization.mk K v✝ h✝).submodule ≤ s
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
g : SpecialLinearGroup R V
a : R
v : V
⊢ g • a • v = a • g • v

Tactic:
by
    simp [SpecialLinearGroup.smul_def]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
⊢ PSLAction.toPermHom g = 1 → g = 1

Tactic:
hg

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : PSLAction.toPermHom g = 1
⊢ g = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g

Tactic:
· simp only [IsUnit.unit_spec, ← (mem_center_iff.mp g.prop).choose_spec.2]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r

Tactic:
replace hR := not_subsingleton_iff_nontrivial.mp hR

Goal state after:
case pos
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hV : Subsingleton V
hR : Nontrivial R
⊢ 1 = r
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r

Tactic:
not_subsingleton_iff_nontrivial

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
⊢ ⟨⋯.unit, ⋯⟩ = r
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
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : ∀ (x : V), H.choose • x = ↑↑r • x
x : V
⊢ ⋯.choose • x = ↑↑r • x

Tactic:
this x

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : ∀ (x : V), H.choose • x = ↑↑r • x
x : V
⊢ ↑↑r • x = ↑↑r • x
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = ⟨⋯.unit * ⋯.unit, ⋯⟩

Tactic:
not_subsingleton_iff_nontrivial

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
⊢ ⟨⋯.unit, ⋯⟩ = ⟨⋯.unit * ⋯.unit, ⋯⟩
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑↑g = ⋯.choose • LinearMap.id

Tactic:
not_subsingleton_iff_nontrivial

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Nontrivial V
⊢ ↑↑↑g = ⋯.choose • LinearMap.id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : ¬Subsingleton V
hι : ¬IsEmpty ι
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)

Tactic:
not_subsingleton_iff_nontrivial

Goal state after:
case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : Module R M
Q : QuadraticForm R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
⊢ IsGreatest {r | ∃ V, Module.finrank R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef} (sigPos Q)

Tactic:
by
  classical
  refine ⟨(mem_filter.mp <| max'_mem _ _).2, ?_⟩
  rintro _ ⟨V, rfl, hV⟩
  apply le_max'
  rw [mem_filter, mem_Iic]
  exact ⟨V.finrank_le, V, rfl, hV⟩

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

Tactic:
comp_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.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) (h x✝¹) x✝ =
    (⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i) x✝¹ x✝
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
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ LinearIndependent ℤ fun i j ↦ P.pairingIn ℤ ↑j ↑i

Tactic:
apply b.cartanMatrix.transpose.linearIndependent_rows_of_det_ne_zero

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✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ b.cartanMatrixᵀ.det ≠ 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: 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

Tactic:
rw [← neg_mem_iff]

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
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.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
rw [pairingIn_eq_add_of_root_eq_add (shortAddLongRoot_eq P)]

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

Goal state before:
pp: case h.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
this : (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0
⊢ (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0

pp: case h.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 : ι
x : ℕ
hk₁ : P.root k = P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i
⊢ (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0

Tactic:
· assumption

Goal state after:
case h.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 : ι
x : ℕ
hk₁ : P.root k = P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i
⊢ (e i ^ (chainTopCoeff (↑i) j + 1)).col (Sum.inr j) = 0
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.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 * P.pairingIn ℤ i (long P)

Tactic:
by
  suffices P.pairing i (threeShortAddTwoLong P) =
      P.pairing i (short P) + 2 * P.pairing i (long P) from
    algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
  have : Fintype ι := Fintype.ofFinite ι
  have B := (P.posRootForm ℤ).toInvariantForm
  apply mul_right_cancel₀ (B.ne_zero <| threeShortAddTwoLong P)
  calc P.pairing i (threeShortAddTwoLong P) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddTwoLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * (2 * B.form (P.root i) (longRoot P)) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          2 * P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 2 * P.pairing i (long P)) *
          B.form (threeShortAddTwoLongRoot P) (threeShortAddTwoLongRoot P) := ?_
  · rw [B.two_mul_apply_root_root]
  · simp only [threeShortAddTwoLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]; ring
  · rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, long_eq_three_mul_short]; ring
  · rw [threeShortAddTwoLongRoot_longRoot]; ring

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
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
⊢ P.root k + P.root i - P.root j = P.root m + P.root i

Tactic:
← h₂

Goal state after:
ι : 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
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
⊢ P.root k + P.root i - P.root j = P.root k - P.root j + P.root i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inr.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 : ι
hij : i ≠ j
⊢ d j ≠ d i

Tactic:
exact hd₁ <| by simp [hij.symm]

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.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
_i✝ : P.EmbeddedG2
_i : Nonempty ι
⊢ b.support.card = 2

Tactic:
rw [← Fintype.card_fin 2, ← Module.finrank_eq_card_basis (EmbeddedG2.basis P),
    Module.finrank_eq_card_basis b.toWeightBasis, Fintype.card_coe]

Goal state after: