mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (lof R ι (fun i ↦ ↥(ℬ i)) j₁) b₁))
          ((lof R ι (fun i ↦ ↥(𝒜 i)) i₂) a₂ ⊗ₜ[R] (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))

Tactic:
rw [tmul_of_gradedMul_of_tmul]

Goal state after:
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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        ((-1) ^ (j₁ * i₂) •
          ((decompose 𝒜) a₁ * (lof R ι (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
            ((lof R ι (fun x ↦ ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] 1 * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] b₂

Tactic:
convert! tmul_zero_coe_mul_coe_tmul 𝒜 ℬ a₁ (@GradedMonoid.GOne.one _ (ℬ ·) _ _) a₂ b₂
  rw [SetLike.coe_gOne, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (j₁ * i₂) •
      (gradedComm R 𝒜 ℬ)
        ((DirectSum.of 𝒜 (i₁ + i₂)) (GradedMonoid.GMul.mul a₁ a₂) ⊗ₜ[R]
          (DirectSum.of ℬ (j₁ + j₂)) (GradedMonoid.GMul.mul b₁ b₂)) =
    (-1) ^ (j₂ * i₂) •
      (-1) ^ (j₁ * i₁) •
        ((gradedMul R ℬ 𝒜) ((DirectSum.of ℬ j₁) b₁ ⊗ₜ[R] (DirectSum.of 𝒜 i₁) a₁))
          ((DirectSum.of ℬ j₂) b₂ ⊗ₜ[R] (DirectSum.of 𝒜 i₂) a₂)

Tactic:
← DirectSum.lof_eq_of R,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (j₁ * i₂) •
      (gradedComm R 𝒜 ℬ)
        ((lof R ι 𝒜 (i₁ + i₂)) (GradedMonoid.GMul.mul a₁ a₂) ⊗ₜ[R]
          (lof R ι ℬ (j₁ + j₂)) (GradedMonoid.GMul.mul b₁ b₂)) =
    (-1) ^ (j₂ * i₂) •
      (-1) ^ (j₁ * i₁) •
        ((gradedMul R ℬ 𝒜) ((lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁) a₁)) ((lof R ι ℬ j₂) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e'_2.a
ι : 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
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
j : Fin n
h : ¬i = f j
a✝ : j ∈ Finset.univ
⊢ (c j • if i = f j then a j else 0) = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index

Tactic:
simp [h]

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ ∀ (B : FixedDetMatrix (Fin 2) ℤ m) (n : ℤ), C (T ^ n • B) ↔ C B

Tactic:
intro B

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ ∀ (n : ℤ), C (T ^ n • B) ↔ C B
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
h : A.det = 0
⊢ Module.End.HasEigenvalue (Matrix.toLin' A) 0

Tactic:
rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]

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
h : A.det = 0
⊢ ⊥ ≠ (Matrix.toLin' A).ker
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: n : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_4
inst✝ : CommRing R
A : Matrix n n R
⊢ A.Nonsingular ↔ A.det ∈ nonZeroDivisors R

Tactic:
Nonsingular,

Goal state after:
n : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_4
inst✝ : CommRing R
A : Matrix n n R
⊢ (∀ (a b : R), A.IsDetpBalanced a b → a = b) ↔ A.det ∈ nonZeroDivisors R
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
A : Matrix n n R
inst✝¹ : IsCancelAdd R
inst✝ : Finite n
⊢ LinearIndependent R A.col ↔ LinearIndependent R A.row

Tactic:
have := Fintype.ofFinite
  classical rw [linearIndependent_col_iff, linearIndependent_row_iff]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : f * f = f
⊢ IsSelfAdjoint f

Tactic:
WithConv.ext_iff,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : (f * f).ofConv = f.ofConv
⊢ IsSelfAdjoint f
Module: Mathlib.LinearAlgebra.PiTensorProduct.Finite

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
n : ι → ℕ
γ : (i : ι) → Fin (n i) → M i
hg : ∀ (i : ι), Submodule.span R (Set.range (γ i)) = ⊤
⊢ Module.Finite R (⨂[R] (i : ι), M i)

Tactic:
Module.finite_def,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
n : ι → ℕ
γ : (i : ι) → Fin (n i) → M i
hg : ∀ (i : ι), Submodule.span R (Set.range (γ i)) = ⊤
⊢ ⊤.FG
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
cases finite_or_infinite k with
  | inr h =>
    have : Infinite V := Module.Free.infinite k V
    simp
  | inl h =>
  cases finite_or_infinite V with
  | inr h =>
    have := not_iff_not.mpr (finite_iff_of_finite k V)
    push Not at this
    have : Infinite (ℙ k V) := by rwa [this]
    simp
  | inl h =>
  classical
  have : Fintype V := Fintype.ofFinite V
  have : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  have : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
a b : ℙ K V
h : a = b
⊢ IsCollinear {a, b}

Tactic:
simp [h]

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

Goal state before:
pp: case h.a
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 := ⋯
b : Module.Basis (↑s) K V := ⋯
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : D.rep = D'.rep
⊢ ![D.rep, D'.rep] 0 = ![D.rep, D'.rep] 1

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Submodule.map (↑e.toLinearEquiv) Q.radical = Q'.radical

Tactic:
ext
  simp [mem_radical_iff', ← e.map_app, -map_app, e.toEquiv.forall_congr_left]

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

Goal state before:
pp: case zero
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
h : w i = zero
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 0 ∨ (fun x ↦ ↑(w x)) i = 1

Tactic:
simp [h]

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

Goal state before:
pp: case neg
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
h : w i = neg
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 0 ∨ (fun x ↦ ↑(w x)) i = 1

Tactic:
simp [h]

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

Goal state before:
pp: case pos
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module ℝ M
inst✝ : FiniteDimensional ℝ M
Q : QuadraticForm ℝ M
w : Fin (finrank ℝ M) → SignType
hw : Equivalent Q (weightedSumSquares ℝ fun i ↦ ↑(w i))
i : Fin (finrank ℝ M)
h : w i = pos
⊢ (fun x ↦ ↑(w x)) i = -1 ∨ (fun x ↦ ↑(w x)) i = 0 ∨ (fun x ↦ ↑(w x)) i = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (λ_ X).hom =
    (((Iso.refl
              ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj (𝟙_ (QuadraticModuleCat R)) ⊗
                (forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X)).symm ≪≫
          ((Iso.refl (𝟙_ (ModuleCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X))) ≪≫
        λ_ ((forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X)).hom

Tactic:
simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom,
          Iso.refl_hom, MonoidalCategory.tensorIso_hom, MonoidalCategory.tensorHom_id]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        erw [MonoidalCategory.id_whiskerRight]
        simp
        rfl

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

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
j : ℕ
V : Submodule R M
⊢ Module.finrank R ↥V = j ↔ Module.finrank R ↥((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv V) = j

Tactic:
revert j

Goal state after:
case e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
V : Submodule R M
⊢ ∀ (j : ℕ), Module.finrank R ↥V = j ↔ Module.finrank R ↥((Submodule.orderIsoMapComap e.toLinearEquiv).toEquiv V) = j
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
⊢ W ≤ Vp → W ≤ V → W ≤ ⊥

Tactic:
hWp

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
⊢ W ≤ V → W ≤ ⊥
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
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' : P.root k + P.root l ∈ range ⇑P.root
hl : P.root l = P.root k + P.root l - P.root j
⊢ False

Tactic:
rw [add_comm, add_sub_assoc, left_eq_add, sub_eq_zero, P.root.injective.eq_iff] at hl

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
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' : P.root k + P.root l ∈ range ⇑P.root
hl : k = j
⊢ False
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
i✝ : ↥b.support
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i val✝ : ↥b.support
⊢ h i (Sum.inl val✝) (Sum.inl i✝) = 0

Tactic:
simp [h]

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

Goal state before:
pp: case mem.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
b : P.Base
i✝ : ↥b.support
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
val✝ : ι
⊢ h i (Sum.inr val✝) (Sum.inl i✝) = 0

Tactic:
simp [h]

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

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
· simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
⊢ P.root k = P.root i + P.root j

Tactic:
rwa [contra, sub_eq_iff_eq_add] at h₂

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
contra : P.root m = -P.root i
⊢ P.root k = -P.root i + P.root j

Tactic:
rwa [contra, sub_eq_iff_eq_add] at h₂

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * ⁅x, y⁆ * ω b = ⁅ω b * x * ω b, ω b * y * ω b⁆

Tactic:
simp only [Ring.lie_def]
    nth_rw 1 [← mul_one x]
    nth_rw 2 [← one_mul x]
    simp only [← ω_mul_ω (b := b)]
    noncomm_ring

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

Goal state before:
pp: case pos.inr.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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
m : ι
hl : P.root m = P.root j + (n + 1) • P.root ↑i
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr m) 1) (Sum.inr m)

Tactic:
replace hl : P.root m = P.root i + P.root k := by rw [hl, hk₁]; module

Goal state after:
case pos.inr.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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
m : ι
hl : P.root m = P.root ↑i + P.root k
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr m) 1) (Sum.inr m)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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✝⁷ : 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 : LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2

pp: case neg
ι : 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 : ¬LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2

Tactic:
swap

Goal state after:
case neg
ι : 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 : ¬LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2

case pos
ι : 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 : LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 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✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
long short : ι
h : P.pairingIn ℤ long short = 3
⊢ P.pairingIn ℤ ((P.reflectionPerm long) long) short = -3

Tactic:
simp [h]

Goal state after: