mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case convert_3
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h✝ : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
j : Fin n
h : j ≠ hj.choose
hinj : f j ≠ f hj.choose
⊢ (if i = f j then ⋯.choose • a j else 0) = 0

Tactic:
hj.choose_spec

Goal state after:
case convert_3
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h✝ : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
j : Fin n
h : j ≠ hj.choose
hinj : f j ≠ i
⊢ (if i = f j then ⋯.choose • a j else 0) = 0
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, kpos⟩
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
have : Fact p.Prime := ⟨hp⟩

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, kpos⟩
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly
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:
AlgHom.map_det,

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)
⊢ ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix).det = M.charmatrix.det ^ Fintype.card K
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)
⊢ matPolyEquiv ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) = (X - C M) ^ Fintype.card K

Tactic:
hk,

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)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = (X - C M) ^ p ^ k
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
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
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove i) b

Tactic:
Fin.succAbove_castSucc_self,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
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
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ -∑ x, M (i.succ.succAbove x) b = M i.succ 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)
⊢ (M.submatrix id j₁.succAbove)ᵀ.det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

Tactic:
transpose_submatrix,

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)
⊢ (Mᵀ.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det
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)
⊢ (↑↑j₁ - ↑↑j₂).negOnePow • (Mᵀ.submatrix j₂.succAbove id)ᵀ.det =
    (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

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)
⊢ ∑ j, Mᵀ j = 0

Tactic:
transpose_submatrix,

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)
⊢ (↑↑j₁ - ↑↑j₂).negOnePow • (Mᵀᵀ.submatrix id j₂.succAbove).det =
    (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

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)
⊢ ∑ j, Mᵀ j = 0
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
⊢ ((-1) ^ (↑j₀ + ↑i₀) * ∑ i, Mᵀ i i₀) * (Mᵀ.submatrix j₀.succAbove i₀.succAbove)ᵀ.det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
transpose_submatrix,

Goal state after:
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
⊢ ((-1) ^ (↑j₀ + ↑i₀) * ∑ i, Mᵀ i i₀) * (Mᵀᵀ.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
x y : SpecialLinearGroup n R
b : FixedDetMatrix n R m
⊢ ⟨↑(x * y) * ↑b, ⋯⟩ = ⟨↑x * ↑y * ↑b, ⋯⟩

Tactic:
coe_mul

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
⊢ ↑(A i j * ↑A.den).num = A i j * ↑A.den

Tactic:
hk,

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
⊢ ↑(A i j * ↑((A i j).den * k)).num = A i j * ↑((A i j).den * k)
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ (↑A.den)⁻¹ • A.num.map Int.cast = A

Tactic:
ext
  simp [← Matrix.num_div_den A, div_eq_inv_mul]

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

Tactic:
by
                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]

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
⊢ ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖

Tactic:
rw [Finset.sum_mul]

Goal state after:
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)⁻¹‖
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ swap R i j *ᵥ a = a ∘ ⇑(Equiv.swap i j)

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ (swap R i j *ᵥ a) i = a j

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
σ : Perm n
M : Matrix n n R
⊢ (M.submatrix id ⇑σ)ᵀ.permanent = M.permanent

Tactic:
transpose_submatrix,

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
σ : Perm n
M : Matrix n n R
⊢ (Mᵀ.submatrix (⇑σ) id).permanent = M.permanent
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: case neg
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
this✝ : ∀ (s : ℤˣ), detp s Ai = ∑ j, detp (-s) (Aj j) * A.col (g j) i + detp s D * A.col j₀ i
this : ∀ (a b : R), (Finsupp.linearCombination R A.col) (v a b) i = a * detp 1 Ai + b * detp (-1) Ai
⊢ (Finsupp.linearCombination R A.col) (v a b) i = (Finsupp.linearCombination R A.col) (v b a) i

Tactic:
simpa [this, IsDetpBalanced, ← submatrix_submatrix] using
    ih (Option.rec i f ∘ finSuccEquiv r) (Option.rec j₀ g ∘ finSuccEquiv r)

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), (f * f).ofConv i j = f.ofConv i j
⊢ IsSelfAdjoint f

Tactic:
convMul_def,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), (f.ofConv ⊙ f.ofConv) i j = f.ofConv i j
⊢ IsSelfAdjoint f
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case succ.e_f
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
⊢ ∀ (s : ↑(Set.range g)),
    ((lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ) ↑s =
      ((lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ') ↑s

Tactic:
rintro ⟨_, ⟨g₀, rfl⟩⟩

Goal state after:
case succ.e_f
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
g₀ : γ i₀
⊢ ((lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ) ↑⟨g g₀, ⋯⟩ =
    ((lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ') ↑⟨g g₀, ⋯⟩
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
S : Set (ℙ K V)
hS : S.Subsingleton
⊢ IsCollinear S

Tactic:
obtain hS' | ⟨x, hx⟩ := hS.eq_empty_or_singleton

Goal state after:
case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.Subsingleton
hS' : S = ∅
⊢ IsCollinear S

case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.Subsingleton
x : ℙ K V
hx : S = {x}
⊢ IsCollinear S
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
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)
r : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hV : 1 ≤ Module.finrank R V
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1

Tactic:
rw [mem_rootsOfUnity', max_eq_left hV] at hr

Goal state after:
case neg
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)
r : Rˣ
hr✝ : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hr : ↑r ^ Module.finrank R V = 1
hV : 1 ≤ Module.finrank R V
⊢ ↑↑⟨r, hr✝⟩ ^ Module.finrank R V = 1
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 ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
⊢ x ∈ span R (⇑g '' range h')

Tactic:
← range_comp

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property✝ : x ∈ lieAlgebra b
hx : x ∈ span R (range h)
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  (lieAlgebra b).subtype ∘ₗ (cartanSubalgebra' b).subtype
⊢ x ∈ span R (range (⇑g ∘ h'))
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i - P.root j ∈ Set.range ⇑P.root
⊢ 0 ≤ P.pairingIn ℤ i j

Tactic:
replace h : P.root i + P.root (P.reflectionPerm j j) ∈ range P.root := by simpa [← sub_eq_add_neg]
  simpa using P.pairingIn_le_zero_of_root_add_mem h

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
i : ι
⊢ P.root (threeShortAddTwoLong P) = 3 • P.root (short P) + 2 • P.root (long P)

Tactic:
· simp only [threeShortAddTwoLongRoot_eq]
    norm_cast

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

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ι
⊢ ⁅e i, f j⁆ᵀ (Sum.inr ↑j) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
suffices ((if k = i then ↑|b.cartanMatrix i j| else (0 : R)) -
        ∑ x, if P.root x = P.root i + P.root j ∧ P.root k = P.root x - P.root j then
          (P.chainTopCoeff j x : R) + 1 else 0) = 0 by
      have hij : (j : ι) ≠ -i := by simpa using b.root_ne_neg_of_ne j.property i.property hij'.symm
      have aux : ∀ x ∈ Finset.univ,
        x ≠ j → (if x = j ∧ k = i then ↑|b.cartanMatrix i x| else 0) = (0 : R) := by aesop
      simpa [e, f, P.ne_zero, hij, -indexNeg_neg, -Finset.univ_eq_attach, ← ite_and,
        Finset.sum_eq_single_of_mem j (Finset.mem_univ _) aux]
    rcases eq_or_ne k i with rfl | hk; swap
    · rw [if_neg (by tauto), Finset.sum_ite_of_false (by aesop)]; simp
    by_cases hij_mem : P.root i + P.root j ∈ range P.root
    · obtain ⟨m, hm⟩ := hij_mem
      rw [Finset.sum_eq_single_of_mem m (Finset.mem_univ _) (by rintro x - hx; simp [← hm, hx]),
        b.abs_cartanMatrix_apply, Base.cartanMatrix, Base.cartanMatrixIn_def]
      have aux₁ := b.chainTopCoeff_eq_of_ne hij.symm
      have aux₂ := chainTopCoeff_of_add (b.linearIndependent_pair_of_ne hij.symm) hm
      norm_cast
      aesop
    · have aux : ∀ x ∈ Finset.univ,
          ¬ (P.root x = P.root i + P.root j ∧ P.root i = P.root x - P.root j) := by
        rintro x - ⟨hx, -⟩; exact hij_mem ⟨x, hx⟩
      simp [Finset.sum_ite_of_false aux, b.cartanMatrix_apply_eq_zero_iff hij, hij_mem]

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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l : ι
h₁ : P.root l = P.root j + P.root k
h₂ : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b j ∈ U → ∃ j, u j ∈ U
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hl : v b l ∈ U
this : ⁅f ⟨k, hk⟩, v b l⁆ = (↑(chainTopCoeff k l) + 1) • v b j
⊢ ⁅f ⟨k, hk⟩, v b l⁆ ∈ U

Tactic:
let f' : lieAlgebra b := ⟨f ⟨k, hk⟩, f_mem_lieAlgebra _⟩

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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l : ι
h₁ : P.root l = P.root j + P.root k
h₂ : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b j ∈ U → ∃ j, u j ∈ U
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hl : v b l ∈ U
this : ⁅f ⟨k, hk⟩, v b l⁆ = (↑(chainTopCoeff k l) + 1) • v b j
f' : ↥(lieAlgebra b) := ⟨f ⟨k, hk⟩, ⋯⟩
⊢ ⁅f ⟨k, hk⟩, v b l⁆ ∈ U