mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
i₂ : ι
⊢ AlgebraTensorModule.curry
        (((AlgebraTensorModule.curry
                  ((LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ)).compr₂
                      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
                    ↑(of R 𝒜 ℬ)))
                a₁ ∘ₗ
              (ℬ j₁).subtype)
            b₁ ∘ₗ
          ↑(of R 𝒜 ℬ)) ∘ₗ
      (𝒜 i₂).subtype =
    AlgebraTensorModule.curry
        (((AlgebraTensorModule.curry
                  ((LinearMap.mul R C ∘ₗ
                          LinearMap.mul' R C ∘ₗ
                            TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm).compl₂
                      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
                    ↑(of R 𝒜 ℬ)))
                a₁ ∘ₗ
              (ℬ j₁).subtype)
            b₁ ∘ₗ
          ↑(of R 𝒜 ℬ)) ∘ₗ
      (𝒜 i₂).subtype

Tactic:
ext a₂ b₂ : 2

Goal state after:
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
i₂ : ι
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.curry
                      ((LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ)).compr₂
                          (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
                        ↑(of R 𝒜 ℬ)))
                    a₁ ∘ₗ
                  (ℬ j₁).subtype)
                b₁ ∘ₗ
              ↑(of R 𝒜 ℬ)) ∘ₗ
          (𝒜 i₂).subtype)
        a₂)
      b₂ =
    ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.curry
                      ((LinearMap.mul R C ∘ₗ
                              LinearMap.mul' R C ∘ₗ
                                TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm).compl₂
                          (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
                        ↑(of R 𝒜 ℬ)))
                    a₁ ∘ₗ
                  (ℬ j₁).subtype)
                b₁ ∘ₗ
              ↑(of R 𝒜 ℬ)) ∘ₗ
          (𝒜 i₂).subtype)
        a₂)
      b₂
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps✝ maps : {i : I} → A i →ₐ[R] B
x y : FreeTensorAlgebra R A
r : rel R A x y
⊢ (RingCon.ker ((TensorAlgebra.lift R) (toModule R I B fun x ↦ maps.toLinearMap)).toRingHom) x y

Tactic:
by
          cases r with
          | id => simp
          | prod => simp

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
⊢ circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
ext i j

Goal state after:
α : Type u_1
n : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝³ : CommMagma α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
⊢ circulant v * circulant w = circulant w * circulant v

Tactic:
ext i j

Goal state after:
α : Type u_1
n : Type u_3
inst✝³ : CommMagma α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_5
n : Type u_6
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
⊢ circulant (Pi.single 0 1) = 1

Tactic:
ext i j

Goal state after:
α : Type u_5
n : Type u_6
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = 1 i j
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_5
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
⊢ circulant (Pi.single 0 a) = (scalar n) a

Tactic:
ext i j

Goal state after:
α : Type u_1
n : Type u_5
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = (scalar n) a i j
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
rw [snf.toAddSubgroup_index_ne_zero_iff]

Goal state after:
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ A.IsPivotedBy l ↔
    Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c

Tactic:
by
  rw [isPivotedBy_iff]
  refine and_congr_right' <| and_congr_right' <| forall_congr' fun i => ?_
  cases l i <;> simp [IsLeadingEntry, funext_iff]

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

Goal state before:
pp: case neg
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ¬∃ x, g x = j'
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rw [not_exists] at hj''

Goal state after:
case neg
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∀ (x : Fin (k + 1)), ¬g x = j'
⊢ ((A.fromRows B).submatrix f 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
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (A.fromCols 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
← transpose_isTotallyUnimodular_iff,

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (A.fromCols 1)ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
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
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (fromCols 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
← transpose_isTotallyUnimodular_iff,

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (fromCols 1 A)ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
← transpose_isTotallyUnimodular_iff,

Goal state after:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
⊢ ↑A = ↑B

Tactic:
ext i j

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
i j : n
⊢ ↑A i j = ↑B i j
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ Fintype.card (Fin n) = (↑M).rank

Tactic:
rank_unit

Goal state after:
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ Fintype.card (Fin n) = Fintype.card (Fin n)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
suffices ((reduceStep A).1 1 0) = A.1 0 0 % A.1 1 0 by
    rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]
    exact Int.emod_lt_abs (A.1 0 0) h
  simp_rw [Int.emod_def, sub_eq_add_neg, reduceStep, smul_coe, coe_T_zpow, S]
  norm_num [vecMul, vecHead, vecTail, mul_comm]

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : ↑(reps k)
h : (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) M = (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) N
⊢ M = N

Tactic:
ext i j

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : ↑(reps k)
h : (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) M = (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) N
i j : Fin 2
⊢ ↑↑M i j = ↑↑N i j
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
j : n
⊢ (1 ᵥ* A) j = (s • 1) j

Tactic:
simpa [Matrix.vecMul, dotProduct] using hcol j

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
⊢ ↑(Fintype.card n) = s * star s

Tactic:
have hvcol : (1 : n → R) ᵥ* A = s • 1 := by
    ext j
    simpa [Matrix.vecMul, dotProduct] using hcol j
  have hconjcol : Aᴴ *ᵥ (1 : n → R) = star s • 1 := by
    ext i
    simp [Matrix.mulVec, dotProduct, ← star_sum, hcol i]
  have hleft : (1 : n → R) ᵥ* (A * Aᴴ) ⬝ᵥ 1 = (Fintype.card n : R) ^ 2 := by
    rw [hA.mul_conjTranspose, Nat.cast_smul_eq_nsmul, vecMul_smul, smul_dotProduct]
    simp [dotProduct, pow_two]
  have hright : (1 : n → R) ᵥ* (A * Aᴴ) ⬝ᵥ 1 = (Fintype.card n : R) * (s * star s) := by
    rw [← vecMul_vecMul, ← dotProduct_mulVec, hvcol, hconjcol]
    simp [dotProduct]
  exact hcard.left <| show (Fintype.card n : R) * (Fintype.card n : R) =
      (Fintype.card n : R) * (s * star s) by
    simpa [pow_two] using hleft.symm.trans hright

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

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
⊢ A.IsSymm

Tactic:
ext i j

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ Aᵀ i j = A i j
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
⊢ A = 1

Tactic:
ext i j

Goal state after:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
i j : Fin 2
⊢ ↑A i j = ↑1 i j
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
hdet : IsRegular (A.det * star A.det)
hreg : IsLeftRegular A
⊢ Aᴴ * A = ↑(Fintype.card n) • 1

Tactic:
exact hreg <| show A * (Aᴴ * A) = A * ((Fintype.card n : R) • 1) by
    rw [← mul_assoc, hmul, smul_mul_assoc, one_mul, mul_smul_comm, mul_one]

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

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

Tactic:
hexpand

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

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

Tactic:
simp [Finset.sum_add_distrib, horth hrs.symm, horth hrt.symm, horth hst]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝¹ : Unique m
inst✝ : Unique n
M : Matrix m n A
⊢ (fun a ↦ of fun x x_1 ↦ a) ((fun M ↦ M default default) M) = M

Tactic:
ext i j

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝¹ : Unique m
inst✝ : Unique n
M : Matrix m n A
i : m
j : n
⊢ (fun a ↦ of fun x x_1 ↦ a) ((fun M ↦ M default default) M) i j = M i j
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 : IsRightRegular A
⊢ LinearIndependent R A.row

Tactic:
by rwa [← vecMul_injective_iff, ← isRightRegular_iff_vecMul_injective]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
⊢ (star f).ofConv = f.ofConv

Tactic:
ext i j

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
⊢ (star f).ofConv i j = f.ofConv i j
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: n : Type u_2
α : Type u_3
inst✝³ : CommSemiring α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ A.IsSymm ↔ Aᵀ = A

Tactic:
IsSymm

Goal state after:
n : Type u_2
α : Type u_3
inst✝³ : CommSemiring α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ Aᵀ = A ↔ Aᵀ = A
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)
r s : R'
⊢ (r * s) • 1 = s • (r • mul 1) 1

Tactic:
LinearMap.smul_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)
r s : R'
⊢ (r * s) • 1 = s • r • (mul 1) 1
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
⊢ ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → (↑a ∈ s) = (↑b ∈ s)

Tactic:
rintro ⟨-, h⟩ ⟨y, -⟩ c rfl

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
y : V
property✝ : y ≠ 0
c : K
h : c • ↑⟨y, property✝⟩ ≠ 0
⊢ (↑⟨c • ↑⟨y, property✝⟩, h⟩ ∈ s) = (↑⟨y, property✝⟩ ∈ s)
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.rank K ↥(Subspace.submodule ⊥) ≤ 2 ∧ ∅ ⊆ ↑⊥

Tactic:
map_bot

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.rank K ↥⊥ ≤ 2 ∧ ∅ ⊆ ↑⊥
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case mp
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

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

Tactic:
· rintro ⟨v, hv⟩
    rw [← hv, toGeneralLinearGroup_toLinearEquiv_apply]
    exact v.prop

Goal state after:
case mpr
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ LinearEquiv.det u.toLinearEquiv = 1 → u ∈ Set.range ⇑toGeneralLinearGroup
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 B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • (β • v + w) = B • (α • v + w)

Tactic:
smul_add,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + A • w = B • (α • v + w)
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 B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + A • w = B • (α • v + w)

Tactic:
smul_add,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + A • w = B • α • v + B • w
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
m : M
⊢ m ∈ Q.radical → m ∈ LinearMap.ker Q.polarBilin

Tactic:
simp +contextual [mem_radical_iff', LinearMap.ext_iff, QuadraticMap.polar]

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ { toSubmodule := span R (range h), lie_mem' := ⋯ } ≤
    LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)

Tactic:
← LieSubalgebra.toSubmodule_le_toSubmodule,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ { toSubmodule := span R (range h), lie_mem' := ⋯ }.toSubmodule ≤
    (LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)).toSubmodule
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ι
k : ↥b.support
h : P.root i = P.root j + P.root ↑k
⊢ ⁅f k, v b i⁆ = (↑(chainTopCoeff (↑k) i) + 1) • v b j

Tactic:
ext (l | l)
  · replace h : i ≠ k := by rintro rfl; exact P.ne_zero j <| by simpa using h
    simp [f, h]
  · simp [f, h, Pi.single_apply]

Goal state after: