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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs : LinearIndepOn R id s
⊢ LinearIndependent R fun (x : ↑↑⟨s, hs⟩) ↦ M'.mkQ ↑x

Tactic:
rw [LinearIndepOn, linearIndependent_iff'] at hs

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ LinearIndependent R fun (x : ↑↑⟨s, hs✝⟩) ↦ M'.mkQ ↑x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: 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
m : M₁ × M₂
⊢ (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) *
      (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))
          ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1 + Q₂ m.2)

Tactic:
GradedTensorProduct.includeRight_apply,

Goal state after:
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
m : M₁ × M₂
⊢ (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) *
      (↑((LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯) m.1) ᵍ⊗ₜ[R] 1 +
        1 ᵍ⊗ₜ[R] ↑((LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯) m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1 + Q₂ m.2)
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ toDirectSum ((ι R) x) = (DirectSum.of (fun n ↦ ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_1 ↦ x)

Tactic:
simp [toDirectSum, TensorAlgebra.lift_ι_apply, DirectSum.lof_eq_of]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x 0) *
      (List.map (fun x_1 ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_2 ↦ Fin.cons x₀ x x_1.succ))
          (List.finRange n)).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
Fin.cons_zero,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x ↦ x₀) *
      (List.map (fun x_1 ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_2 ↦ Fin.cons x₀ x x_1.succ))
          (List.finRange n)).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x m✝ : ExteriorAlgebra R M
hm : m✝ ∈ (ι R).range
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ (ι R).range ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
⊢ (liftι R M) (m✝ * x✝) = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝.succ) ⟨m✝ * x✝, ⋯⟩

Tactic:
obtain ⟨_, rfl⟩ := hm

Goal state after:
case mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ (ι R).range ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (liftι R M) ((ι R) w✝ * x✝) = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
i : Fin n
⊢ ↑((bM.equivFun.submoduleMap N) (bN i)) = Pi.single (f i) (a i)

Tactic:
LinearEquiv.submoduleMap_apply

Goal state after:
ι : 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)
i : Fin n
⊢ bM.equivFun ↑(bN i) = Pi.single (f i) (a i)
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 π : {i : I} → A i →ₐ[R] B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext i aᵢ

Goal state after:
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 π : {i : I} → A i →ₐ[R] B
i : I
aᵢ : A i
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.LinearAlgebra.FreeModule.Int

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

Tactic:
simp only [hj.choose_spec, ↓reduceIte]

Goal state after:
ι : 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, f j = i
⊢ ⋯.choose * a hj.choose = g i
Module: Mathlib.LinearAlgebra.FreeModule.Int

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

Tactic:
rw [← zero_dvd_iff]
          convert! h i
          simp [hj]

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

Goal state before:
pp: case h.inl
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
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

Tactic:
rw [← det_transpose, transpose_submatrix]
        apply det_zero_of_column_eq hij.symm
        simp [hfij]

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

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B * (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')

pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ * kroneckerMap (fun x1 x2 ↦ x1 * x2) A B) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')

Tactic:
· calc
      _ = ∑ x₁, ∑ x₂, A i x₁ * (B i' x₂ * Bᴴ x₂ j') * Aᴴ x₁ j := by
        simp [conjTranspose_kronecker', mul_apply, mul_assoc, ← Finset.sum_product']
      _ = if i' = j' then ∑ x, A i x * (Fintype.card n • Aᴴ) x j else 0 := by
        simp [← Finset.sum_mul, ← Finset.mul_sum, ← mul_apply, hB.mul_conjTranspose,
          one_apply, mul_assoc _ (Fintype.card n : R), -conjTranspose_apply]
      _ = _ := by
        simp only [← mul_apply, mul_smul_comm, hA.mul_conjTranspose]
        simp [one_apply, ← Nat.cast_mul, mul_comm, ← ite_and, and_comm]

Goal state after:
case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ * kroneckerMap (fun x1 x2 ↦ x1 * x2) A B) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, 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
hA : A.IsHadamard
this : (A * Aᴴ).det = (↑(Fintype.card n) • 1).det
⊢ A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n

Tactic:
rwa [det_mul, det_conjTranspose, det_smul, det_one, mul_one] at this

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

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
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)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ (piFamily (Pi.single p f)) x p' = Pi.single p (f fun i ↦ x i (p i)) p'

Tactic:
· simp [hp]

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ((fromDirectSumEquiv f) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) = (f p) x

Tactic:
have : Fintype ι := Fintype.ofFinite ι

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
this : Fintype ι
⊢ ((fromDirectSumEquiv f) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) = (f p) x
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
⊢ fromDirectSumEquiv.symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)

Tactic:
have : Fintype ι := Fintype.ofFinite ι

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ fromDirectSumEquiv.symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)
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 = (mul (r • 1)) (s • 1)

Tactic:
rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply, mul_comm,
        mul_smul]

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'
⊢ s • r • 1 = s • r • (mul 1) 1
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case e_a.e_a
ι : 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'
⊢ 1 = (mul 1) 1

Tactic:
change (1 : ⨂[R] i, A i) = 1 * 1

Goal state after:
case e_a.e_a
ι : 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'
⊢ 1 = 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✝ : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (ofDirectSumEquiv ((tprod R) x)) p = (tprod R) fun i ↦ (x i) (p i)

Tactic:
have : Fintype ι := Fintype.ofFinite ι

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✝ : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
this : Fintype ι
⊢ (ofDirectSumEquiv ((tprod R) x)) p = (tprod R) fun i ↦ (x i) (p i)
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
rintro ⟨ff, hff, hh1⟩
    contrapose hh1
    choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
    convert! hh1.units_smul a⁻¹
    ext i
    simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W

Tactic:
· exact (@sInf_le _ _ { W : Subspace K V | S ⊆ ↑W } W hW) hx

Goal state after:
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
x : ℙ K V
⊢ x ∉ ⊥

Tactic:
induction x using ind with

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : ℙ K V
hxy : x ≠ y
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
hp2 : x ∈ Submodule.projectivization p
hp3 : y ∈ Submodule.projectivization p
hq2 : x ∈ Submodule.projectivization q
hq3 : y ∈ Submodule.projectivization q
⊢ p = q

Tactic:
induction x using ind with

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

Goal state before:
pp: F : Type u_2
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
⊢ commutator PSL(2, F) = ⊤

Tactic:
have : Group.IsPerfect SL(2, F) := ⟨SL2.commutator_eq_top ha hasq⟩

Goal state after:
F : Type u_2
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
this : Group.IsPerfect SL(2, F)
⊢ commutator PSL(2, F) = ⊤
Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
⊢ (weightedSumSquares K w).IsometryEquiv (weightedSumSquares K fun i ↦ if w i = 0 then 0 else 1)

Tactic:
refine isometryEquivWeightedSumSquaresWeightedSumSquares (fun i => if h : w i = 0 then 1 else
    Units.mk0 (IsAlgClosed.exists_eq_mul_self (w i)).choose (by
      rw [← mul_self_eq_zero.ne, ← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec]
      simpa using h)) ?_
  intro i
  split_ifs with h <;>
    simp [h, pow_two, ← (IsAlgClosed.exists_eq_mul_self (w i : K)).choose_spec]

Goal state after:
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:
by
  rw [nondegenerate_iff_radical_eq_bot, radical_eq_ker_polarBilin,
    LinearMap.IsRefl.nondegenerate_iff_separatingLeft, LinearMap.separatingLeft_iff_ker_eq_bot]
  exact fun x y ↦ (polar_comm Q y x).trans

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
hx' : ¬x = 0
this : 0 < (QuadraticMap.restrict Q Vp) ⟨x, ⋯⟩
⊢ False

Tactic:
have := hV x (hWm hx)

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
W : Submodule 𝕜 M
hWp : W ≤ Vp
hWm : W ≤ V
x : M
hx : x ∈ W
hx' : ¬x = 0
this✝ : 0 < (QuadraticMap.restrict Q Vp) ⟨x, ⋯⟩
this : Q x ≤ 0
⊢ False
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✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
⊢ ω b * h i = -h i * ω b

Tactic:
classical
  ext (k | k) (l | l)
  · simp [ω, h]
  · simp [ω, h]
  · simp [ω, h]
  · simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop

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 ι
i : ↥b.support
⊢ ⁅f i, v b ↑i⁆ = u i

Tactic:
ext (j | j)

Goal state after:
case inl
ι : 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 : ↥b.support
⊢ ⁅f i, v b ↑i⁆ (Sum.inl j) = u i (Sum.inl j)

case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ↥b.support
j : ι
⊢ ⁅f i, v b ↑i⁆ (Sum.inr j) = u i (Sum.inr j)