mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ (gradedComm R 𝒜 ℬ)
      (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂)) =
    ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)))
      ((gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂))

Tactic:
rw [gradedComm_of_tmul_of, gradedComm_of_tmul_of, tmul_of_gradedMul_of_tmul]

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₂
⊢ (gradedComm R 𝒜 ℬ)
      ((-1) ^ (j₁ * i₂) • ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂)) =
    ((gradedMul R ℬ 𝒜) ((-1) ^ (j₁ * i₁) • (lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁) a₁))
      ((-1) ^ (j₂ * i₂) • (lof R ι ℬ j₂) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂)
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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r ⊗ₜ[R] 1))
        ((auxEquiv R 𝒜 ℬ) x))

Tactic:
algebraMap_gradedMul

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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x = (auxEquiv R 𝒜 ℬ).symm (r • (auxEquiv R 𝒜 ℬ) x)
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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x = (auxEquiv R 𝒜 ℬ).symm (r • (auxEquiv R 𝒜 ℬ) x)

Tactic:
LinearEquiv.map_smul

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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x = r • (auxEquiv R 𝒜 ℬ).symm ((auxEquiv R 𝒜 ℬ) x)
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 *
          ↑((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) *
          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:
GradedTensorProduct.algebraMap_def,

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 +
        ↑((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) *
          1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (CliffordAlgebra Q₁)) (Q₁ m.1) ᵍ⊗ₜ[R] 1 + (algebraMap R (CliffordAlgebra Q₁)) (Q₂ m.2) ᵍ⊗ₜ[R] 1
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ (ι R).range ^ i✝
hy✝ : y✝ ∈ (ι R).range ^ i✝
ihx : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
ihy : (liftι R M) y✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩
⊢ (liftι R M) (x✝ + y✝) = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩

Tactic:
simp_rw [map_add, ihx, ihy, ← map_add]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
⊢ f = (lift R A) fun {i} ↦ maps

Tactic:
by
  ext i a; simp_rw [AlgHom.ext_iff] at h; specialize h i a
  simp [h.symm, ι, ← ι_apply]

Goal state after:
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
⊢ (LinearIndependent S fun i ↦ ⇑(algebraMap R S) ∘ v i) ↔ LinearIndependent R v

Tactic:
change LinearIndependent S (Pi.algebraMap ι' R S ∘ v) ↔ LinearIndependent R v

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
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v) ↔ LinearIndependent R v
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e'_3
ι : 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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∀ (j : Fin n), f j ≠ i
⊢ 0 ∣ g i

Tactic:
convert! h i

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
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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∀ (j : Fin n), f j ≠ i
⊢ 0 = if h : ∃ j, f j = i then a h.choose else 0
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
⊢ (A.map f).IsDiag

Tactic:
by
  intro i j h
  simp [ha h, hf]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
qT : Path i j := transposePath (q.cons e)
⊢ ∃ p, 0 < p.length

Tactic:
let : Quiver n := toQuiver Aᵀ

Goal state after:
case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this✝ : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
qT : Path i j := transposePath (q.cons e)
this : Quiver n := Aᵀ.toQuiver
⊢ ∃ p, 0 < p.length
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : MultilinearMap R M N
h : ∀ (j : (i : ι) → γ i), (φ fun i ↦ g (j i)) = φ' fun i ↦ g (j i)
j : (i : ι) → γ i
⊢ (lift φ) (⨂ₜ[R] (i : ι), g (j i)) = (lift φ') (⨂ₜ[R] (i : ι), g (j i))

Tactic:
by simpa using h j

Goal state after:
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
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Function.LeftInverse (fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val fun x ↦ 0)

Tactic:
by intro x; aesop

Goal state after:
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
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Function.RightInverse (fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val fun x ↦ 0)

Tactic:
by intro x; aesop

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

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ Dependent ![u, v] ↔ u = v

Tactic:
rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2]

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : i < j
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ (((s • Q).toBilin bm) (bm i)) (bm i) = ((s • Q.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

Tactic:
· simp [h.ne, h, toBilin_apply, polar_smul]

Goal state after:
case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ (((s • Q).toBilin bm) (bm i)) (bm i) = ((s • Q.toBilin bm) (bm i)) (bm i)

case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)
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
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)
⊢ (e i ^ 0).col (Sum.inr j) = 1 • Pi.single (Sum.inr j) 1

Tactic:
by ext; simp [Pi.single_apply]

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 ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
A : ↥(lieAlgebra b)
x : ↥b.support ⊕ ι → R
hx : x ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier
A' : ↥(lieAlgebra b) := ⟨(ωConj b) ↑A, ⋯⟩
⊢ ⁅A, x⁆ ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier

Tactic:
suffices ⁅A', ω b *ᵥ x⁆ ∈ N by simpa [A', mul_assoc] using this

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N✝ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R N✝
P : RootPairing ι R M N✝
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
A : ↥(lieAlgebra b)
x : ↥b.support ⊕ ι → R
hx : x ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier
A' : ↥(lieAlgebra b) := ⟨(ωConj b) ↑A, ⋯⟩
⊢ ⁅A', ω b *ᵥ x⁆ ∈ N
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
⊢ P.pairingIn ℤ (short P) (long P) = -1

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed (long P) (short P)

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
this :
  (P.pairingIn ℤ (long P) (short P), P.pairingIn ℤ (short P) (long P)) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
⊢ P.pairingIn ℤ (short P) (long P) = -1
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

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 : P.root (short P) = -P.root (long P)
⊢ False

Tactic:
· norm_num [h] at this

Goal state after:
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 : P.root (short P) = -P.root (long P)
⊢ False
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
i : ↥b.support
t : IsSl2Triple (h i) (e i) (f i) := isSl2Triple i
⊢ ⁅⟨h i, ⋯⟩, ⟨f i, ⋯⟩⁆ = -(2 • ⟨f i, ⋯⟩)

Tactic:
simp [Subtype.ext_iff, t.lie_h_f_nsmul]

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

Goal state before:
pp: case inl.inr
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0 (Sum.inl k) (Sum.inr l)

Tactic:
exact lie_e_f_ne_aux₀ k l

Goal state after:
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}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : 2 * (B ↑x) ↑y = (B ↑x) ↑x * 2
h2y : (B ↑y) ↑y * 2 = 2 * (B ↑y) ↑x
⊢ 2 * (B ↑x) ↑x = 2 * (B ↑y) ↑y

Tactic:
rw [mul_comm, ← h2x, ← hSB.eq, RingHom.id_apply, ← h2y, mul_comm]

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

Goal state before:
pp: case neg
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : ¬P.root k = P.root l + P.root ↑i - P.root ↑j
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

pp: case pos
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

Tactic:
· grind

Goal state after:
case pos
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0