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

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Nontrivial ι
⊢ ∃ a, f = a • 1

Tactic:
exact exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis b h

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

Goal state before:
pp: case pos
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v

pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
· by_cases hv : v = 0
    · simp [hv]
    by_cases hf : f = 0
    · simp [hf]
    obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    suffices toMatrix b b (LinearMap.transvection f v) = Matrix.transvection i j 1 by
      rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.transvection]
    simp only [hj.2, Basis.coord_apply, Basis.repr_self, hj.1, map_add, map_smul,
      Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_add, Pi.add_apply, Matrix.add_apply]
    apply congr_arg₂
    · by_cases h : x = y
      · rw [h]; simp
      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
    · by_cases h : i = x ∧ j = y
      · rw [h.1, h.2]; simp
      · rcases not_and_or.mp h with h' | h' <;>
          simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]

Goal state after:
case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v
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 ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ ((includeLeftRingHom 𝒜 ℬ).comp (algebraMap R A)) r * x = x * ((includeLeftRingHom 𝒜 ℬ).comp (algebraMap R A)) r

Tactic:
by
    dsimp [mul_def, mulHom_apply, auxEquiv_tmul]
    simp_rw [DirectSum.decompose_algebraMap, DirectSum.decompose_one, algebraMap_gradedMul,
      gradedMul_algebraMap]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
⊢ b.ExteriorAlgebra ↑s = ↑((Basis.exteriorPower m b) s)

Tactic:
rw [basis_apply_powersetCard, exteriorPower.basis_apply, ιMulti_family_apply_coe]

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

Goal state before:
pp: case refine_2
ι : 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
⊢ ∃ c, g = ∑ x, c x • Pi.single (f x) (a x)

Tactic:
refine ⟨fun j ↦ (h (f j)).choose, ?_⟩
      ext i
      simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq,
        Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero]
      rw [eq_comm]
      by_cases! hj : ∃ j, f j = i
      · calc ∑ x : Fin n, _ =
            if i = f hj.choose then (h (f hj.choose)).choose * a hj.choose else 0 := by
              convert! Finset.sum_eq_single (M := R) hj.choose ?_ ?_
              · simp
              · rintro j - h
                have hinj := f.injective.ne h
                rw [hj.choose_spec] at hinj
                simp [hinj.symm]
              · simp
          _ = g i := by
              simp only [hj.choose_spec, ↓reduceIte]
              rw [mul_comm]
              conv_rhs =>
                rw [← hj.choose_spec, (h (f hj.choose)).choose_spec]
              simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq]
              congr!
              · exact hj.choose_spec.symm
              · simp [hj]
      · convert! Finset.sum_const_zero with x
        · specialize hj x
          rw [ne_comm] at hj
          simp [hj]
        · rw [← zero_dvd_iff]
          convert! h i
          simp [hj]

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

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
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 j, f i = Sum.inr j) ∨ ∃ f', f = Sum.inl ∘ f'

Tactic:
simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true,
        Sum.isRight_eq_false, Sum.isLeft_iff]
      intro hfr
      choose f' hf' using hfr
      exact ⟨f', funext hf'⟩

Goal state after:
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 : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ 1 • M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1),

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 : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ (M.updateRow i₀ (∑ k, 1 • M k)).det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
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✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ N.toAddSubgroup.index = if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Tactic:
by
  rw [snf.toAddSubgroup_index_eq_pow_mul_prod]
  split_ifs with h
  · simp [h]
  · have hlt : n < Fintype.card ι :=
      Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)
    simp [hlt]

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

Goal state before:
pp: case pos
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
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∃ x, g x = j'
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

pp: case neg
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
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ¬∃ x, g x = j'
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
· obtain ⟨x, rfl⟩ := hj''
          rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB
          · rw [hAB]
            change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
            refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
            · apply pow_mem
              exact ⟨-1, by simp⟩
            · exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)
          · simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]

Goal state after:
case neg
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
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ¬∃ x, g x = j'
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < (A ^ (m + 1)) i j ↔ Nonempty { p // p.length = m + 1 }

Tactic:
rw [pow_succ, mul_apply]

Goal state after:
case succ
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j ↔ Nonempty { p // p.length = m + 1 }
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
v : ι → M
⊢ (mapMatrixModule ι (g ∘ₗ f)) v = (mapMatrixModule ι g) ((mapMatrixModule ι f) v)

Tactic:
simp [mapMatrixModule_comp]

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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ ↑4 ∣ ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j)

Tactic:
exact Finset.dvd_sum fun j _ => hdvd j

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

Goal state before:
pp: n : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_4
inst✝ : CommRing R
A : Matrix n n R
⊢ A.Nonsingular ↔ A.det ∈ nonZeroDivisors R

Tactic:
simp_rw [Nonsingular, isDetpBalanced_iff_sub_mul_det_eq_zero, mem_nonZeroDivisors_iff_right]
  exact ⟨fun h x eq ↦ h x 0 (by simpa), fun h a b eq ↦ sub_eq_zero.mp <| h _ (by simpa)⟩

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

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A✝ : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
hg : Function.Injective ⇑g
A : Matrix (Fin n) (Fin n) R := LinearMap.toMatrix' (g ∘ₗ f)
hA : A.Nonsingular
this : A.row ⟨m, hnm⟩ = 0
⊢ ∀ (a b : R), a = b

Tactic:
simpa [Nonsingular, IsDetpBalanced, detp_eq_of_row_eq_zero _ this] using hA

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

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
⊢ n ≤ m

Tactic:
by
    let g : (Fin m → R) →ₗ[R] (Fin n → R) := .pi fun i ↦ if h : i < m then .proj ⟨i, h⟩ else 0
    by_contra! hnm
    have hg : Function.Injective g := fun x y eq ↦ funext fun i ↦ by
      simpa [g] using congr($eq ⟨i, i.prop.trans hnm⟩)
    let A := (g ∘ₗ f).toMatrix'
    have hA : A.Nonsingular := .of_linearIndependent_col <| mulVec_injective_iff.mp <| by
      convert hg.comp hf; ext; simp [A, g]
    have : A.row ⟨m, hnm⟩ = 0 := by ext; simp [A, g]
    exact not_subsingleton R
      ⟨by simpa [Nonsingular, IsDetpBalanced, detp_eq_of_row_eq_zero _ this] using hA⟩

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

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → iSupIndep fun i ↦ (f i).submodule

Tactic:
rintro ⟨f, hf, hi⟩

Goal state after:
case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep fun i ↦ ((fun i ↦ mk K (f i) ⋯) i).submodule
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 : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ span S ↔ x ∈ sInf {W | S ⊆ ↑W}

Tactic:
mem_span x

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W) ↔ x ∈ sInf {W | S ⊆ ↑W}
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 0 1) ≤ ⨆ p, lineStab p.submodule

Tactic:
← Projectivization.submodule_mk (K := F) _ (Pi.single_ne_zero_iff.2 one_ne_zero)

Goal state after:
case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 0 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 1 1) ≤ ⨆ p, lineStab p.submodule

Tactic:
← Projectivization.submodule_mk (K := F) _ (Pi.single_ne_zero_iff.2 one_ne_zero)

Goal state after:
case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 1 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule
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
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
a : K
ha : f = a • 1
hscalar : ↑m = (Matrix.scalar ι) a
⊢ a ^ Fintype.card ι = 1

Tactic:
simpa [hscalar] using m.2

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
u : Kˣ
v : ι → K
hv : v ≠ 0
⊢ (Matrix.GeneralLinearGroup.scalar ι) u • mk K v hv = mk K v hv

Tactic:
by
    simp only [smul_mk, mk_eq_mk_iff]
    exact ⟨u, by simp [Units.smul_def]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
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
⊢ ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • LinearMap.id =
    ↑↑(center_equiv_rootsOfUnity g) • LinearMap.id

Tactic:
have hgg' := Subgroup.centerCongr_apply_coe (Matrix.SpecialLinearGroup.toLin_equiv b) g

Goal state after:
case neg
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
hgg' : ↑((centerCongr (toLin_equiv b)) g) = (toLin_equiv b) ↑g
⊢ ↑↑(centerEquivRootsOfUnity ((centerCongr (toLin_equiv b)) g)) • LinearMap.id =
    ↑↑(center_equiv_rootsOfUnity g) • LinearMap.id
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
⊢ shortAddLongRoot P = shortRoot P + longRoot P

Tactic:
by
  simp [shortAddLongRoot, shortAddLong, reflection_apply_root]

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

Goal state before:
pp: case inr.inr.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
k l : ι
hkl : k ≠ l
⊢ ∑ x ∈ {k, l},
      ((if P.root x = P.root ↑i + P.root l then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) l) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x l
        else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) l) + ↑(b.cartanMatrix i j)
    else 0

Tactic:
simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]

Goal state after:
case inr.inr.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
k l : ι
hkl : k ≠ l
⊢ (if P.root k = P.root ↑i + P.root l then
      ↑(P.pairingIn ℤ k ↑j) * (↑(chainBotCoeff (↑i) l) + 1) - (↑(chainBotCoeff (↑i) l) + 1) * ↑(P.pairingIn ℤ l ↑j)
    else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(P.pairingIn ℤ ↑i ↑j) * ↑(chainBotCoeff (↑i) l) + ↑(P.pairingIn ℤ ↑i ↑j)
    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✝ : CharZero R
i : ι
⊢ P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 1) (i := short P) (l := long P)

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.EmbeddedG2
inst✝ : CharZero R
i : ι
⊢ 3 • P.pairingIn ℤ (short P) i + 1 • P.pairingIn ℤ (long P) i =
    3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

ι : 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✝ : CharZero R
i : ι
⊢ P.root (threeShortAddLong P) = 3 • P.root (short P) + 1 • P.root (long P)
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.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i

Tactic:
by
  rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 2) (i := short P) (l := long P)]
  · simp
  · simp only [threeShortAddTwoLongRoot_eq]
    norm_cast

Goal state after: