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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm h') ((changeForm h) x) = (changeForm ⋯) x

Tactic:
by
  induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
      LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
      add_comm (_ : CliffordAlgebra Q'')]

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

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ LinearMap.det (transvection (ibc.toDual fM) v) = 1 + (ibc.toDual fM) v

Tactic:
← hv,

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ LinearMap.det (transvection (ibc.toDual fM) (ε vM)) = 1 + (ibc.toDual fM) (ε vM)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
⊢ -((even.ι Q').bilin m) m = (algebraMap R ↥(even Q')) (Q m)

Tactic:
EvenHom.contract,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
⊢ -(algebraMap R ↥(even Q')) (Q' m) = (algebraMap R ↥(even Q')) (Q m)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: case e_a
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) ^ (2 • (j₁ * i₂) + (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))

Tactic:
rw [two_nsmul, uzpow_add, uzpow_add, Int.units_mul_self, one_mul]

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

Goal state before:
pp: case refine_2
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
⊢ ⇑mod ∘ ⇑b.repr = ⇑g ∘ ⇑nG.mkQ

Tactic:
ext x b

Goal state after:
case refine_2
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b✝ : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b✝.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
b : ι
⊢ ((⇑mod ∘ ⇑b✝.repr) x) b = ((⇑g ∘ ⇑nG.mkQ) x) b
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h.inl
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

Tactic:
rw [← det_transpose, transpose_submatrix]

Goal state after:
case h.inl
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (Aᵀ.submatrix g f).det = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular

Tactic:
· intro k f g
    by_cases hfg : f.Injective ∧ g.Injective
    · exact hA k f g hfg.1 hfg.2
    · use 0
      rw [SignType.coe_zero, eq_comm]
      simp_rw [not_and_or, Function.not_injective_iff] at hfg
      obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg
      · rw [← det_transpose, transpose_submatrix]
        apply det_zero_of_column_eq hij.symm
        simp [hfij]
      · apply det_zero_of_column_eq hij
        simp [hgij]

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
i : m
⊢ ((∀ (j : n), ↑j < ⊤ → A i j = 0) ∧ ∀ (c : n), ⊤ = ↑c → A i c ≠ 0) ↔
    ⊤ = ⊤ ∧ A i = 0 ∨ ∃ c, ⊤ = ↑c ∧ A.IsLeadingEntry i c

Tactic:
simp [IsLeadingEntry, funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case coe
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
i : m
a✝ : n
⊢ ((∀ (j : n), ↑j < ↑a✝ → A i j = 0) ∧ ∀ (c : n), ↑a✝ = ↑c → A i c ≠ 0) ↔
    ↑a✝ = ⊤ ∧ A i = 0 ∨ ∃ c, ↑a✝ = ↑c ∧ A.IsLeadingEntry i c

Tactic:
simp [IsLeadingEntry, funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
⊢ ∃ j s, replicateRow m' 0 x✝ = Pi.single j ↑s
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

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

Tactic:
simp_rw [mem_closedBall_iff_norm']

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᴴ * A = A * Aᴴ

Tactic:
hA.conjTranspose_mul,

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ ↑(Fintype.card n) • 1 = A * Aᴴ
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ (Aᴴ * A)ᵀ = ↑(Fintype.card n) • 1

Tactic:
hA.conjTranspose_mul,

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ (↑(Fintype.card n) • 1)ᵀ = ↑(Fintype.card n) • 1
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Ring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ (-A).IsHadamard

Tactic:
by
  simpa [isHadamard_iff, Unitary.mem_iff] using hA

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional

Goal state before:
pp: case intro
R : Type u_2
M₂ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [∀ (i : Fin n), Module.Finite R (N i)] [∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst✝³ : (i : Fin (n + 1)) → AddCommGroup (N i)
inst✝² : (i : Fin (n + 1)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (n + 1)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (n + 1)), Module.Free R (N i)
left✝ : Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i ↦ N i.succ) M₂)
right✝ : Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i ↦ N i.succ) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
exact
        ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • (mul 1) x

Tactic:
change _ = r • (1 * x)

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • (1 * x)
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case mem_add
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ⊆ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K (v✝ + w✝) hvw✝ ∈ B

Tactic:
apply B.mem_add; assumption'

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
⊢ Independent ![u, v] ↔ u ≠ v

Tactic:
rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
v : SpecialLinearGroup R V
hv : toGeneralLinearGroup v = u
⊢ LinearEquiv.det u.toLinearEquiv = 1

Tactic:
← hv,

Goal state after:
case mp
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
v : SpecialLinearGroup R V
hv : toGeneralLinearGroup v = u
⊢ LinearEquiv.det (toGeneralLinearGroup v).toLinearEquiv = 1
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 : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ LinearMap.det ↑g = ↑1

Tactic:
apply LinearMap.det_eq_one_of_not_module_finite hV

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
⊢ ((weightedSumSquares 𝕜 w).restrict (Pi.spanSubset 𝕜 s)).PosDef

Tactic:
intro ⟨v, hv⟩

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
⊢ ⟨v, hv⟩ ≠ 0 → 0 < ((weightedSumSquares 𝕜 w).restrict (Pi.spanSubset 𝕜 s)) ⟨v, hv⟩
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ sigPos (weightedSumSquares 𝕜 w) + sigNeg (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(weightedSumSquares 𝕜 w).radical =
    Nat.card ι

Tactic:
by
  rw [radical_weightedSumSquares, sigPos_weightedSumSquares, sigNeg_weightedSumSquares,
    Pi.dim_spanSubset]
  calc {i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard
  _ = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard := by
    rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
    · congr! 1
      ext
      grind
    · grind [disjoint_iff_ne]
  _ = Set.univ.ncard := by
    rw [← Set.ncard_union_eq]
    · congr! 1
      ext
      grind [le_iff_lt_or_eq]
    · grind [disjoint_iff_ne]
  _ = Nat.card ι := Set.ncard_univ _

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
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
⊢ P.IsNotG2

Tactic:
rw [← P.not_isG2_iff_isNotG2]

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
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
⊢ ¬P.IsG2
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✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
⊢ ω b * h i = -h i * ω b

Tactic:
ext (k | k) (l | l)
  · simp [ω, h]
  · simp [ω, h]
  · simp [ω, h]
  · simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop

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✝ : Fintype ι
i : ↥b.support
⊢ ω b * e i = f i * ω b

Tactic:
let := P.indexNeg
  classical
  ext (k | k) (l | l)
  · simp [ω, e, f]
  · simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
  · simp [ω, e, f]
  · simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
    rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
    simp [neg_eq_iff_eq_neg, sub_eq_add_neg]

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

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ι
k : ↥b.support
h : P.root j = P.root ↑k + P.root i
this : InvolutiveNeg ι := P.indexNeg
l : ↥b.support
⊢ ⁅e k, v b i⁆ (Sum.inl l) = ((↑(chainBotCoeff (↑k) i) + 1) • v b j) (Sum.inl l)

Tactic:
replace h : i ≠ -k := by rintro rfl; exact P.ne_zero j <| by simpa using h
    simp [e, h, -indexNeg_neg]

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

Goal state before:
pp: case mem.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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : f i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (f i) ∈ lieAlgebra b

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_f, mul_assoc]

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

Goal state before:
pp: a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
⊢ a = 0 ∧ b = 0

Tactic:
by
  simp [S_def] at ha hb hc hd he hf
  omega

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
⊢ Submodule.span R {longRoot P, shortRoot P} = ⊤

Tactic:
refine this fun k hk ij hij ↦ ?_

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
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 ∉ Submodule.span R {longRoot P, shortRoot P}
ij : ι
hij : ij ∈ {long P, short P}
⊢ P.IsOrthogonal k ij
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.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
⊢ Submodule.span ℤ (⇑P.root '' ↑b.support) = P.rootSpan ℤ

Tactic:
b.span_int_root_support

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.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
h_ne : i ≠ j
this : {i, j} ⊆ b.support
⊢ Submodule.span ℤ (Set.range ⇑P.root) = P.rootSpan ℤ