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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v : V
r : R
x : V
⊢ r • x + f (r • x) • v = (RingHom.id R) r • (x + f x • v)

Tactic:
simp [smul_eq_mul, smul_add, mul_smul]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ (LinearMap.transvection f v) ((LinearMap.transvection f (-h.unit⁻¹ • v)) x) = x

Tactic:
by
    simp only [LinearMap.transvection.apply, add_assoc, add_eq_left,
      Units.smul_def]
    rw [smul_smul, ← add_smul]
    suffices (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) = 0 by rw [this, zero_smul]
    rw [LinearMap.map_add, LinearMap.map_smul, smul_eq_mul]
    nth_rewrite 2 [← mul_one (f x)]
    rw [mul_assoc, ← mul_add, ← mul_add]
    rw [← add_assoc, add_comm _ 1, add_assoc]
    nth_rewrite 1 [← mul_one (-h.unit⁻¹), Units.val_mul, Units.val_one, ← mul_add]
    simp

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

Goal state before:
pp: case refine_1.right
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e.fixedReduce = 1

Tactic:
rw [one_eq_refl, fixedReduce_eq_one, he]

Goal state after:
case refine_1.right
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ ∀ (v_1 : V), (transvection hfv) v_1 - v_1 ∈ (↑(transvection hfv)).fixedSubmodule
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id A (A ⊗[R] CliffordAlgebra Q)

Tactic:
ext v
  simp

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

Goal state before:
pp: case h
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
hefixed_ne_top : finrank K (V ⧸ (↑e).fixedSubmodule) = 0
⊢ finrank K V = finrank K (V ⧸ (↑e).fixedSubmodule) + finrank K V

Tactic:
hefixed_ne_top,

Goal state after:
case h
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
hefixed_ne_top : finrank K (V ⧸ (↑e).fixedSubmodule) = 0
⊢ finrank K V = 0 + finrank K V
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (ι 0) r₁ * (ι 0) r₂ = 0

Tactic:
rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul,
    smul_mul_smul_comm, ι_sq_scalar, zero_apply, map_zero, smul_zero]

Goal state after:
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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q
⊢ (changeForm ⋯) x = x

Tactic:
by simp_rw [(add_neg_cancel B), changeForm_self_apply]

Goal state after:
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
⊢ ((gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x

Tactic:
suffices (gradedMul R 𝒜 ℬ).flip (algebraMap R _ r ⊗ₜ 1) = DistribSMul.toLinearMap R _ r by
    exact DFunLike.congr_fun this x
  ext
  dsimp
  erw [tmul_of_gradedMul_of_tmul]
  rw [mul_zero, uzpow_zero, one_smul, smul_tmul',
      mul_one, _root_.Algebra.smul_def, Algebra.commutes]
  rfl

Goal state after:
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
⊢ ((gradedMul R 𝒜 ℬ) x) 1 = x

Tactic:
by
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_one` to avoid timeouts.
  simpa only [RingHom.map_one, one_smul] using! gradedMul_algebraMap 𝒜 ℬ x 1

Goal state after:
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] ℬ
⊢ r • x = ((includeLeftRingHom 𝒜 ℬ).comp (algebraMap R A)) r * x

Tactic:
by
    dsimp [mul_def, mulHom_apply, auxEquiv_tmul]
    simp_rw [DirectSum.decompose_algebraMap, DirectSum.decompose_one, algebraMap_gradedMul]
    -- Qualified `map_smul` to avoid a TC timeout https://github.com/leanprover-community/mathlib4/pull/8386
    rw [LinearEquiv.map_smul]
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
hlt : i₁ < i₂
⊢ A i₁ c = 0

Tactic:
exact hA.eq_zero hlt hlead

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

Goal state before:
pp: case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g✝ : Fin 0 → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ ↑1 = !![].det

Tactic:
det_fin_zero,

Goal state after:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g✝ : Fin 0 → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ ↑1 = 1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

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

Tactic:
rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
i : Fin n
hi : a i = 0
⊢ bN i = 0

Tactic:
specialize snf i

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
i : Fin n
snf : ↑(bN i) = a i • bM (f i)
hi : a i = 0
⊢ bN i = 0
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
h : n = Fintype.card ι
⊢ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

pp: case refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ n = Fintype.card ι

Tactic:
· subst h
    exact ⟨(bN.reindex (Fintype.equivFin _).symm).equivFun⟩

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ n = Fintype.card ι
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 : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1,
      (-1) ^ (↑i + ↑x_1) * Pi.single (g x) (↑s) (g x_1) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
y : Fin (k + 1)
hxy : y ≠ x
⊢ (-1) ^ (↑i + ↑y) * Pi.single (g x) (↑s) (g y) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove y.succAbove).det =
    0

Tactic:
simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case zero
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
i j : n
⊢ 0 < (A ^ 0) i j ↔ Nonempty { p // p.length = 0 }

Tactic:
refine ⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩

Goal state after:
case zero.refine_1
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
i j : n
h_pos : 0 < (A ^ 0) i j
⊢ Nonempty { p // p.length = 0 }

case zero.refine_2
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
i j : n
x✝ : Nonempty { p // p.length = 0 }
p : Path i j
hp : p.length = 0
⊢ 0 < (A ^ 0) i j
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' : ι
⊢ single i j r i' j • v j = Pi.single i (r • v j) i'

pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' j' : ι
hj : j' ≠ j
⊢ single i j r i' j' • v j' = 0

Tactic:
· obtain rfl | hi := eq_or_ne i i' <;> simp [*]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' j' : ι
hj : j' ≠ j
⊢ single i j r i' j' • v j' = 0
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: case refine_2
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
⊢ ∏ i, diagonal d (1 i) i = ∏ i, d i

Tactic:
· simp only [Perm.one_apply, diagonal_apply_eq]

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (x + y) i_1 (p i_1)) =
    ((f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)) + (f p) fun i_1 ↦ Function.update m i y i_1 (p i_1)

Tactic:
Function.apply_update (fun i m => m (p i)) m,

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update (fun k ↦ m k (p k)) i ((x + y) (p i)) i_1) =
    ((f p) fun i_1 ↦ Function.update (fun k ↦ m k (p k)) i (x (p i)) i_1) +
      (f p) fun i_1 ↦ Function.update (fun k ↦ m k (p k)) i (y (p i)) i_1
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (c • x) i_1 (p i_1)) = c • (f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)

Tactic:
Function.apply_update (fun i m => m (p i)) m,

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update (fun k ↦ m k (p k)) i ((c • x) (p i)) i_1) =
    c • (f p) fun i_1 ↦ Function.update (fun k ↦ m k (p k)) i (x (p i)) i_1
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
h : IsLeftRegular A
⊢ LinearIndependent R A.col

Tactic:
by rwa [← mulVec_injective_iff, ← isLeftRegular_iff_mulVec_injective]

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
⊢ False

Tactic:
have : A.row ⟨m, hnm⟩ = 0 := by ext; simp [A, g]

Goal state after:
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
⊢ False
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ↑(Set.singleton i₀)ᶜ) → M ↑i
x : M i₀
⊢ (equivPiTensorComplSingletonTensor R M i₀).symm (((tprod R) fun j ↦ m j) ⊗ₜ[R] x) =
    ⨂ₜ[R] (i : ι), Function.subtypeNeLift i₀ m x i

Tactic:
by
  apply (equivPiTensorComplSingletonTensor R M i₀).injective
  simp only [LinearEquiv.apply_symm_apply, equivPiTensorComplSingletonTensor_tprod,
    Function.subtypeNeLift_self]
  congr
  ext ⟨i, hi⟩
  rw [Function.subtypeNeLift_of_neq _ _ _ _ hi]
  rfl

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
⊢ (mul ((mul x) y)) z = (mul x) ((mul y) z)

Tactic:
suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <|
        LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
  ext x y z
  dsimp [← mul_def]
  simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z)

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ u ∈ Set.range ⇑toGeneralLinearGroup ↔ LinearEquiv.det u.toLinearEquiv = 1

Tactic:
constructor
  · rintro ⟨v, hv⟩
    rw [← hv, toGeneralLinearGroup_toLinearEquiv_apply]
    exact v.prop
  · intro hu
    refine ⟨⟨u.toLinearEquiv, hu⟩, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
x : (ι → F) ⧸ L
⊢ (L.mapQ L (↑(toLin' A)) hcomap) x = LinearMap.id x

Tactic:
by
    induction x using Submodule.Quotient.induction_on with
    | _ w => simpa [Submodule.Quotient.eq] using! hA w

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Fintype.card (Module.Free.ChooseBasisIndex R V) ≤ 1

Tactic:
← Module.finrank_eq_card_basis b

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Module.finrank R V ≤ 1
Module: Mathlib.LinearAlgebra.Quotient.Bilinear

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ ∀ (a : M), (f a) n = 0 (Submodule.Quotient.mk a)

Tactic:
← f.flip_apply,

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ ∀ (a : M), (f.flip n) a = 0 (Submodule.Quotient.mk a)
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
⊢ (weightedSumSquares ℝ w).IsometryEquiv (weightedSumSquares ℝ fun i ↦ ↑(sign (w i)))

Tactic:
by
  let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h
  have hu : ∀ i : ι, 1 / √|(u i : ℝ)| ≠ 0 := fun i ↦
    have : (u i : ℝ) ≠ 0 := (u i).ne_zero
    by positivity
  have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by
    by_cases hi : w i = 0
    · simp [hi]
    · simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp
  convert!
    QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℝ w)
      ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i))
  ext1 v
  classical
  suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
  exact sum_congr rfl fun j _ ↦ by ring

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

Goal state before:
pp: case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ ∀ (x : M), (Q.polarBilin n) x = 0 x

Tactic:
(hN hn).2,

Goal state after:
case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ ∀ (x : M), True
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
⊢ LinearMap.Nondegenerate Q.polarBilin ↔ Nondegenerate

Tactic:
rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_polarBilin,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
⊢ LinearMap.IsRefl Q.polarBilin