mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j = chainTopCoeff i j
⊢ chainBotCoeff i j = if chainBotCoeff i j = chainTopCoeff i j then 1 else 0

Tactic:
aux₄,

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j = chainTopCoeff i j
⊢ chainTopCoeff i j = if True then 1 else 0
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j ≠ chainTopCoeff i j
⊢ chainBotCoeff i j = if chainBotCoeff i j = chainTopCoeff i j then 1 else 0

Tactic:
aux₄,

Goal state after:
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
aux₄ : chainBotCoeff i j ≠ chainTopCoeff i j
⊢ chainBotCoeff i j = if False then 1 else 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case pos
ι : 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
⊢ ∃ n, (e i ^ n).col (Sum.inr j) = 0

Tactic:
use 2 + 1
      replace hij : (e i).col (Sum.inr j) = u i := by
        ext (k | k)
        · simp [e, -indexNeg_neg, Pi.single_apply, hij]
        · have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k]
          simp [e, -indexNeg_neg, hk]
      rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]
      simp [hij, case_inl i]

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
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)

Tactic:
have aux₀ : P.pairingIn ℤ j i = - P.pairingIn ℤ m i := by
    suffices P.pairing j i = - P.pairing m i from
      algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_neg]
    replace hki : P.pairing k i = 0 := by rw [← P.algebraMap_pairingIn ℤ, hki, map_zero]
    simp only [← root_coroot_eq_pairing, ← h₂]
    simp [hki]

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
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)
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
w : ↥b.support ⊕ ι → K
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)
hw₀ : genWeightSpace (↥b.support ⊕ ι → K) χ ≠ ⊥
χ' : ↥H →ₗ[K] K := Weight.toLinear K (↥H) (↥b.support ⊕ ι → K) { toFun := χ, genWeightSpace_ne_bot' := hw₀ }
hχ : χ' = 0
⊢ χ = 0

Tactic:
ext x

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
w : ↥b.support ⊕ ι → K
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)
hw₀ : genWeightSpace (↥b.support ⊕ ι → K) χ ≠ ⊥
χ' : ↥H →ₗ[K] K := Weight.toLinear K (↥H) (↥b.support ⊕ ι → K) { toFun := χ, genWeightSpace_ne_bot' := hw₀ }
hχ : χ' = 0
x : ↥H
⊢ χ x = 0 x
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, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b

Tactic:
simp_rw [cartanSubalgebra, LieSubalgebra.mem_mk_iff', diagonal_elim_mem_span_h_iff]

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
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, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ d ∈ span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
⊢ B.form (P.root i) = 0

Tactic:
ext x

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
x : M
⊢ (B.form (P.root i)) x = 0 x
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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
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✝² : InvolutiveNeg ι := P.indexNeg
this✝¹ : P.IsNotG2
this✝ : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
this : P.pairingIn ℤ l j = P.pairingIn ℤ i j + P.pairingIn ℤ k j
⊢ -P.pairingIn ℤ i j < P.pairingIn ℤ k j

Tactic:
have := zero_le_pairingIn_of_root_sub_mem hlj_mem

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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
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✝³ : InvolutiveNeg ι := P.indexNeg
this✝² : P.IsNotG2
this✝¹ : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
this✝ : P.pairingIn ℤ l j = P.pairingIn ℤ i j + P.pairingIn ℤ k j
this : 0 ≤ P.pairingIn ℤ l j
⊢ -P.pairingIn ℤ i j < P.pairingIn ℤ k j
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

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

Tactic:
rw [Int.cast_smul_eq_zsmul, ← lie_e_lie_f_apply l' 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.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 : ↥b.support
hj : u j ∈ U
k l l' : ↥b.support
hl₁ : u l ∈ U
hl₂ : b.cartanMatrix l' l ≠ 0
⊢ ⁅e l', ⁅f l', u l⁆⁆ ∈ U
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 : ↥b.support
hj : u j ∈ U
k l l' : ↥b.support
hl₁ : u l ∈ U
hl₂ : b.cartanMatrix l' l ≠ 0
e' : ↥(lieAlgebra b) := ⟨e l', ⋯⟩
f' : ↥(lieAlgebra b) := ⟨f l', ⋯⟩
⊢ ⁅e l', ⁅f l', u l⁆⁆ ∈ U

Tactic:
change ⁅e', ⁅f', u l⁆⁆ ∈ 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
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 : ↥b.support
hj : u j ∈ U
k l l' : ↥b.support
hl₁ : u l ∈ U
hl₂ : b.cartanMatrix l' l ≠ 0
e' : ↥(lieAlgebra b) := ⟨e l', ⋯⟩
f' : ↥(lieAlgebra b) := ⟨f l', ⋯⟩
⊢ ⁅e', ⁅f', u l⁆⁆ ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₀
ι : 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 : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
⊢ ∀ (i : ι),
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b i ∈ U) →
      ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)},
        (∀ (k : ↥b.support), u k ∈ U) → v b ((P.reflectionPerm i) i) ∈ U

Tactic:
intro j h U hU

Goal state after:
case h₀
ι : 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 : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j✝ j : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : ∀ (k : ↥b.support), u k ∈ U
⊢ v b ((P.reflectionPerm j) j) ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
z : M
⊢ 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z - 2 * (B z) ↑y =
    2 * (B z) ((IsReflective.coroot B ⋯) ↑y • ↑x) - 2 * (B z) ↑y

Tactic:
sub_left_inj

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
z : M
⊢ 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z = 2 * (B z) ((IsReflective.coroot B ⋯) ↑y • ↑x)
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
F G : SymmetricAlgebra R M →ₐ[R] A
h : ↑F ∘ₗ ι R M = ↑G ∘ₗ ι R M
⊢ F = G

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
F G : SymmetricAlgebra R M →ₐ[R] A
h : ↑F ∘ₗ ι R M = ↑G ∘ₗ ι R M
x : M
⊢ ((F.comp (RingCon.mkₐ R (symRingCon R M))).toLinearMap ∘ₗ TensorAlgebra.ι R) x =
    ((G.comp (RingCon.mkₐ R (symRingCon R M))).toLinearMap ∘ₗ TensorAlgebra.ι R) x
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f
⊢ ↑e = SymmetricAlgebra.lift f

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f
x : M
⊢ (↑↑e ∘ₗ SymmetricAlgebra.ι R M) x = (↑(SymmetricAlgebra.lift f) ∘ₗ SymmetricAlgebra.ι R M) x
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
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
by
  have := finrank_fixedSubmodule_add_le e f
  have := finrank_le_one_add_finrank_fixedSubmodule_dilatransvection f hf
  have : finrank K ↥(e.fixedSubmodule ⊔ f.fixedSubmodule) ≤ finrank K V :=
    finrank_le _
  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 : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ finrank K ↥(↑(transvection hfv * e)).fixedSubmodule ≤ finrank K ↥((↑e).fixedSubmodule ⊔ K ∙ v)

Tactic:
finrank_sup_span_singleton hv,

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 : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ finrank K ↥(↑(transvection hfv * e)).fixedSubmodule ≤ finrank K ↥(↑e).fixedSubmodule + 1
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 : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
⊢ (↑e).fixedSubmodule ⊔ K ∙ v = (↑(transvection hfv * e)).fixedSubmodule

Tactic:
suffices e.fixedSubmodule ⊔ K ∙ v ≤ (transvection hfv * e).fixedSubmodule by
    apply Submodule.eq_of_le_of_finrank_le this
    rw [finrank_sup_span_singleton hv, add_comm]
    apply finrank_fixedSubmodule_dilatransvection_mul_le
    exact transvection_mem_dilatransvections hfv

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 : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
⊢ (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
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 : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ f x ∈ map f (↑e).fixedSubmodule

Tactic:
exact mem_map_of_mem hx

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
n✝ : ℕ
e : V ≃ₗ[K] V
he✝ : e.fixedReduce = 1
n : ℕ
h✝ : finrank K (V ⧸ ⊤) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
he : (↑e).fixedSubmodule = ⊤
h : finrank K V = n + 2 + finrank K V
⊢ False

Tactic:
simp at h

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case singleton
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
a✝ : ι
hs : ∀ n ∈ {a✝}, s n ∈ C
⊢ ⋂ i ∈ {a✝}, s i ∈ C

Tactic:
simpa using hs

Goal state after: