mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : Matrix.SpecialLinearGroup ι F
H : Subgroup (Matrix.SpecialLinearGroup ι F)
x : Matrix.SpecialLinearGroup ι F ⧸ Subgroup.center (Matrix.SpecialLinearGroup ι F)
x✝ : ∃ x_1 ∈ H, ↑x_1 = (↑g)⁻¹ * x * ↑g
a : Matrix.SpecialLinearGroup ι F
ha : a ∈ H
hx : ↑a = (↑g)⁻¹ * x * ↑g
⊢ g⁻¹ * (g * a * g⁻¹) * g ∈ H

Tactic:
simp [mul_assoc, ha]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
⊢ ↑(A * B) • w = ↑(B * A) • w

Tactic:
obtain ⟨β, hβ⟩ := Submodule.mem_span_singleton.mp (hB w)

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ ↑(A * B) • w = ↑(B * A) • w
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝¹ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this✝ : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this✝
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this : (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0
⊢ D'.rep = D'.rep + (b.repr D'.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • ↑⟨D.rep, hD_mem⟩

Tactic:
simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inr
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)
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
this : ↑↑r = 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Q m' + (Q.polarBilin (m - m')) m' = Q m'

Tactic:
simp [(hN hmm').2]

Goal state after:
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
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank R ↥V = Module.finrank R ↥V ∧ (QuadraticMap.restrict Q V).PosDef

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
this : P.pairingIn ℤ l k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k
⊢ P.pairingIn ℤ i k ≤ -2

Tactic:
linarith

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

Goal state before:
pp: case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ 1 - P.pairing j i = (P.coroot' i) (P.root k + P.root i - P.root j)

Tactic:
simp only [map_sub, map_add, LinearMap.flip_apply, root_coroot_eq_pairing, hki, pairing_same,
      sub_left_inj]

Goal state after:
case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ 1 = -1 + 2
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
aux₁ : LinearIndependent R ![P.root j, P.root i]
aux₂ : chainBotCoeff j i + chainTopCoeff j i ≤ 2
⊢ P.root i + 1 • P.root j ∈ Set.range ⇑P.root

Tactic:
one_smul

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
aux₁ : LinearIndependent R ![P.root j, P.root i]
aux₂ : chainBotCoeff j i + chainTopCoeff j i ≤ 2
⊢ P.root i + P.root j ∈ Set.range ⇑P.root
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
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
hx :
  x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![0, 1] ∨
    x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![0, -1] ∨
      x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![1, 0] ∨
        x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![-1, 0] ∨
          x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![1, 1] ∨
            x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![-1, -1] ∨
              x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![2, 1] ∨
                x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![-2, -1] ∨
                  x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![3, 1] ∨
                    x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![-3, -1] ∨
                      x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![3, 2] ∨
                        x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) ![-3, -2]
⊢ ∃ c, (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) c = x

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
⊢ LinearIndependent R ![P.root ↑i, P.root y]

Tactic:
rw [← add_eq_of_eq_sub hy, add_comm]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
⊢ LinearIndependent R ![P.root ↑i, P.root ↑i + P.root k]
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
y : ι
hy : P.root k = P.root y - P.root ↑i
h₁ : chainBotCoeff (↑i) k = 0
⊢ LinearIndependent R ![P.root ↑i, P.root y]

Tactic:
rw [← add_eq_of_eq_sub hy, add_comm]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
y : ι
hy : P.root k = P.root y - P.root ↑i
h₁ : chainBotCoeff (↑i) k = 0
⊢ LinearIndependent R ![P.root ↑i, P.root ↑i + P.root k]
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
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
this : 2 ≤ P.pairingIn ℤ j k
⊢ P.pairingIn ℤ j k = 2

Tactic:
by have := IsNotG2.pairingIn_mem_zero_one_two (P := P) j k; grind

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

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

Tactic:
tauto

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

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

Tactic:
tauto

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this : P.pairing (long P) (short P) = -3
h : short P = long P
⊢ False

Tactic:
norm_num [h] at this

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

Goal state before:
pp: case refine_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
inst✝ : P.IsIrreducible
this : P.pairing (long P) (short P) = -3
h : short P = (P.reflectionPerm (long P)) (long P)
⊢ False

Tactic:
norm_num [h] at this

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
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥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)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
⊢ d ∈ span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i)) ∧ (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ↔
    (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ d ∈ span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))

Tactic:
tauto

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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : genWeightSpace (↥U) 0 = ⊤
⊢ U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)

Tactic:
simp [this]

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
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ι
hk : k ≠ ↑i
⊢ ¬k = ↑i

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
⊢ cartanSubalgebra' b = LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range fun i ↦ ⟨h i, ⋯⟩)

Tactic:
by
    rw [cartanSubalgebra', cartanSubalgebra_eq_lieSpan, ← LieSubalgebra.comap_lieSpan_range_eq]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x

pp: case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ (B x) x

Tactic:
· rw [star_dotProduct_toMatrix₂_mulVec]
    exact h _

Goal state after:
case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ (B x) x
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case isTrue
ι : 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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root i + P.root k ∈ range ⇑P.root
hjk_mem : P.root (-k) + P.root j ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
h₁' : P.root (-k) - P.root i = P.root (-l)
h₂' : P.root (-k) + P.root j = P.root (-m)
h₃' : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff j (-k) = 0
aux₁ : ¬(chainBotCoeff i m = 1 ∧ chainBotCoeff j (-l) = 0)
aux₂ : ¬(chainBotCoeff j (-l) = 1 ∧ chainBotCoeff i m = 0)
h✝ : P.pairingIn ℤ i m = 0
this : chainBotCoeff i m = 1
⊢ chainBotCoeff i m = 0 ∨ chainBotCoeff i m = 1

Tactic:
simp [this]

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

Goal state before:
pp: case isFalse
ι : 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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root i + P.root k ∈ range ⇑P.root
hjk_mem : P.root (-k) + P.root j ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
h₁' : P.root (-k) - P.root i = P.root (-l)
h₂' : P.root (-k) + P.root j = P.root (-m)
h₃' : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff j (-k) = 0
aux₁ : ¬(chainBotCoeff i m = 1 ∧ chainBotCoeff j (-l) = 0)
aux₂ : ¬(chainBotCoeff j (-l) = 1 ∧ chainBotCoeff i m = 0)
h✝ : ¬P.pairingIn ℤ i m = 0
this : chainBotCoeff i m = 0
⊢ chainBotCoeff i m = 0 ∨ chainBotCoeff i m = 1

Tactic:
simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this✝¹ :
  finrank K ↥(↑f).fixedSubmodule + finrank K ↥(↑e).fixedSubmodule ≤
    finrank K ↥((↑f).fixedSubmodule ⊔ (↑e).fixedSubmodule) + finrank K ↥(↑(f * e)).fixedSubmodule
this✝ : finrank K V ≤ 1 + finrank K ↥(↑f).fixedSubmodule
this : finrank K ↥((↑f).fixedSubmodule ⊔ (↑e).fixedSubmodule) ≤ finrank K V
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(f * e)).fixedSubmodule

Tactic:
linarith

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this✝¹ :
  finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule
this✝ : finrank K V ≤ 1 + finrank K ↥(↑f).fixedSubmodule
this : finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) ≤ finrank K V
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
linarith

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
⊢ r a₁ a ∧ r a₂ a

Tactic:
tauto

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ u - e u ∈ ker f

Tactic:
apply hf

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e f✝ : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
⊢ u - e u ∈ (↑e).fixedSubmodule ⊔ K ∙ (e u - u)