mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) *
      ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₁ 1).subtype ((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ((evenOdd Q₂ 1).subtype ((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2))) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1 + Q₂ m.2)

Tactic:
Submodule.coe_subtype,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)) ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) *
      ((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))
          ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1 + Q₂ m.2)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) *
      (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1) + (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₂ m.2)

Tactic:
add_mul,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
m : M₁ × M₂
⊢ ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 *
        (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
          1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) +
      1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) *
        (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
          1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1) + (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₂ m.2)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
x y : 𝒜 ᵍ⊗[R] ℬ
⊢ ((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun i ↦ ↥(𝒜 i)) fun i ↦ ↥(ℬ i)) ≪≫ₗ (auxEquiv R ℬ 𝒜).symm) (x * y) =
    ((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun i ↦ ↥(𝒜 i)) fun i ↦ ↥(ℬ i)) ≪≫ₗ (auxEquiv R ℬ 𝒜).symm) x *
      ((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun i ↦ ↥(𝒜 i)) fun i ↦ ↥(ℬ i)) ≪≫ₗ (auxEquiv R ℬ 𝒜).symm) y

Tactic:
by
      dsimp
      simp_rw [auxEquiv_mul, gradedComm_gradedMul, LinearEquiv.symm_apply_eq,
        ← gradedComm_gradedMul, auxEquiv_mul, LinearEquiv.apply_symm_apply, gradedComm_gradedMul]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
set N' : Submodule R (ι → R) := N.map bM.equivFun.toLinearMap with hN'

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
⊢ N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v)

Tactic:
have : IsDomain R := .of_faithfulSMul R S

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ detMonoidHom ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    detMonoidHom (M.charmatrix ^ Fintype.card K)

Tactic:
apply congr_arg det

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix = M.charmatrix ^ Fintype.card K
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case pos
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 : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1,
      (-1) ^ (↑i + ↑x_1) * Pi.single (g x) (↑s) (g x_1) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
Fintype.sum_eq_single x fun y hxy => ?_,

Goal state after:
case pos
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 : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * Pi.single (g x) (↑s) (g x) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

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 : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1,
      (-1) ^ (↑i + ↑x_1) * Pi.single (g x) (↑s) (g x_1) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
y : Fin (k + 1)
hxy : y ≠ x
⊢ (-1) ^ (↑i + ↑y) * Pi.single (g x) (↑s) (g y) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove y.succAbove).det =
    0
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃+ (ι → ℤ))

Tactic:
by
  convert! submodule_toAddSubgroup_index_ne_zero_iff (N := AddSubgroup.toIntSubmodule H) using 1
  exact ⟨fun ⟨e⟩ ↦ ⟨e.toIntLinearEquiv⟩, fun ⟨e⟩ ↦ ⟨e.toAddEquiv⟩⟩

Goal state after:
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
inst✝ : DecidableEq m
A : Matrix m n R
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
transpose_isTotallyUnimodular_iff

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
transpose_isTotallyUnimodular_iff

Goal state after:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ LinearIndependent 𝔽 (↑M).col

Tactic:
apply linearIndependent_iff_card_eq_finrank_span.2

Goal state after:
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M).col)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ reduce A = reduce (reduceStep A)

Tactic:
reduce,

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then T ^ (-(↑A 0 1 / ↑A 1 1)) • A else T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    reduce (reduceStep A)
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
r : ℕ
⊢ A.den ∣ r ↔ ∀ (i : m) (j : n), (A i j).den ∣ r

Tactic:
by
  simp [Matrix.den]

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v j‖ ≤ 0

Tactic:
refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v i‖ ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: case inr
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Tactic:
have h_nz : v i ≠ 0 := by
      contrapose h_nz
      ext j
      rw [Pi.zero_apply, ← norm_le_zero_iff]
      refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
      exact norm_le_zero_iff.mpr h_nz

Goal state after:
case inr
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
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
inst✝ : IsCancelAdd R
⊢ IsRightRegular A ↔ A.Nonsingular

Tactic:
rw [isRightRegular_iff_vecMul_injective, vecMul_injective_iff, linearIndependent_row_iff]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
⊢ 0 ∈ s

Tactic:
exact s.zero_mem

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
⊢ IsMulCommutative ↥(lineStab p.submodule)

Tactic:
← Projectivization.mk_rep p,

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
⊢ IsMulCommutative ↥(lineStab (Projectivization.mk F p.rep ⋯).submodule)
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 : P.root k ≠ -P.root i
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
⊢ P.root (-k) + P.root j = -(P.root k - P.root j)

Tactic:
simp [neg_add_eq_sub]

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
⊢ ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j)

Tactic:
by rw [Ring.lie_def]

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
⊢ -(h j * e i - e i * h j) * ω b = -⁅h j, e i⁆ * ω b

Tactic:
by rw [Ring.lie_def]

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
⊢ IsNilpotent (f i)

Tactic:
obtain ⟨n, hn⟩ := isNilpotent_e i
  suffices (ω b) * (f i ^ n) = 0 from ⟨n, by simpa [← mul_assoc] using congr_arg (ω b * ·) this⟩
  suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn]
  clear hn
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]

Goal state after:
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
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)
l : ↥b.support
hl : χ (h' l) ≠ 0
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
i : ↥b.support
hw : w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ (h' l)) (h' l)
⊢ w (Sum.inl i) = 0

Tactic:
aux (Sum.elim 0 (P.pairingIn ℤ · l)) (h' l) (h_eq_diagonal l)

Goal state after:
ι : 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
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)
l : ↥b.support
hl : χ (h' l) ≠ 0
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
i : ↥b.support
hw : ∃ k, diagonal (((0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑l)) - χ (h' l) • 1) ^ k) *ᵥ w = 0
⊢ w (Sum.inl i) = 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
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k ij : ι
hij : ij ∈ {long P, short P}
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k ij

Tactic:
rcases hij with rfl | rfl

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.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k : ι
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k (long P)

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.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k : ι
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k (short P)
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) <;> simp [ω, u, Pi.single_apply, one_apply]

Goal state after:
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
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∃ j, u j ∈ U

Tactic:
revert U

Goal state after:
ι : 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
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U