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

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
this : (b.coord i) (f (b i)) = (b.coord j) (f (b j))
⊢ f (b j) = (b.coord i) (f (b i)) • b j

Tactic:
feq,

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
this : (b.coord i) (f (b i)) = (b.coord j) (f (b j))
⊢ (b.coord j) (f (b j)) • b j = (b.coord i) (f (b i)) • b j
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0 + foldr' Q (contractLeftAux Q d₂) ⋯ 0) x

Tactic:
rw [LinearMap.add_apply]

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m ∈ (ι (Q' Q)).range * (ι (Q' Q)).range

Tactic:
exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mem
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
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range

Tactic:
← invOf_units x,

Goal state after:
case mem
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
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑x * (ι Q) m * ⅟↑x ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case inv_mem
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
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ↑x⁻¹ * (ι Q) m * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
← invOf_units x,

Goal state after:
case inv_mem
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
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ⅟↑x * (ι Q) m * ↑x⁻¹⁻¹ ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ (ι Q).range

Tactic:
← invOf_units x,

Goal state after:
case mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ involute ↑x * (ι Q) b * ⅟↑x ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
← invOf_units x,

Goal state after:
case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ involute ⅟↑x * (ι Q) b * ↑x⁻¹⁻¹ ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
⊢ L.goursatFst.toAddSubgroup = L.toAddSubgroup.goursatFst

Tactic:
ext x
  simp [goursatFst, AddSubgroup.mem_goursatFst]

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

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

Tactic:
calc ∑ x : Fin n, _ = c h.choose * if i = f h.choose then a h.choose else 0 := by
              refine Finset.sum_eq_single h.choose ?_ (by simp)
              rintro j - hj
              have hinj := f.injective.ne hj
              rw [h.choose_spec] at hinj
              simp [hinj.symm]
          _ = c h.choose * a h.choose := by simp [h.choose_spec]

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
⊢ (∀ (x : Fin (k + 1)), (f x).isLeft = true) → ∃ f', f = Sum.inl ∘ f'

Tactic:
Sum.isLeft_iff

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)), ∃ y, f x = Sum.inl y) → ∃ f', f = Sum.inl ∘ f'
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
htri : (A.submatrix Subtype.val g).IsUpperTriangular
⊢ (A.submatrix Subtype.val g).det ≠ 0

Tactic:
rw [det_of_isUpperTriangular htri]

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
htri : (A.submatrix Subtype.val g).IsUpperTriangular
⊢ ∏ i, A.submatrix Subtype.val g i i ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑A 1 0 = 0
⊢ (↑(reduceStep A) 1 0).natAbs < (↑A 1 0).natAbs

Tactic:
zify

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑A 1 0 = 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑a 1 0 = 0
⊢ (↑(reduceStep a) 1 0).natAbs < (↑a 1 0).natAbs

Tactic:
zify

Goal state after:
m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑a 1 0 = 0
⊢ |↑(reduceStep a) 1 0| < |↑a 1 0|
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0 ∧ -↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ -↑A 0 1 ∧ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|

Tactic:
refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩

Goal state after:
case neg.refine_1
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0

case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᴴ.IsHadamard

Tactic:
by
  exact ⟨fun i j => Unitary.star_mem (hA.apply_mem j i),
    by simpa using hA.conjTranspose_mul,
    by simpa using hA.mul_conjTranspose⟩

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
⊢ 1 ᵥ* (↑(Fintype.card n) • 1) ⬝ᵥ 1 = ↑(Fintype.card n) ^ 2

Tactic:
Nat.cast_smul_eq_nsmul,

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
⊢ 1 ᵥ* (Fintype.card n • 1) ⬝ᵥ 1 = ↑(Fintype.card n) ^ 2
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j

Tactic:
simp [h g, h (Ne.symm g)]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ Finset.univ
⊢ (f fun i ↦ Pi.single (p i) (x i (p i))) = g fun i ↦ Pi.single (p i) (x i (p i))

Tactic:
simp_rw [MultilinearMap.ext_iff] at h

Goal state after:
case a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ Finset.univ
h :
  ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) x =
      (g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) x
⊢ (f fun i ↦ Pi.single (p i) (x i (p i))) = g fun i ↦ Pi.single (p i) (x i (p i))
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
a₁ a₂ a₃ : (i : ι) → A i
ha : SemiconjBy a₁ a₂ a₃
⊢ SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)

Tactic:
rw [SemiconjBy, tprod_mul_tprod, tprod_mul_tprod, ha]

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
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
have : 1 < Nat.card k := Finite.one_lt_card
  rw [card k, Nat.mul_div_cancel]
  lia

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✝
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
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ Nat.card (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)

Tactic:
zify

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
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
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ ↑(Nat.card (ℙ k V)) * ↑(Nat.card k - 1) = (∑ x ∈ Finset.range n, ↑(Nat.card k) ^ x) * ↑(Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

Tactic:
rcases eq_or_ne y 0 with rfl | hy₂

Goal state after:
case inr.inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ x + 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

case inr.inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₂ : y ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (b.repr ↑⟨D.rep, hD_mem⟩) ⟨D.rep, hD_mem⟩ = 1

Tactic:
rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (Finsupp.single ⟨D.rep, hD_mem⟩ 1) ⟨D.rep, hD_mem⟩ = 1
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (b.repr ↑⟨D'.rep, hD'_mem⟩) ⟨D.rep, hD_mem⟩ = 0

Tactic:
rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (Finsupp.single ⟨D'.rep, hD'_mem⟩ 1) ⟨D.rep, hD_mem⟩ = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ sigPos (weightedSumSquares 𝕜 w) = {i | 0 < w i}.ncard

Tactic:
by
  let p : Set ι := {i | 0 < w i}
  let m : Set ι := {i | w i ≤ 0}
  convert_to sigPos _ = p.ncard
  have : p.ncard + m.ncard = Nat.card ι := by
    convert! Set.ncard_add_ncard_compl p
    ext
    grind
  have : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w) :=
    (sigPos_isGreatest _).2 ⟨Pi.spanSubset 𝕜 p, Pi.dim_spanSubset,
      posDef_spanSubset p (by grind)⟩
  suffices sigPos (weightedSumSquares 𝕜 w) + m.ncard ≤ Nat.card ι by lia
  simpa using sigPos_add_finrank_le_of_nonpos <| negSemidef_spanSubset m (fun _ hi ↦ hi)

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 ι
inst✝ : DecidableEq ι
x y : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ (span R (range h)).carrier
hy : y ∈ (span R (range h)).carrier
⊢ ⁅x, y⁆ ∈ (span R (range h)).carrier

Tactic:
have aux : (∀ u ∈ range (h (b := b)), ∀ v ∈ range (h (b := b)), ⁅u, v⁆ = 0) := by
      rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩; exact lie_h_h i j
    simp only [Submodule.carrier_eq_coe, SetLike.mem_coe, LieSubalgebra.mem_toSubmodule,
      ← LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero (R := R) aux] at hx hy ⊢
    exact LieSubalgebra.lie_mem _ hx hy

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

Goal state before:
pp: case inr.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✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]

Goal state after:
case inr.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✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ ∑ a₁,
        Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inr k) (Sum.inl a₁) *
          Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl a₁) (Sum.inr l) +
      ∑ a₂, Matrix.of (fun i j ↦ if i = -j then 1 else 0) k a₂ * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑i)) a₂ l =
    ∑ a₁,
        (-Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i))) (Sum.inr k) (Sum.inl a₁) *
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl a₁) (Sum.inr l) +
      ∑ a₂,
        (-Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i))) (Sum.inr k) (Sum.inr a₂) *
          Matrix.of (fun i j ↦ if i = -j then 1 else 0) a₂ l
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
contra : P.root m = -P.root i
⊢ False

Tactic:
replace h₂ : P.root k = -P.root i + P.root j := by rwa [contra, sub_eq_iff_eq_add] at h₂
    replace h₃ : P.root n = 0 := by rw [h₃, h₂]; abel
    exact P.ne_zero _ h₃

Goal state after: