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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ↑↑((-1) ^ (ixb * iya)) •
      (-1) ^ ((ixb + iyb) * iza) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    ↑↑((-1) ^ (iyb * iza)) •
      (-1) ^ (ixb * (iya + iza)) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))

Tactic:
simp_rw [Int.cast_smul_eq_zsmul R, ← Units.smul_def, smul_smul, ← uzpow_add, add_mul, mul_add]

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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ (-1) ^ (ixb * iya + (ixb * iza + iyb * iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    (-1) ^ (iyb * iza + (ixb * iya + ixb * iza)) •
      ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
        ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
i₂ : ι
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (LinearMap.mul' R C)
      ((TensorProduct.map f.toLinearMap g.toLinearMap)
        ((of R 𝒜 ℬ).symm ((of R 𝒜 ℬ) (a₁ ⊗ₜ[R] ↑b₁) * (of R 𝒜 ℬ) (↑a₂ ⊗ₜ[R] b₂)))) =
    f a₁ * g ↑b₁ * (f ↑a₂ * g b₂)

Tactic:
tmul_coe_mul_coe_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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
i₂ : ι
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (LinearMap.mul' R C)
      ((TensorProduct.map f.toLinearMap g.toLinearMap)
        ((of R 𝒜 ℬ).symm ((-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)))) =
    f a₁ * g ↑b₁ * (f ↑a₂ * g b₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))

Tactic:
ext m <;> dsimp

Goal state after:
case hl
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m, 0))) = (ι (QuadraticMap.prod Q₁ Q₂)) (m, 0)

case hr
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (0, m))) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m)
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
f : ModN G n →+ M
g : G
Gn : AddSubgroup G := ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup
this : n • g ∈ (QuotientAddGroup.mk' Gn).ker
⊢ n • (f.comp (QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup)) g = 0

Tactic:
simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
f : ModN G n →+ M
g : G
Gn : AddSubgroup G := ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup
this : n • g ∈ (QuotientAddGroup.mk' Gn).ker
⊢ f ((QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup) (n • g)) = 0
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_1
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
c : ι → ℤ
hc : ∀ (b : ι), (f x) b = ↑n * c b
⊢ b.repr (((LinearMap.lsmul ℤ G) ↑n) (b.repr.symm { support := (f x).support, toFun := c, mem_support_toFun := ⋯ })) =
    b.repr x

Tactic:
simpa [DFunLike.ext_iff, eq_comm] using! hc

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
this✝¹ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this✝ : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent L (⇑(Pi.algebraMap ι' R L) ∘ v)
⊢ LinearIndependent S (⇑(Pi.algebraMap ι' R S) ∘ v)

Tactic:
rw [← LinearIndependent.iff_fractionRing (R := S)] at this
    have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' S L ∘ Pi.algebraMap ι' R S ∘ v := by
      ext; simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]
    rw [aux] at this
    exact this.of_comp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
⊢ A i ≠ 0 ↔ ∃ c, A.IsLeadingEntry i c

Tactic:
refine ⟨fun h => ?_, fun ⟨c, hc⟩ => hc.row_ne_zero⟩

Goal state after:
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
h : A i ≠ 0
⊢ ∃ c, A.IsLeadingEntry i c
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
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
⊢ (∀ (x : Fin (k + 1)), ¬(f x).isRight = true) → ∃ f', f = Sum.inl ∘ f'

Tactic:
Bool.not_eq_true,

Goal state after:
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
⊢ (∀ (x : Fin (k + 1)), (f x).isRight = false) → ∃ f', f = Sum.inl ∘ f'
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ p'.length = 0

Tactic:
by simp_all

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ∑ x₁, ∑ x₂, Bᴴ i' x₂ * (Aᴴ i x₁ * A x₁ j) * B x₂ j' = if i = j then ∑ x, Bᴴ i' x * (Fintype.card m • B) x j' else 0

Tactic:
by
        rw [Finset.sum_comm]
        simp [← Finset.sum_mul, ← Finset.mul_sum, ← mul_apply, hA.conjTranspose_mul,
          one_apply, mul_assoc _ (Fintype.card m : R), -conjTranspose_apply]

Goal state after:
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
μ : 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
⊢ ∑ i_1 ∈ Finset.univ.erase i, ‖A i i_1 * v i_1 * (v i)⁻¹‖ = ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖

Tactic:
by simp_rw [mul_assoc, norm_mul]

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

Goal state before:
pp: 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
⊢ LinearIndependent R A.col ↔ A.Nonsingular

Tactic:
linearIndependent_col_iff

Goal state after:
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
⊢ A.Nonsingular ↔ A.Nonsingular
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
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x ∈ ↑p

Tactic:
refine hx.casesOn ?_ ?_

Goal state after:
case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x = u → x ∈ ↑p

case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x ∈ {v} → x ∈ ↑p
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
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
⊢ p = Submodule.span K {u, v}

Tactic:
have h1 : Submodule.span K {u, v} ≤ p := by
    refine Submodule.span_le.2 fun x hx ↦ ?_
    simp only [Submodule.mk_mem_projectivization_iff] at hp2 hp3
    refine hx.casesOn ?_ ?_ <;> simp_all

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
⊢ p = Submodule.span K {u, v}
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
this : Finite F
x : Fˣ
hF : 4 ≤ orderOf x + 1
hx : Function.Surjective fun x_1 ↦ x ^ x_1
h : ↑x ^ 2 = 1
⊢ ↑(x ^ 2) = ↑1

Tactic:
by simpa using h

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

Goal state before:
pp: F : Type u_2
inst✝ : Field F
this : Finite F
x : Fˣ
hF : 4 ≤ orderOf x + 1
hx : Function.Surjective fun x_1 ↦ x ^ x_1
h : ↑x ^ 2 = 1
⊢ False

Tactic:
orderOf_le_of_pow_eq_one zero_lt_two (Units.ext <| by simpa using h)

Goal state after:
F : Type u_2
inst✝ : Field F
this : Finite F
x : Fˣ
hF : 4 ≤ 2 + 1
hx : Function.Surjective fun x_1 ↦ x ^ x_1
h : ↑x ^ 2 = 1
⊢ False
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : Matrix.SpecialLinearGroup ι F
H : Subgroup (Matrix.SpecialLinearGroup ι F)
x : Matrix.SpecialLinearGroup ι F ⧸ Subgroup.center (Matrix.SpecialLinearGroup ι F)
x✝ : ∃ x_1 ∈ H, ↑x_1 = (↑g)⁻¹ * x * ↑g
a : Matrix.SpecialLinearGroup ι F
ha : a ∈ H
hx : ↑a = (↑g)⁻¹ * x * ↑g
⊢ g⁻¹ * (g * a * g⁻¹) * g ∈ H

Tactic:
by simp [mul_assoc, ha]

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
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ Module.finrank R V = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)

Tactic:
rw [← Nat.max_eq_left hV] at hr

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
Module: Mathlib.LinearAlgebra.Quotient.Bilinear

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ n ∈ (M'.liftQ f hM').flip.ker

Tactic:
by
    simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this✝ : FaithfulSMul R V
x : V
this :
  ∀ (x : V), ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • x = ↑↑(center_equiv_rootsOfUnity g) • x
⊢ ↑↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) • x = ↑↑(center_equiv_rootsOfUnity g) • x

Tactic:
MulEquiv.trans_apply,

Goal state after:
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Nontrivial V
hι : ¬IsEmpty ι
this✝ : FaithfulSMul R V
x : V
this :
  ∀ (x : V), ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • x = ↑↑(center_equiv_rootsOfUnity g) • x
⊢ ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • x = ↑↑(center_equiv_rootsOfUnity g) • x
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:
rw [← neg_mem_range_root_iff, 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.Basic

Goal state before:
pp: case smul
ι : 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
j : ↥b.support ⊕ ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
t : R
u : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx✝ : u ∈ span R (range h)
hu : u j (Sum.inl i) = 0
⊢ (t • u) j (Sum.inl i) = 0

Tactic:
simp [hu]

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
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ i →
      (if b_1 = i ∧ l = -↑i then
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl k) (Sum.inl b_1) * 1
        else 0) =
        0

Tactic:
by simp_all

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:
by
  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: ι : 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 j : ↥b.support
⊢ e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)

Tactic:
by rw [mul_assoc, mul_assoc]

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 j : ↥b.support
⊢ ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)

Tactic:
by rw [mul_assoc, mul_assoc]

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

Goal state before:
pp: case smul
ι : 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
b : P.Base
inst✝ : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
t : R
u : ↥b.support ⊕ ι → R
hx✝ : u ∈ span R (range GeckConstruction.u)
hu : u (Sum.inr j) = 0
⊢ (t • u) (Sum.inr j) = 0

Tactic:
simp [hu]

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 ι
j : ι
k : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
l : ↥b.support
h : P.root j = P.root ↑k + P.root (-↑k)
⊢ P.root j = 0

Tactic:
by simpa using 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 ι
j : ι
k l : ↥b.support
h : P.root ↑k = P.root j + P.root ↑k
⊢ P.root j = 0

Tactic:
by simpa using h

Goal state after: