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 ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ (-1) ^ (0 * ia) •
      ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R]
        ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b

Tactic:
rw [zero_mul, uzpow_zero, one_smul, smul_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 ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R] ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) =
    (r • (lof R ι 𝒜 ia) a) ⊗ₜ[R] (lof R ι ℬ ib) b
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
⊢ ↑(y * z) * (ι Q) m * ↑(y * z)⁻¹ ∈ (ι Q).range

Tactic:
simp_rw [mul_inv_rev, Units.val_mul]

Goal state after:
case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
⊢ ↑y * ↑z * (ι Q) m * (↑z⁻¹ * ↑y⁻¹) ∈ (ι Q).range
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) *
            ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) ᵍ⊗ₜ[R]
          1 +
        ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.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) *
            ↑((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

Tactic:
GradedTensorProduct.tmul_coe_mul_coe_tmul,

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) *
            ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) ᵍ⊗ₜ[R]
          1 +
        ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R]
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) +
      ((-1) ^ (1 * 1) •
          (1 * ↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1)) ᵍ⊗ₜ[R]
            (↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) * 1) +
        1 ᵍ⊗ₜ[R]
          (↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2) *
            ↑((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.FreeProduct.Basic

Goal state before:
pp: case of
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
i✝ : ι
x✝ : M i✝
⊢ motive ((of M i✝) x✝)

Tactic:
exact lof _ _

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

Goal state before:
pp: case e'_2.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
h : ∀ (x : Fin n), ¬f x = i
j : Fin n
a✝ : j ∈ Finset.univ
⊢ (c j • if i = f j then a j else 0) = 0

Tactic:
specialize h j

Goal state after:
case e'_2.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
j : Fin n
h : ¬f j = i
a✝ : j ∈ Finset.univ
⊢ (c j • if i = f j then a j else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (if a = i then -(∑ x, M.submatrix i.succ.succAbove id x) b else M.submatrix i.succ.succAbove id a b) =
    M.submatrix i.castSucc.succAbove id a b

Tactic:
Finset.sum_apply,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (if a = i then -∑ c, M.submatrix i.succ.succAbove id c b else M.submatrix i.succ.succAbove id a b) =
    M.submatrix i.castSucc.succAbove id a b
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

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

Tactic:
Finset.sum_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
x✝ : Fin n
⊢ ∑ c, Mᵀ c x✝ = 0 x✝
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ diagonal A.diag i j = A i j

Tactic:
rw [diagonal_apply_ne _ hij, h hij]

Goal state after:
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
hA_nonneg : ∀ (i j : n), 0 ≤ A i j
h : Aᵀ.IsIrreducible
i j : n
⊢ 0 ≤ Aᵀ i j

Tactic:
by
      simpa [Matrix.transpose_apply] using hA_nonneg j i

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (κ i)
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : (i : ι) → DecidableEq (M i)
p : (i : ι) → κ i
m : (i : ι) → M i
⊢ ofFinsuppEquiv ((tprod R) fun i ↦ Finsupp.single (p i) (m i)) = Finsupp.single p (⨂ₜ[R] (i : ι), m i)

Tactic:
by
  simp [ofFinsuppEquiv]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (κ i)
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : (i : ι) → DecidableEq (M i)
f : (i : ι) → κ i →₀ M i
p : (i : ι) → κ i
⊢ (ofFinsuppEquiv ((tprod R) fun i ↦ f i)) p = ⨂ₜ[R] (i : ι), (f i) (p i)

Tactic:
by
  simp [ofFinsuppEquiv]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Finite (ℙ k V)
⊢ Finite V

Tactic:
rwa [finite_iff_of_finite] at hf

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

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite (ℙ k V)
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
have : n = 0 := by
      rw [← h]
      apply Module.finrank_of_not_finite
      contrapose hf
      simpa using Module.finite_of_finite k

Goal state after:
case inr
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this✝¹ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this✝ : Infinite (ℙ k V)
this : n = 0
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
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
A : Set (ℙ K V)
B : Subspace K V
h : A ⊆ ↑B
x : ℙ K V
hx : x ∈ span A
⊢ x ∈ B

Tactic:
induction hx with
      | of => apply h; assumption
      | mem_add => apply B.mem_add; assumption'

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

Goal state before:
pp: case h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Module.finrank K ↥(Subspace.submodule (Submodule.projectivization (K ∙ v))) ≤ 2

Tactic:
rw [Subspace.submodule.apply_symm_apply, finrank_span_singleton hv]

Goal state after:
case h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ 2
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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this✝ : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
r : R
hr : r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1
this : ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) = Matrix.of fun i j ↦ (b.repr ((fun x ↦ ↑g x) (b j))) i
⊢ ((Matrix.diagonal fun x ↦ r) = Matrix.of fun i j ↦ (b.repr (↑g (b j))) i) ↔ ↑↑g = r • LinearMap.id

Tactic:
rw [← (LinearMap.toMatrix b b).injective.eq_iff]

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 : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this✝ : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
r : R
hr : r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1
this : ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) = Matrix.of fun i j ↦ (b.repr ((fun x ↦ ↑g x) (b j))) i
⊢ ((Matrix.diagonal fun x ↦ r) = Matrix.of fun i j ↦ (b.repr (↑g (b j))) i) ↔
    (LinearMap.toMatrix b b) ↑↑g = (LinearMap.toMatrix b b) (r • LinearMap.id)
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
⊢ m ∈ (toPermHom (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))).ker ↔
    m ∈ Subgroup.center (Matrix.SpecialLinearGroup ι K)

Tactic:
simp only [MonoidHom.mem_ker, toPermHom_apply, Equiv.Perm.one_def, DFunLike.ext_iff, toPerm_apply,
    Equiv.refl_apply, Matrix.SpecialLinearGroup.mem_center_iff]

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
⊢ (∀ (x : ℙ K (ι → K)), m • x = x) ↔ ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg :
  g ∈
    Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι K)))
      (Subgroup.center (Matrix.SpecialLinearGroup ι K))
⊢ g = 1

Tactic:
QuotientGroup.map_mk'_self,

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : g ∈ ⊥
⊢ g = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r

Tactic:
replace hR := not_subsingleton_iff_nontrivial.mp hR
      symm
      rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
      simpa [hV] using (mem_rootsOfUnity _ _).mp r.prop

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (a b : M), a ≈ b → Q a = Q b

Tactic:
by exact lift_aux hN

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
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ 0 < ((weightedSumSquares 𝕜 w).restrict (Pi.spanSubset 𝕜 s)) ⟨v, hv⟩

Tactic:
rw [restrict_apply, weightedSumSquares_apply]

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
hv' : ⟨v, hv⟩ ≠ 0
⊢ 0 < ∑ i, w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inl.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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ ((∑ a₁,
        if a₁ = 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 a₁) * 1
        else 0) +
      ∑ a₂, if P.root a₂ = P.root ↑i + P.root l then 0 k a₂ * (↑(chainBotCoeff (↑i) l) + 1) else 0) =
    ∑ 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 j - P.root ↑i then ↑(chainTopCoeff (↑i) j) + 1 else 0)
            (Sum.inl k) (Sum.inl a₁) *
          0 a₁ l +
      if -l ∈ Finset.univ then (if k = i ∧ -l = ↑i then 1 else 0) * 1 else 0

Tactic:
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]

Goal state after:
case inl.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✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ ((if i = 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 i) * 1
      else 0) +
      ∑ a₂, if P.root a₂ = P.root ↑i + P.root l then 0 k a₂ * (↑(chainBotCoeff (↑i) l) + 1) else 0) =
    ∑ 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 j - P.root ↑i then ↑(chainTopCoeff (↑i) j) + 1 else 0)
            (Sum.inl k) (Sum.inl a₁) *
          0 a₁ l +
      if -l ∈ Finset.univ then (if k = i ∧ -l = ↑i then 1 else 0) * 1 else 0
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
B : P.InvariantForm
⊢ (B.form (longRoot P)) (longRoot P) = 3 * (B.form (shortRoot P)) (shortRoot P)

Tactic:
simpa using B.pairing_mul_eq_pairing_mul_swap (long P) (short P)

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
⊢ ∃ i, v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)

Tactic:
obtain ⟨i, t, hi : t • w = v b i⟩ := this (by simpa) hw

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
i : ι
t : K
hi : t • ↑w = v b i
⊢ ∃ i, v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inl.inl
ι : 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 : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
h_lin_ind_y : LinearIndependent R ![P.root ↑i, P.root y]
hx' : chainBotCoeff (↑i) k = chainBotCoeff (↑i) x + 1
hy' : chainTopCoeff (↑i) k = chainTopCoeff (↑i) y + 1
⊢ ((if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) -
      if P.root k = P.root y - P.root ↑i then (↑(chainTopCoeff (↑i) y) + 1) * (↑(chainBotCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)

Tactic:
simp only [hx, hy.symm, hx', hy', reduceIte, Nat.cast_add]

Goal state after:
case inl.inl
ι : 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 : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
h_lin_ind_x : LinearIndependent R ![P.root ↑i, P.root x]
h_lin_ind_y : LinearIndependent R ![P.root ↑i, P.root y]
hx' : chainBotCoeff (↑i) k = chainBotCoeff (↑i) x + 1
hy' : chainTopCoeff (↑i) k = chainTopCoeff (↑i) y + 1
⊢ (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) y) + ↑1 + 1) -
      (↑(chainTopCoeff (↑i) y) + 1) * (↑(chainBotCoeff (↑i) x) + ↑1 + 1) =
    ↑(chainBotCoeff (↑i) x) + ↑1 - (↑(chainTopCoeff (↑i) y) + ↑1)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : 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 : ι
this : InvolutiveNeg ι := P.indexNeg
aux₁ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ k = j ∧ x = ↑j)
hl : P.root (-↑i) = P.root l - P.root ↑j
⊢ P.root ↑i = P.root ↑j - P.root l

Tactic:
simpa [neg_eq_iff_eq_neg] using hl

Goal state after: