mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case mul
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * (x₂ * y) = y * (x₁ * x₂)

Tactic:
hx₂,

Goal state after:
case mul
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * (y * x₂) = y * (x₁ * x₂)
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
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
⊢ (b.repr (b y + f (b y) • v)) x = (1 + Matrix.single i j 1) x y

Tactic:
simp only [hj.2, Basis.coord_apply, Basis.repr_self, hj.1, map_add, map_smul,
      Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_add, Pi.add_apply, Matrix.add_apply]

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
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single y 1) x + (Finsupp.single i ((Finsupp.single y 1) j)) x = 1 x y + Matrix.single i j 1 x y
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
⊢ -((v Q) m * e0 Q) = e0 Q * (v Q) m

Tactic:
by
  rw [neg_eq_iff_eq_neg]
  exact (neg_e0_mul_v _ m).symm

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

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
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
⊢ ↥(even Q) →ₗ[R] A

Tactic:
refine ?_ ∘ₗ (even Q).val.toLinearMap

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
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
⊢ CliffordAlgebra Q →ₗ[R] A
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 j : ι
a : 𝒜 i
b : ℬ j
⊢ (TensorProduct.directSum R R ℬ 𝒜).symm
      (↑((-1) ^ (j * i)) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)) =
    (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Tactic:
← Int.cast_smul_eq_zsmul R,

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 j : ι
a : 𝒜 i
b : ℬ j
⊢ (TensorProduct.directSum R R ℬ 𝒜).symm
      (↑↑((-1) ^ (j * i)) • (lof R (ι × ι) (fun i ↦ ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)) =
    (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a
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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
      ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
        (a₁ ⊗ₜ[R]
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
            ((↑((-1) ^ (i₂ * j₁)) • (lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁) ⊗ₜ[R] b₂))) =
    ↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)

Tactic:
← Int.cast_smul_eq_zsmul R,

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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
      ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
        (a₁ ⊗ₜ[R]
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
            ((↑↑((-1) ^ (i₂ * j₁)) • (lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁) ⊗ₜ[R] b₂))) =
    ↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
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:
rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((gradedMul R 𝒜 ℬ)
        (↑((-1) ^ (ixb * iya)) •
          ((lof R ι 𝒜 ixa) xa * (lof R ι 𝒜 iya) ya) ⊗ₜ[R] ((lof R ι ℬ ixb) xb * (lof R ι ℬ iyb) yb)))
      ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb) =
    ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
      (↑((-1) ^ (iyb * iza)) •
        ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za) ⊗ₜ[R] ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))

Tactic:
← Int.cast_smul_eq_zsmul R,

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 z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((gradedMul R 𝒜 ℬ)
        (↑↑((-1) ^ (ixb * iya)) •
          ((lof R ι 𝒜 ixa) xa * (lof R ι 𝒜 iya) ya) ⊗ₜ[R] ((lof R ι ℬ ixb) xb * (lof R ι ℬ iyb) yb)))
      ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb) =
    ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
      (↑↑((-1) ^ (iyb * iza)) •
        ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za) ⊗ₜ[R] ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))
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
        (↑((-1) ^ (j₁ * i₂)) •
          ((decompose 𝒜) a₁ * (DirectSum.of (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
            ((DirectSum.of (fun x ↦ ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))

Tactic:
← Int.cast_smul_eq_zsmul R,

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₁ * (DirectSum.of (fun x ↦ ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R]
            ((DirectSum.of (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 𝒜 ℬ)
      (↑((-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₂)

Tactic:
← Int.cast_smul_eq_zsmul R,

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.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₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] ↑b₁ * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
by
  convert! tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ b₁ (@GradedMonoid.GOne.one _ (𝒜 ·) _ _) b₂
  rw [SetLike.coe_gOne, mul_one]

Goal state after:
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
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₁
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ (map f₁) m₁ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) m₁)

Tactic:
by
  -- for each variable, induct on powers of `ι`, then on the exponent of each power
  induction hm₁ using Submodule.iSup_induction' with
  | zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
  | add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
  | mem i₁' m₁' hm₁ =>
    obtain ⟨i₁n, rfl⟩ := i₁'
    dsimp only at *
    induction hm₁ using Submodule.pow_induction_on_left' with
    | algebraMap =>
      rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
    | add _ _ _ _ _ ihx ihy =>
      rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
    | mem_mul m₁ hm₁ i x₁ _hx₁ ih₁ =>
      obtain ⟨v₁, rfl⟩ := hm₁
      -- This is the first interesting goal.
      rw [map_mul, mul_assoc, ih₁, mul_smul_comm, map_apply_ι, Nat.cast_succ, mul_add_one,
        uzpow_add, mul_smul, ← mul_assoc, ← mul_assoc, ← smul_mul_assoc ((-1) ^ i₂)]
      clear ih₁
      congr 2
      induction hm₂ using Submodule.iSup_induction' with
      | zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
      | add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
      | mem i₂' m₂' hm₂ =>
        clear m₂
        obtain ⟨i₂n, rfl⟩ := i₂'
        dsimp only at *
        induction hm₂ using Submodule.pow_induction_on_left' with
        | algebraMap =>
          rw [AlgHom.commutes, Nat.cast_zero, uzpow_zero, one_smul, Algebra.commutes]
        | add _ _ _ _ _ ihx ihy =>
          rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
        | mem_mul m₂ hm₂ i x₂ _hx₂ ih₂ =>
          obtain ⟨v₂, rfl⟩ := hm₂
          -- This is the second interesting goal.
          rw [map_mul, map_apply_ι, Nat.cast_succ, ← mul_assoc,
            ι_mul_ι_comm_of_isOrtho (hf _ _), neg_mul, mul_assoc, ih₂, mul_smul_comm,
            ← mul_assoc, ← Units.neg_smul, uzpow_add, uzpow_one, mul_neg_one]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
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
⊢ (LinearMap.mul' R C)
      ((TensorProduct.map f.toLinearMap g.toLinearMap)
        ((of R 𝒜 ℬ).symm (↑((-1) ^ (j₁ * i₂)) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)))) =
    f a₁ * g ↑b₁ * (f ↑a₂ * g b₂)

Tactic:
← Int.cast_smul_eq_zsmul R,

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
⊢ (LinearMap.mul' R C)
      ((TensorProduct.map f.toLinearMap g.toLinearMap)
        ((of R 𝒜 ℬ).symm (↑↑((-1) ^ (j₁ * i₂)) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)))) =
    f a₁ * g ↑b₁ * (f ↑a₂ * g b₂)
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
φ : { φ // ∀ (g : G), n • φ g = 0 }
⊢ ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup ≤ (↑φ).ker

Tactic:
rintro - ⟨g, rfl⟩

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
φ : { φ // ∀ (g : G), n • φ g = 0 }
g : G
⊢ ((LinearMap.lsmul ℤ G) ↑n) g ∈ (↑φ).ker
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

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

Tactic:
by_cases hfg : f.Injective ∧ g.Injective

Goal state after:
case pos
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
hfg : Function.Injective f ∧ Function.Injective g
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

case neg
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
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A i j| ≤ |m|

Tactic:
fin_cases i

Goal state after:
case «0»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i ↦ i) ⟨0, ⋯⟩) j| ≤ |m|

case «1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ |m|
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
x✝ : ℕ
⊢ Aᵀ.den ∣ x✝ ↔ A.den ∣ x✝

Tactic:
by simpa [den_dvd_iff] using forall_comm

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✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n

Tactic:
have := congr_arg det hA.mul_conjTranspose
  rwa [det_mul, det_conjTranspose, det_smul, det_one, mul_one] at this

Goal state after:
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
i j : Fin 2
⊢ ↑A i j = ↑1 i j

Tactic:
fin_cases i

Goal state after:
case «0»
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
j : Fin 2
⊢ ↑A ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑1 ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
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
j : Fin 2
⊢ ↑A ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑1 ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: n : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_4
inst✝ : CommRing R
A : Matrix n n R
⊢ A.Nonsingular ↔ A.det ∈ nonZeroDivisors R

Tactic:
by
  simp_rw [Nonsingular, isDetpBalanced_iff_sub_mul_det_eq_zero, mem_nonZeroDivisors_iff_right]
  exact ⟨fun h x eq ↦ h x 0 (by simpa), fun h a b eq ↦ sub_eq_zero.mp <| h _ (by simpa)⟩

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Function.LeftInverse (fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val fun x ↦ 0)

Tactic:
intro x; aesop

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Function.RightInverse (fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val fun x ↦ 0)

Tactic:
intro x; aesop

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
⊢ ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ ∅ ⊆ ↑M

Tactic:
use ⊥

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 ↥(Subspace.submodule ⊥) ≤ 2 ∧ ∅ ⊆ ↑⊥
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
i j : Fin 2
hij : i ≠ j
c : F
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
fin_cases i

Goal state after:
case «0»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

case «1»
F : Type u_2
inst✝ : Field F
j : Fin 2
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : Matrix.SpecialLinearGroup ι F
H : Subgroup (Matrix.SpecialLinearGroup ι F)
x : Matrix.SpecialLinearGroup ι F ⧸ Subgroup.center (Matrix.SpecialLinearGroup ι F)
x✝ : ∃ x_1 ∈ H, ↑x_1 = (↑g)⁻¹ * x * ↑g
a : Matrix.SpecialLinearGroup ι F
ha : a ∈ H
hx : ↑a = (↑g)⁻¹ * x * ↑g
⊢ ↑(g * a * g⁻¹) = x

Tactic:
simp [hx, mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
A : SpecialLinearGroup R V
⊢ LinearMap.det ↑↑A = 1

Tactic:
simp [← LinearEquiv.coe_det, A.prop]

Goal state after: