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

Goal state before:
pp: case zero
R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
W : Type u_3
inst✝⁵ : AddCommMonoid W
inst✝⁴ : Module R W
A : Type u_4
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
⊢ (TensorProduct.lift { toFun := fun a ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }).toFun (a • 0) =
    (RingHom.id A) a • (TensorProduct.lift { toFun := fun a ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }).toFun 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: case zero
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
⊢ (ibc.toDualBaseChangeAux (1 ⊗ₜ[R] f)) 0 =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case zero
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
⊢ (j.endHom 1) 0 = 1 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
⊢ Q₁ 0 = Q₂ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_3
V : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
A : Type u_5
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
W : Type u_6
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
⊢ (ibc.endHom (LinearMap.transvection f v)) 0 = (LinearMap.transvection (ibc.toDual f) (ε v)) 0

Tactic:
| zero =>

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

Goal state before:
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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : x = y
hxi : ¬x = i
⊢ (Finsupp.single y 1) x + f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 1

Tactic:
Finsupp.single_eq_of_ne hxi

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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : x = y
hxi : ¬x = i
⊢ (Finsupp.single y 1) x + f v * (Finsupp.single y 1) i * 0 = 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ (Finsupp.single y 1) x + f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]

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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ f v * ((Finsupp.single y 1) i * (Finsupp.single i 1) x) = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
hxi : ¬x = i
⊢ (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
· simp [Finsupp.single_eq_of_ne hxi]

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

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
let vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case zero
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ (map f₁) 0 * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) 0)

Tactic:
| zero =>

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

Goal state before:
pp: case mem.mem_mul.e_a.e_a.zero
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) 0 = (-1) ^ i₂ • ((map f₂) 0 * (ι Qₙ) (f₁ v₁))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ 0 ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
⊢ motive 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
cases (isEmpty_or_nonempty n).symm
  · obtain ⟨p, hp⟩ := CharP.exists K
    rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩
    have : Fact p.Prime := ⟨hp⟩
    dsimp at hk; rw [hk]
    apply (frobenius_inj K[X] p).iterate k
    repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]
    rw [← FiniteField.expand_card]
    unfold charpoly
    rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]
    apply congr_arg det
    refine matPolyEquiv.injective ?_
    rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
    · exact (id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) :)
    · exact (C M).commute_X
  · exact congr_arg _ (Subsingleton.elim _ _)

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

Goal state before:
pp: case zero
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)
⊢ (M.submatrix (Fin.succAbove 0) id).det = (↑↑0).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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✝
⊢ (A.submatrix f g✝).det ∈ Set.range SignType.cast

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
f : Fin 0 → m ⊕ m'
g : Fin 0 → n
hf : Function.Injective f
hg : Function.Injective g
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
| zero =>

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) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

Tactic:
by
  rw [← det_transpose, transpose_submatrix,
    submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det M.transpose ?_ j₁ j₂,
    ← det_transpose, transpose_submatrix, transpose_transpose]
  ext
  simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]

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

Goal state before:
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:
· have hc := card_eq_of_linearEquiv ℤ <| bN.equivFun.symm.trans e
    simpa using hc

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

Tactic:
rw [← det_transpose, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det _ j₀ i₀
    (by simpa using hv), ← det_transpose, transpose_submatrix, transpose_transpose, add_comm]

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) ^ (↑i₀ + ↑j₀) * ∑ 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.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:
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.GeneralLinearGroup.Card

Goal state before:
pp: case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
⊢ card { s // LinearIndependent K s } = ∏ i, (q ^ n - q ^ ↑i)

Tactic:
| zero =>

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:
| zero =>

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T • B) ↔ C B

Tactic:
refine ⟨?_, hT _⟩
  intro ih
  rw [show B = T⁻¹ • T • B by simp, ← T_S_rel_smul]
  solve_by_elim (maxDepth := 10)

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

Goal state before:
pp: case zero
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T ^ 0 • B) ↔ C B

Tactic:
| zero =>

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 ᵥ* (A * Aᴴ) ⬝ᵥ 1 = ↑(Fintype.card n) ^ 2

Tactic:
hA.mul_conjTranspose,

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.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ (A * Aᴴ)ᵀ = ↑(Fintype.card n) • 1

Tactic:
hA.mul_conjTranspose,

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ (↑(Fintype.card n) • 1)ᵀ = ↑(Fintype.card n) • 1
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ (∀ (i j : n), 0 ≤ A j i) → ∃ x x_1, ∀ (x_2 : Path x x_1), x_2.length = 0

Tactic:
intro a

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
a : ∀ (i j : n), 0 ≤ A j i
⊢ ∃ x x_1, ∀ (x_2 : Path x x_1), x_2.length = 0
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
| ∏ x, c * M (x✝ x) x

Tactic:
simp [mul_comm c]

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
| ∏ x, M (x✝ x) x * c
Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional

Goal state before:
pp: case zero
R : Type u_2
M₂ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
N : Fin 0 → Type u_5
inst✝³ : (i : Fin 0) → AddCommGroup (N i)
inst✝² : (i : Fin 0) → Module R (N i)
inst✝¹ : ∀ (i : Fin 0), Module.Finite R (N i)
inst✝ : ∀ (i : Fin 0), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
| zero =>

Goal state after:
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
ind : LinearIndependent R A.col
⊢ A.Nonsingular

Tactic:
intro a

Goal state after:
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 : R
⊢ ∀ (b : R), A.IsDetpBalanced a b → a = b
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
inst✝ : IsCancelAdd R
⊢ IsLeftRegular A ↔ A.Nonsingular

Tactic:
rw [isLeftRegular_iff_mulVec_injective, mulVec_injective_iff, linearIndependent_col_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case zero
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
hι : Nat.card ι = 0
⊢ φ = φ'

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
inst✝ : DecidableEq ι
i : ι
r : R
⊢ tprodCoeff R 1 ((MonoidHom.mulSingle A i) (r • 1 i)) = r • tprodCoeff R 1 1

Tactic:
MonoidHom.mulSingle_apply,

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
inst✝ : DecidableEq ι
i : ι
r : R
⊢ tprodCoeff R 1 (Pi.mulSingle i (r • 1 i)) = r • tprodCoeff R 1 1
Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝² : (i : ι) → (j : κ i) → Module R (M i j)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDirectSumEquiv ((tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) =
    (lof R ((i : ι) → κ i) (fun i ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p) ((tprod R) fun i ↦ x i)

Tactic:
ofDirectSumEquiv

Goal state after:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝² : (i : ι) → (j : κ i) → Module R (M i j)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv ((tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) =
    (lof R ((i : ι) → κ i) (fun i ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p) ((tprod R) fun i ↦ x i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝² : (i : ι) → (j : κ i) → Module R (M i j)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDirectSumEquiv.symm ((lof R ((i : ι) → κ i) (fun p ↦ ⨂[R] (i : ι), M i (p i)) p) ((tprod R) x)) =
    (tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)

Tactic:
ofDirectSumEquiv

Goal state after:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝² : (i : ι) → (j : κ i) → Module R (M i j)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv.symm ((lof R ((i : ι) → κ i) (fun p ↦ ⨂[R] (i : ι), M i (p i)) p) ((tprod R) x)) =
    (tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ Module.finrank K ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w}))) ≤ 2

pp: case h.h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s = mk K v hv → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

pp: case h.h.refine_4
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s ∈ {mk K w hw} → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

Tactic:
· rw [Subspace.submodule.apply_symm_apply, ← Matrix.range_cons_cons_empty v w ![]]
    simp [finrank_span_eq_card h]

Goal state after:
case h.h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s = mk K v hv → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

case h.h.refine_4
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s ∈ {mk K w hw} → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))