mathlib-initiative/mathlib-tactics huggingface dataset:
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)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ (algebraMap S R) 1 + (algebraMap S R) (fM vM) = 1 + (ibc.toDual fM) (ε vM)

Tactic:
map_one,

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)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ 1 + (algebraMap S R) (fM vM) = 1 + (ibc.toDual fM) (ε vM)
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)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ (((-1) ^ (i.2 * i.1) * (-1) ^ (i.1 * i.2)) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (i.1, i.2)) (a ⊗ₜ[R] b)) i✝ =
    ((lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)) i✝

Tactic:
mul_comm i.2 i.1,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ (((-1) ^ (i.1 * i.2) * (-1) ^ (i.1 * i.2)) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (i.1, i.2)) (a ⊗ₜ[R] b)) i✝ =
    ((lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)) i✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_mul_smul_comm, e0_mul_e0, smul_neg]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0) = (ι Q) m

Tactic:
map_one,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ((ι Q) 0 + 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0) = (ι Q) m
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m : M
⊢ ((-(even.ι Q').bilin) m) m = (algebraMap R ↥(even Q')) (Q m)

Tactic:
simp_rw [LinearMap.neg_apply, EvenHom.contract, h, neg_apply, map_neg, neg_neg]

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 ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ ((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) ((lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b

Tactic:
tmul_of_gradedMul_of_tmul

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ (-1) ^ (0 * ia) •
      ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R]
        ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

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

Tactic:
tmul_of_gradedMul_of_tmul

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ (-1) ^ (i✝ * 0) • ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] ((lof R ι ℬ i✝) x✝ * 1) =
    r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝
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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (lof R ι (fun i ↦ ↥(ℬ i)) j₁) b₁))
          ((lof R ι (fun i ↦ ↥(𝒜 i)) i₂) a₂ ⊗ₜ[R] (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))

Tactic:
tmul_of_gradedMul_of_tmul

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 ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        ((-1) ^ (j₁ * i₂) •
          ((decompose 𝒜) a₁ * (lof R ι (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
            ((lof R ι (fun x ↦ ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
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 y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (gradedComm R 𝒜 ℬ)
      (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i₁) a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₂) b₂)) =
    ((gradedMul R ℬ 𝒜) ((-1) ^ (j₁ * i₁) • (lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁) a₁))
      ((-1) ^ (j₂ * i₂) • (lof R ι ℬ j₂) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂)

Tactic:
tmul_of_gradedMul_of_tmul

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (gradedComm R 𝒜 ℬ)
      ((-1) ^ (j₁ * i₂) • ((lof R ι 𝒜 i₁) a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * (lof R ι ℬ j₂) b₂)) =
    ((gradedMul R ℬ 𝒜) ((-1) ^ (j₁ * i₁) • (lof R ι ℬ j₁) b₁ ⊗ₜ[R] (lof R ι 𝒜 i₁) a₁))
      ((-1) ^ (j₂ * i₂) • (lof R ι ℬ j₂) b₂ ⊗ₜ[R] (lof R ι 𝒜 i₂) a₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case one
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
b : M
⊢ involute 1 * (ι Q) b * 1 ∈ (ι Q).range

Tactic:
map_one,

Goal state after:
case one
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
b : M
⊢ 1 * (ι Q) b * 1 ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
⊢ (map (QuadraticMap.Isometry.inl Q₁ Q₂)) ((ι Q₁) m₁) * (map (QuadraticMap.Isometry.inr Q₁ Q₂)) 1 =
    (ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)

Tactic:
map_one,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
⊢ (map (QuadraticMap.Isometry.inl Q₁ Q₂)) ((ι Q₁) m₁) * 1 = (ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₂ : M₂
⊢ (map (QuadraticMap.Isometry.inl Q₁ Q₂)) 1 * (map (QuadraticMap.Isometry.inr Q₁ Q₂)) ((ι Q₂) m₂) =
    (ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)

Tactic:
map_one,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₂ : M₂
⊢ 1 * (map (QuadraticMap.Isometry.inr Q₁ Q₂)) ((ι Q₂) m₂) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case hr
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (0, m))) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m)

Tactic:
· rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
      map_zero, zero_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
⊢ b.ExteriorAlgebra ↑s = ιMulti_family R m (⇑b) s

Tactic:
simp [basis_apply_ofCard]

Goal state after:
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
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra

Tactic:
clear! a b

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
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
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (Fintype.card K)).mapMatrix (M ^ Fintype.card K).charmatrix) =
    matPolyEquiv (M.charmatrix ^ Fintype.card K)

Tactic:
rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]

Goal state after:
case inl
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
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = X ^ p ^ k - C (M ^ p ^ k)

case inl.h
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
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
let f'' : Fin n ↪ { x // x ∈ Finset.filter (fun x ↦ ∃ j, f j = x) Finset.univ } :=
      ⟨f', hf'⟩

Goal state after:
case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
x : ↥{x | ∃ j, f j = x}
hx : ↑x ∈ {x | ∃ j, f j = x}
⊢ ∃ a, f'' a = x

Tactic:
simp only [Finset.univ_filter_exists, Finset.mem_image, Finset.mem_univ, true_and] at hx

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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
x : ↥{x | ∃ j, f j = x}
hx : ∃ a, f a = ↑x
⊢ ∃ a, f'' a = x
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ᵀ.fromRows (replicateCol n' 0)ᵀ).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
transpose_replicateCol,

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ᵀ.fromRows (replicateRow n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
⊢ IsUnit (↑M)ᵀ.det

Tactic:
let b := basisOfPiSpaceOfLinearIndependent M.2

Goal state after:
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
⊢ IsUnit (↑M)ᵀ.det
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
hcard : IsRegular ↑(Fintype.card n)
⊢ IsRegular A.det

Tactic:
by
  have : IsRegular (A.det * star A.det) := by
    rw [hA.det_mul_star_det]
    exact hcard.pow _
  exact this.of_mul_left

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:
by
  ext i j
  by_cases g : i = j; · rw [g, transpose_apply]
  simp [h g, h (Ne.symm g)]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Fintype (κ i)
b : (i : ι) → Basis (κ i) R (M i)
f : Dual R (⨂[R] (i : ι), M i)
⊢ (dualDistribInvOfBasis b) f = ∑ p, f (⨂ₜ[R] (i : ι), (b i) (p i)) • (tprod R) fun i ↦ (b i).dualBasis (p i)

Tactic:
simp only [dualDistribInvOfBasis, Basis.coe_dualBasis, ringLmapEquivSelf_symm_apply, coe_sum,
    coe_comp, coe_smulRight, End.one_apply, Finset.sum_apply, Function.comp_apply,
    applyₗ_apply_apply]
  convert! rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (κ i)
b : (i : ι) → Basis (κ i) R (M i)
this✝ : Fintype ι
this : (i : ι) → Fintype (κ i)
⊢ dualDistrib ∘ₗ dualDistribInvOfBasis b = LinearMap.id

Tactic:
classical
  refine (Basis.piTensorProduct b).dualBasis.ext (fun p ↦ ?_)
  refine (Basis.piTensorProduct b).ext (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

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:
by
  induction x using ind with | h v hv =>
  induction y using ind with | h w hw =>
  rw [← independent_pair_iff_ne, independent_mk_iff_LinearIndependent] at hxy
  rw [line_unique' hv hw hxy p hp1 hp2 hp3, line_unique' hv hw hxy q hq1 hq2 hq3]

Goal state after: