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

Goal state before:
pp: 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
i : Fin n
⊢ 1 • b i = b i

Tactic:
one_smul

Goal state after:
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
i : Fin n
⊢ b i = b i
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

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 b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - 1 • b) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

Tactic:
one_smul

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 b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

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
inst✝ : Invertible 2
m : M
h : IsUnit ((ι Q) m)
⊢ IsUnit (Q m)

Tactic:
by
  cases h.nonempty_invertible
  let := invertibleOfInvertibleι Q m
  exact isUnit_of_invertible (Q m)

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

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
⊢ LinearEquiv.det (LinearEquiv.transvection hfv) = 1

Tactic:
by
  rw [← Units.val_inj, LinearEquiv.coe_det,
    LinearEquiv.transvection.coe_toLinearMap hfv, Units.val_one]
  by_contra! h
  have : Free R V := Free.of_det_ne_one h
  have : Module.Finite R V := finite_of_det_ne_one h
  apply h
  rw [transvection.det, hfv, add_zero]

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)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ (1 • (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:
one_smul

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✝ : ι × ι
⊢ ((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.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)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ 1 • (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a = (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Tactic:
one_smul

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)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a = (lof R ι ℬ 0) 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)
a : 𝒜 0
b✝ : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
⊢ 1 • (lof R ι ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0) a = (lof R ι ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0) a

Tactic:
one_smul

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)
a : 𝒜 0
b✝ : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
⊢ (lof R ι ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0) a = (lof R ι ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0) 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 ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ 1 • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂) = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
one_smul

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 ℤˣ)
i₂ : ι
a₁ : A
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂) = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
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₁)
a₂ : ↥(𝒜 0)
b₂ : B
⊢ 1 • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂) = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
one_smul

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₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
⊢ (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂) = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
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 ℤˣ)
⊢ ∀ (x y : B),
    { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
      { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } x *
        { toFun := fun b ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } y

Tactic:
rw [LinearMap.map_mul_iff]
      refine DirectSum.decompose_lhom_ext ℬ fun i₁ => ?_
      ext b₁ b₂ : 2
      dsimp
      rw [tmul_coe_mul_one_tmul]

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
m : M₁ × M₂
⊢ (((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
              (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯).coprod
          ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯))
        m *
      (((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
              (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯).coprod
          ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯))
        m =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) ((QuadraticMap.prod Q₁ Q₂) m)

Tactic:
simp_rw [LinearMap.coprod_apply, LinearMap.coe_comp, Function.comp_apply,
        AlgHom.toLinearMap_apply, QuadraticMap.prod_apply, Submodule.coe_subtype,
        GradedTensorProduct.includeLeft_apply, GradedTensorProduct.includeRight_apply, map_add,
        add_mul, mul_add, GradedTensorProduct.algebraMap_def,
        GradedTensorProduct.tmul_one_mul_one_tmul, GradedTensorProduct.tmul_one_mul_coe_tmul,
        GradedTensorProduct.tmul_coe_mul_one_tmul, GradedTensorProduct.tmul_coe_mul_coe_tmul,
        LinearMap.codRestrict_apply, one_mul, uzpow_one, Units.neg_smul, one_smul, ι_sq_scalar,
        mul_one, ← GradedTensorProduct.algebraMap_def, ← GradedTensorProduct.algebraMap_def']
      abel

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
⊢ 1 • (f a₁ * (g ↑b₁ * f ↑a₂) * g b₂) = f a₁ * (g ↑b₁ * f ↑a₂) * g b₂

Tactic:
one_smul

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 : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] ↑b) = 1 • F (↑a ᵍ⊗ₜ[R] ↑b)

Tactic:
one_smul

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 : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] ↑b) = F (↑a ᵍ⊗ₜ[R] ↑b)
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
n m : ℕ
h : n = m
x : ⨂[R]^n M
⊢ GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x ↦ M) (finCongr h)) x) = GradedMonoid.mk n x

Tactic:
rw [finCongr_eq_equivCast, mk_reindex_cast h]

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
n : ℕ
x : Fin n → M
⊢ (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)

Tactic:
refine Fin.consInduction ?_ ?_ x <;> clear x
  · rw [List.finRange_zero, List.map_nil, List.prod_nil]
    rfl
  · intro n x₀ x ih
    rw [List.finRange_succ, List.map_cons, List.prod_cons, List.map_map]
    simp_rw [Function.comp_def, Fin.cons_zero, Fin.cons_succ]
    rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod]
    refine TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) ?_
    dsimp only [GradedMonoid.mk]
    rw [TensorPower.cast_tprod]
    simp_rw [Fin.append_left_eq_cons, Function.comp_def]
    congr 1 with i

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
n : ℕ
x : Fin n → M
⊢ (List.ofFn fun x_1 ↦ (DirectSum.of (fun n ↦ ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_2 ↦ x x_1)).prod =
    (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
DirectSum.list_prod_ofFn_of_eq_dProd

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (DirectSum.of (fun n ↦ ⨂[R]^n M) ((List.finRange n).dProdIndex fun x ↦ 1))
      ((List.finRange n).dProd (fun x ↦ 1) fun x_1 ↦ (PiTensorProduct.tprod R) fun x_2 ↦ x x_1) =
    (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
⊢ ∑ _σ, ∏ _i, x = (Fintype.card n)! • x ^ Fintype.card n

Tactic:
simp [Fintype.card_perm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
c : ι → R
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x
y : S
hy : ∀ (k : ι), abv (c k) ≤ y
⊢ abv (∑ k ∈ s, c k • A k).det ≤ (Fintype.card n)! • (#s • y * x) ^ Fintype.card n

Tactic:
simpa only [smul_mul_assoc] using!
    det_sum_le s fun k i j =>
      calc
        abv (c k * A k i j) = abv (c k) * abv (A k i j) := abv.map_mul _ _
        _ ≤ y * x := mul_le_mul (hy k) (hx k i j) (abv.nonneg _) ((abv.nonneg _).trans (hy k))

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix (Fin.succAbove 0) id).det = 1 • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
one_smul

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix (Fin.succAbove 0) id).det = (M.submatrix (Fin.succAbove 0) id).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: 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
⊢ (∀ (x : Fin (k + 1)), (f x).isRight = false) → ∃ f', f = Sum.inl ∘ f'

Tactic:
Sum.isRight_eq_false,

Goal state after:
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
⊢ (∀ (x : Fin (k + 1)), (f x).isLeft = true) → ∃ f', f = Sum.inl ∘ f'
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j * (v i)⁻¹‖ ≤ 1

Tactic:
rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr h_nz), one_mul]
      exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)

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|
⊢ A = 1

Tactic:
by
  have := Int.mul_eq_one_iff_eq_one_or_neg_one.mp (A_c_eq_zero a1)
  ext i j
  fin_cases i <;> fin_cases j <;> aesop

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Finite ι
b : (i : ι) → Basis (κ i) R (M i)
p : (i : ι) → κ i
⊢ (piTensorProduct b) p = ⨂ₜ[R] (i : ι), (b i) (p i)

Tactic:
have := Fintype.ofFinite ι
  classical
  refine (Basis.piTensorProduct b).ext_elem (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : MultilinearMap R M N
h : ∀ (j : (i : ι) → γ i), (φ fun i ↦ g (j i)) = φ' fun i ↦ g (j i)
⊢ φ = φ'

Tactic:
suffices lift φ = lift φ' by
    ext m
    simpa using DFunLike.congr_fun this (tprod _ m)

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : MultilinearMap R M N
h : ∀ (j : (i : ι) → γ i), (φ fun i ↦ g (j i)) = φ' fun i ↦ g (j i)
⊢ lift φ = lift φ'
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
x : ι → R
⊢ (constantBaseRingEquiv ι R) ((tprod R) x) = ∏ i, x i

Tactic:
simp [constantBaseRingEquiv]

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

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this✝¹ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this✝ : Infinite (ℙ k V)
this : n = 0
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
simp [this]

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

Goal state before:
pp: case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
y : V
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ 0 + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

Tactic:
rwa [zero_add]

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

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

Tactic:
tauto

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

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

Tactic:
tauto

Goal state after:
case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
t✝ : Set SL(2, F)
a✝ : t✝ ∈ Set.range fun S ↦ ⋂ (_ : S ∈ {x | lineStab (F ∙ Pi.single 0 1) ≤ x ∧ lineStab (F ∙ Pi.single 1 1) ≤ x}), ↑S
⊢ SpecialLinearGroup.transvection hij c ∈ t✝
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

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

Tactic:
tauto

Goal state after:
case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
t✝ : Set SL(2, F)
a✝ : t✝ ∈ Set.range fun S ↦ ⋂ (_ : S ∈ {x | lineStab (F ∙ Pi.single 0 1) ≤ x ∧ lineStab (F ∙ Pi.single 1 1) ≤ x}), ↑S
⊢ SpecialLinearGroup.transvection hij c ∈ t✝
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

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

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
g_SL : SL(2, F)
⊢ PSL.iwasawaT (↑g_SL • p) = MulAut.conj ↑g_SL • PSL.iwasawaT p

Tactic:
rw [Matrix.ProjectiveSpecialLinearGroup.smul_proj_mk]

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
g_SL : SL(2, F)
⊢ PSL.iwasawaT (g_SL • p) = MulAut.conj ↑g_SL • PSL.iwasawaT p
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A B : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), A • w - w ∈ L
hB : ∀ (w : ι → F), B • w - w ∈ L
w : ι → F
⊢ A • (B • w - w) - (B • w - w) + (B • w - w) + (A • w - w) ∈ L

Tactic:
exact add_mem (add_mem (hA _) (hB w)) (hA w)

Goal state after: