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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂
h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q

Tactic:
have h3 : -algebraMap R _ (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q := by
                  rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂
h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q
h3 : -(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] (lof R ι ℬ i✝) x✝ =
    (r • (lof R ι 𝒜 i✝¹) x✝¹) ⊗ₜ[R] (lof R ι ℬ i✝) x✝

Tactic:
_root_.Algebra.smul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] (lof R ι ℬ i✝) x✝ =
    ((algebraMap R (⨁ (i : ι), 𝒜 i)) r * (lof R ι 𝒜 i✝¹) x✝¹) ⊗ₜ[R] (lof R ι ℬ i✝) x✝
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : (mod ∘ₗ f) x = 0
⊢ nG.mkQ x = 0

Tactic:
replace hx : ∀ b, ↑n ∣ f x b := by
      simpa [mod, DFunLike.ext_iff, ZMod.intCast_zmod_eq_zero_iff_dvd] using! hx

Goal state after:
case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : ∀ (b : ι), ↑n ∣ (f x) b
⊢ nG.mkQ x = 0
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case neg
ι : 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 : Fin n), f j ≠ i
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i

Tactic:
convert! Finset.sum_const_zero with x

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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∀ (j : Fin n), f j ≠ i
x : Fin n
a✝ : x ∈ Finset.univ
⊢ (if i = f x then ⋯.choose • a x else 0) = 0

case e'_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 : Fin n), f j ≠ i
⊢ g i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h.inr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hgij : g i = g j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

Tactic:
apply det_zero_of_column_eq hij

Goal state after:
case h.inr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hgij : g i = g j
hij : i ≠ j
⊢ ∀ (k_1 : Fin k), A.submatrix f g k_1 i = A.submatrix f g k_1 j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f_1 : Fin k → m') (g_1 : Fin k → n'), (A.submatrix (f ∘ f_1) (g ∘ g_1)).det ∈ Set.range SignType.cast

Tactic:
intro _ _ _

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m'
g✝ : Fin k✝ → n'
⊢ (A.submatrix (f ∘ f✝) (g ∘ g✝)).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f : Fin k → n) (g : Fin k → m), (A.submatrix g f).det ∈ Set.range SignType.cast

Tactic:
intro _ _ _

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → n
g✝ : Fin k✝ → m
⊢ (A.submatrix g✝ f✝).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

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

Tactic:
simp only [hj'] at hAB

Goal state after:
case succ.inl
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
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
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 i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
transpose_transpose,

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: A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 * ↑A 1 1 = 0
⊢ |↑A 0 1| < 0

Tactic:
simp_all [h₂.ne']

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

Goal state before:
pp: case base
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → C (reduce A) → C A

Tactic:
intro A h
    by_cases h1 : 0 < A.1 0 0
    · simp only [reduce_of_pos h h1, prop_red_T_pow hS hT, imp_self]
    · simp only [reduce_of_not_pos h h1, prop_red_T_pow hS hT, prop_red_S hS, imp_self]

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

Goal state before:
pp: case mpr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
ha : A.IsDiag
hb : B = 0
hc : C = 0
hd : D.IsDiag
⊢ (fromBlocks A B C D).IsDiag

Tactic:
convert! IsDiag.fromBlocks ha hd

Goal state after:
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
⊢ (A.submatrix f g).IsDetpBalanced a b

Tactic:
obtain ⟨j₀, h₀⟩ := by simpa [Function.Surjective] using hg

Goal state after:
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₀
⊢ (A.submatrix f g).IsDetpBalanced a b
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h.left
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ g • mk K D.rep ⋯ = mk K E.rep ⋯

Tactic:
smul_mk,

Goal state after:
case h.left
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ mk K (g • D.rep) ⋯ = mk K E.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h.right
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ g • mk K D'.rep ⋯ = mk K E'.rep ⋯

Tactic:
smul_mk,

Goal state after:
case h.right
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ mk K (g • D'.rep) ⋯ = mk K E'.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ e • mk K D.rep ⋯ = LinearMap.GeneralLinearGroup.ofLinearEquiv e • mk K D.rep ⋯

Tactic:
smul_mk,

Goal state after:
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ mk K (e • D.rep) ⋯ = LinearMap.GeneralLinearGroup.ofLinearEquiv e • mk K D.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
v : V
hv : v ≠ 0
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
w : V
hw : w ≠ 0
hp3 : mk K w hw ∈ Submodule.projectivization p
hq3 : mk K w hw ∈ Submodule.projectivization q
hxy : LinearIndependent K ![v, w]
⊢ Submodule.span K {v, w} = q

Tactic:
line_unique' hv hw hxy q hq1 hq2 hq3

Goal state after:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
v : V
hv : v ≠ 0
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
w : V
hw : w ≠ 0
hp3 : mk K w hw ∈ Submodule.projectivization p
hq3 : mk K w hw ∈ Submodule.projectivization q
hxy : LinearIndependent K ![v, w]
⊢ Submodule.span K {v, w} = Submodule.span K {v, w}
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos.refine_2
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
⊢ dilatransvection ⋯ • mk K D.rep ⋯ = mk K D.rep ⋯

Tactic:
smul_mk,

Goal state after:
case pos.refine_2
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
⊢ mk K (dilatransvection ⋯ • D.rep) ⋯ = mk K D.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A B : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), A • w - w ∈ L
hB : ∀ (w : ι → F), B • w - w ∈ L
w : ι → F
⊢ A • B • w - w ∈ L

Tactic:
rw [show A • B • w - w = ((A • (B • w) - A • w) - (B • w - w)) +
      (B • w - w) + (A • w - w) by abel, ← smul_sub]

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A B : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), A • w - w ∈ L
hB : ∀ (w : ι → F), B • w - w ∈ L
w : ι → F
⊢ A • (B • w - w) - (B • w - w) + (B • w - w) + (A • w - w) ∈ L
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
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : ¬x = 0
⊢ (fun x ↦ ↑u x) x = (fun x ↦ ↑v x) x

Tactic:
suffices ∀ (u : SpecialLinearGroup R V), (u : V →ₗ[R] V) = LinearMap.id by
      simp only [LinearMap.ext_iff, LinearEquiv.coe_coe, LinearMap.id_coe, id_eq] at this
      simp [this u, this v]

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
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : ¬x = 0
⊢ ∀ (u : SpecialLinearGroup R V), ↑↑u = LinearMap.id
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos.refine_3
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
⊢ dilatransvection ⋯ • mk K D'.rep ⋯ = mk K D'.rep ⋯

Tactic:
smul_mk,

Goal state after:
case pos.refine_3
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
⊢ mk K (dilatransvection ⋯ • D'.rep) ⋯ = mk K D'.rep ⋯
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case neg
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)
v : ι → K
hv : ¬v = 0
⊢ ¬LinearIndependent K ![v, f v]

Tactic:
· simpa [LinearIndependent.pair_iff' hv, mk_eq_mk_iff'] using! hm (.mk K v hv)

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

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

Tactic:
· simp [h.ne', h.not_gt, toBilin_apply]

Goal state after: