mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K)) (M ^ Fintype.card K).charmatrix.det = M.charmatrix.det ^ Fintype.card K

Tactic:
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ detMonoidHom ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    detMonoidHom (M.charmatrix ^ Fintype.card K)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : 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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
x : ↥{x | ∃ j, f j = x}
⊢ ∃ a, f'' a = x

Tactic:
have hx := x.property

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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
x : ↥{x | ∃ j, f j = x}
hx : ↑x ∈ {x | ∃ j, f j = x}
⊢ ∃ a, f'' a = x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ∀ (j : Fin (n + 1)), j ≠ i₀ → ∑ i, Mᵀ i j = 0

Tactic:
simpa using hv

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

Goal state before:
pp: case pos.refine_1
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ (-1) ^ (↑i + ↑x) ∈ MonoidHom.mrange ↑SignType.castHom

Tactic:
apply pow_mem
              exact ⟨-1, by simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
this : Unique { s // ⊤ = ⊥ }
⊢ card { s // ⊤ = ⊥ } = ∏ x ∈ ∅, (q ^ n - q ^ ↑x)

Tactic:
Finset.prod_empty,

Goal state after:
case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
this : Unique { s // ⊤ = ⊥ }
⊢ card { s // ⊤ = ⊥ } = 1
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0

Tactic:
simp_rw [Int.emod_def, sub_eq_add_neg, reduceStep, smul_coe, coe_T_zpow, S]

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ (!![0, -1; 1, 0] * (!![1, -(↑A 0 0 / ↑A 1 0); 0, 1] * ↑A)) 1 0 = ↑A 0 0 + -(↑A 1 0 * (↑A 0 0 / ↑A 1 0))
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • T • S • T • S • A = T⁻¹ • A

Tactic:
by
  simp_rw [← T_S_rel, ← smul_assoc]

Goal state after:
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
⊢ ‖A i i - μ‖ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖

Tactic:
calc
      _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field
      _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
                rw [show μ * v i = ∑ x : n, A i x * v x by
                  rw [← dotProduct, ← Matrix.mulVec]
                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
      _ = ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ := by
                rw [Finset.sum_mul]
                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ :=
                (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))

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

Goal state before:
pp: case e_M.inl
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k✝ : n
v : n → R
k i : n
h : k = i
⊢ (adjp 1 A * A + detp (-1) A • 1) k i = (adjp (-1) A * A + detp 1 A • 1) k i

Tactic:
simp [adjp_mul_apply_eq, add_comm, adjp_mul_apply_ne, h]

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

Goal state before:
pp: case e_M.inr
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
hA : A.Nonsingular
x y : n → R
eq : A *ᵥ x = A *ᵥ y
k✝ : n
v : n → R
k i : n
h : k ≠ i
⊢ (adjp 1 A * A + detp (-1) A • 1) k i = (adjp (-1) A * A + detp 1 A • 1) k i

Tactic:
simp [adjp_mul_apply_eq, add_comm, adjp_mul_apply_ne, h]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
⊢ (LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) mul ∘ₗ
      mul =
    (((LinearMap.llcomp R (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
          ↑LinearMap.lflip)
        ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
            mul.flip ∘ₗ
          mul)).flip

Tactic:
ext x y z

Goal state after:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ z✝ : ⨂[R] (i : ι), A i
x y z : (i : ι) → A i
⊢ (((((((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                          mul ∘ₗ
                        mul).compMultilinearMap
                    (tprod R))
                  x).compMultilinearMap
              (tprod R))
            y).compMultilinearMap
        (tprod R))
      z =
    ((((((((LinearMap.llcomp R (⨂[R] (i : ι), A i)
                              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                            ↑LinearMap.lflip)
                          ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i)
                                ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i))
                              mul.flip ∘ₗ
                            mul)).flip.compMultilinearMap
                    (tprod R))
                  x).compMultilinearMap
              (tprod R))
            y).compMultilinearMap
        (tprod R))
      z
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
c : K
x : V
h₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
h₂ : c • x ≠ 0
⊢ ∃ a, a • x = c • x

Tactic:
exact ⟨c, rfl⟩

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : PSL(2, F)
p : ℙ F (Fin 2 → F)
⊢ PSL.iwasawaT (g • p) = MulAut.conj g • PSL.iwasawaT p

Tactic:
by
    obtain ⟨g_SL, rfl⟩ := QuotientGroup.mk_surjective g
    rw [Matrix.ProjectiveSpecialLinearGroup.smul_proj_mk]
    change Subgroup.map _ _ = _
    rw [PSL.smul_submodule, Matrix.SpecialLinearGroup.lineStab_smul,
      PSL.iwasawaT_map_conj]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : A ∈ {A | ∀ (w : ι → F), A • w - w ∈ L}
w : ι → F
⊢ A⁻¹ • w - w = -(w - A⁻¹ • w)

Tactic:
neg_sub

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : A ∈ {A | ∀ (w : ι → F), A • w - w ∈ L}
w : ι → F
⊢ A⁻¹ • w - w = A⁻¹ • w - w
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
⊢ ∃ c, A v = c • v ∧ ∃ (hcomap : R ∙ v ≤ Submodule.comap A (R ∙ v)), A.restrict hcomap = c • id

Tactic:
obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.1 hAv
  refine ⟨c, hc.symm, fun w hw ↦ ?_, LinearMap.ext fun ⟨w, hw⟩ ↦ ?_⟩
  <;> obtain ⟨a, rfl⟩ := Submodule.mem_span_singleton.1 hw
  · simpa [Submodule.mem_comap, map_smul] using Submodule.smul_mem _ _ hAv
  · simp [Subtype.ext_iff, ← hc, smul_comm a c v]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
u : _root_.SpecialLinearGroup R (n → R)
⊢ (fun a ↦ ↑a) ((fun A ↦ ⟨toLin' A, ⋯⟩) ((fun u ↦ ⟨LinearMap.toMatrix' ↑↑u, ⋯⟩) u)) = (fun a ↦ ↑a) u

Tactic:
simp [← LinearEquiv.toLinearMap_inj, Matrix.SpecialLinearGroup.toLin']

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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Free R M
Q : QuadraticMap R M N
ι : Type u_3
b : Basis ι R M
this : LinearOrder ι := IsWellOrder.linearOrder WellOrderingRel
⊢ ∃ a, a.toQuadraticMap = Q

Tactic:
exact ⟨_, toQuadraticMap_toBilin _ b⟩

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

Goal state before:
pp: case mp
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
⊢ (∑ x, w x * v x ^ 2 = 0 ∧ ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0) →
    ∀ i ∉ {i | w i = 0}, v i = 0

Tactic:
rintro ⟨hv, hvv'⟩ i

Goal state after:
case mp
𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w v : ι → 𝕜
hv : ∑ x, w x * v x ^ 2 = 0
hvv' : ∀ (n : ι → 𝕜), ∑ x, w x * v x ^ 2 + ∑ x, w x * (2 * v x * n x) = 0
i : ι
⊢ i ∉ {i | w i = 0} → v i = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

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✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : 0 < P.pairingIn ℤ j k
⊢ -(P.root k - P.root j) ∈ range ⇑P.root

Tactic:
neg_sub

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : 0 < P.pairingIn ℤ j k
⊢ P.root j - P.root k ∈ range ⇑P.root
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
contra : P.root k = P.root i
⊢ 2 • P.root i = P.root l

Tactic:
rwa [contra, ← two_nsmul] at h₁

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 k : ↥b.support
l : ι
⊢ ∑ a₁,
        Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inl k) (Sum.inl a₁) *
          Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) a₁ l -
      (∑ a₁,
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
              (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
              (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
              (Sum.inl k) (Sum.inl a₁) *
            0 +
        ∑ a₂,
          Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) k a₂ *
            Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inr a₂) (Sum.inr l)) =
    (b.cartanMatrix i j •
        Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
          (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
          (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0))
      (Sum.inl k) (Sum.inr l)

Tactic:
Finset.sum_eq_ite l (by aesop)

Goal state after:
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 k : ↥b.support
l : ι
⊢ ∑ a₁,
        Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inl k) (Sum.inl a₁) *
          Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) a₁ l -
      (∑ a₁,
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
              (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
              (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
              (Sum.inl k) (Sum.inl a₁) *
            0 +
        if l ∈ Finset.univ then
          Matrix.of (fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0) k l *
            Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑j)) (Sum.inr l) (Sum.inr l)
        else 0) =
    (b.cartanMatrix i j •
        Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
          (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
          (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0))
      (Sum.inl k) (Sum.inr l)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case succ
ι : 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
n : ℕ
ih : ω b * f i ^ n = e i ^ n * ω b
⊢ ω b * f i ^ n * f i = e i ^ n * e i * ω b

Tactic:
ih,

Goal state after:
case succ
ι : 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
n : ℕ
ih : ω b * f i ^ n = e i ^ n * ω b
⊢ e i ^ n * ω b * f i = e i ^ n * e i * ω b
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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
⊢ ∀ x ∈ Set.range h ∪ Set.range e ∪ Set.range f,
    (trace R (↥b.support ⊕ ι → R)) ((toEnd R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R)) x) = 0

Tactic:
rintro - ((⟨i, rfl⟩ | ⟨i, rfl⟩) | ⟨i, rfl⟩)

Goal state after:
case inl.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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
i : ↥b.support
⊢ (trace R (↥b.support ⊕ ι → R)) ((toEnd R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R)) (h i)) = 0

case inl.inr
ι : 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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
i : ↥b.support
⊢ (trace R (↥b.support ⊕ ι → R)) ((toEnd R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R)) (e i)) = 0

case inr
ι : 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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
i : ↥b.support
⊢ (trace R (↥b.support ⊕ ι → R)) ((toEnd R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R)) (f i)) = 0
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      2 * P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + 2 * P.pairing i (long P)) *
      (B.form (threeShortAddTwoLongRoot P)) (threeShortAddTwoLongRoot P)

Tactic:
rw [threeShortAddTwoLongRoot_longRoot]

Goal state after:
case calc_4
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (longRoot P)) (longRoot P) +
      2 * P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + 2 * P.pairing i (long P)) * (B.form (longRoot P)) (longRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
hki : P.pairingIn ℤ k i = 0
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
⊢ P.pairingIn ℤ m i = 0

Tactic:
simpa [aux₁] using aux₀

Goal state after: