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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v w : V
hv : f v = 0
hw : f w = 0
hvw : f (v + w) = 0
⊢ transvection hw ≪≫ₗ transvection hv = transvection hvw

Tactic:
by
  ext; simp [comp_of_left_eq_apply hw]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hf : f v = 0
hf' : (-f) v = 0
⊢ (transvection hf).symm = transvection hf'

Tactic:
by
  ext; simp [symm_apply_eq, comp_of_right_eq_apply hf]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
this : (b.coord i) (f (b i)) * 1 = 1 * (b.coord j) (f (b j))
⊢ f (b j) = (b.coord i) (f (b i)) • b j

Tactic:
simp only [mul_one, one_mul] at this

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
this : (b.coord i) (f (b i)) = (b.coord j) (f (b j))
⊢ f (b j) = (b.coord i) (f (b i)) • b j
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
⊢ ∃ a, f = a • 1

Tactic:
have ha (r) : Commute (b.coord i (f (b i))) r := by
    obtain ⟨j, hij⟩ := exists_ne i
    rw [commute_iff_eq, h' i j (Ne.symm hij), feq i j, feq i i]
    simp

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i) (f (b i))) r
⊢ ∃ a, f = a • 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case mpr
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u = ↑e - LinearMap.id
⊢ ∃ f v, ↑e = LinearMap.transvection f v

Tactic:
rw [eq_sub_iff_add_eq] at hu

Goal state after:
case mpr
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
⊢ ∃ f v, ↑e = LinearMap.transvection f v
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ polarBilin (QuadraticForm.baseChange A Q) = BilinForm.baseChange A (polarBilin Q)

Tactic:
rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul,
    ← map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq,
    smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul]

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

Goal state before:
pp: case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
⊢ e ∈ transvections K V

Tactic:
set v := (f w)⁻¹ • (e w - w)

Goal state after:
case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
⊢ e ∈ transvections K V
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x

Tactic:
induction x using CliffordAlgebra.left_induction with
      | algebraMap => simp_rw [foldr'_algebraMap, smul_zero, zero_add]
      | add _ _ hx hy => rw [map_add, map_add, map_add, add_add_add_comm, hx, hy]
      | ι_mul _ _ hx =>
        rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]

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

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) ((ι Q) m✝ * x✝) = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) ((ι Q) m✝ * x✝)

Tactic:
rw [foldr'_ι_mul, foldr'_ι_mul, hx]
        dsimp only [contractLeftAux_apply_apply]
        rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]

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

Goal state before:
pp: ⊢ ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)

Tactic:
ext
  dsimp only [LinearMap.comp_apply, Subtype.coe_mk, AlgHom.id_apply, AlgHom.toLinearMap_apply,
    AlgHom.comp_apply]
  rw [toComplex_ι, one_smul, ofComplex_I]

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 : EvenHom Q A
m₁ m₂ : M
a : A × ↥(S f)
m₃ : M
⊢ (f.bilin m₃) (m₁ + m₂) * a.1 = (f.bilin m₃) m₁ * a.1 + (f.bilin m₃) m₂ * a.1

Tactic:
rw [map_add, add_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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (((TensorProduct.directSum R R 𝒜 ℬ).trans
            (LinearEquiv.ofLinearMap (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).trans
        (TensorProduct.directSum R R ℬ 𝒜).symm)
      ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j) b) =
    (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Tactic:
dsimp only [LinearEquiv.trans_apply, LinearEquiv.coe_ofLinearMap]

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
      ((gradedCommAux R 𝒜 ℬ) ((TensorProduct.directSum R R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j) b))) =
    (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h' : Module.rank R M ≠ 0
⊢ False

Tactic:
obtain ⟨f, hf⟩ := by rwa [← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at h'

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h' : Module.rank R M ≠ 0
f : R →ₗ[R] M
hf : Function.Injective ⇑f
⊢ False
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']

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₂
⊢ (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1) + (ι Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂) m.2 +
      (-(ι Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂) m.2 + (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₂ m.2)) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₁ m.1) + (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) (Q₂ m.2)
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
f : ModN G n →+ M
g : G
Gn : AddSubgroup G := ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup
this : n • g ∈ (QuotientAddGroup.mk' Gn).ker
⊢ n • (f.comp (QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup)) g = 0

Tactic:
simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]
      change f (QuotientAddGroup.mk' Gn (n • g)) = 0 -- Can we avoid `change`?
      rw [this, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
⊢ (Pi.algebraMap ι' R K).ker = ⊥

Tactic:
Submodule.eq_bot_iff

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
⊢ ∀ x ∈ (Pi.algebraMap ι' R K).ker, x = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

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

pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j, Mᵀ j = 0

Tactic:
transpose_transpose

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det =
    (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j, Mᵀ j = 0
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case zero.refine_2
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j : n
x✝ : Nonempty { p // p.length = 0 }
p : Path i j
hp : p.length = 0
⊢ 0 < (A ^ 0) i j

Tactic:
· simp [Quiver.Path.eq_of_length_zero p hp]

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

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✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
⊢ (lift ((MultilinearMap.fromDFinsuppEquiv κ R) fun p ↦ (DFinsupp.lsingle p).compMultilinearMap (tprod R)) ∘ₗ
      (DFinsupp.lsum R) fun p ↦ lift ((map fun i ↦ DFinsupp.lsingle (p i)).compMultilinearMap (tprod R))) =
    LinearMap.id

Tactic:
ext p x; simp

Goal state after:
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)
inst✝ : DecidableEq ι
i : ι
r : R
⊢ tprodCoeff R 1 ((MonoidHom.mulSingle A i) ((algebraMap R (A i)) r)) = r • tprodCoeff R 1 1

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← Pi.one_apply, MonoidHom.mulSingle_apply, Pi.mulSingle,
      smul_tprodCoeff]
    rfl

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)
this : lift φ = lift φ'
⊢ φ = φ'

Tactic:
ext m
    simpa using DFunLike.congr_fun this (tprod _ m)

Goal state after:
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✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv ((tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) =
    (lof R ((i : ι) → κ i) (fun i ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p) ((tprod R) fun i ↦ x i)

Tactic:
convert! ofDFinsuppEquiv_tprod_single p x

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

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : ¬mk K v hv = mk K w hw
⊢ IsCollinear {mk K v hv, mk K w hw}

Tactic:
| h w hw =>

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

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
v : V
hv : v ≠ 0
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
w : V
hw : w ≠ 0
hp3 : mk K w hw ∈ Submodule.projectivization p
hq3 : mk K w hw ∈ Submodule.projectivization q
hxy : mk K v hv ≠ mk K w hw
⊢ p = q

Tactic:
| h w hw =>

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

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

Tactic:
obtain ⟨a, ha, hasq⟩ := hF

Goal state after:
F : Type u_2
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
⊢ commutator PSL(2, F) = ⊤
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + A • w - w = B • α • v + B • w - w

Tactic:
← add_sub,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + (A • w - w) = B • α • v + B • w - w
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ A • β • v + α • v = B • α • v + B • w - w

Tactic:
← add_sub,

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

Tactic:
Submodule.eq_bot_iff

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 ∈ W, x = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case smul
ι : 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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
t : R
u : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx✝ : u ∈ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)
hu : (ωConj b) u ∈ lieAlgebra b
⊢ (ωConj b) (t • u) ∈ lieAlgebra b

Tactic:
simpa using SMulMemClass.smul_mem _ hu

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -3
⊢ False

Tactic:
rw [hA] at h₀ h₁ h₂ h₃

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + -3 * y = -3 ∨ 2 * x + -3 * y = -1 ∨ 2 * x + -3 * y = 0 ∨ 2 * x + -3 * y = 1 ∨ 2 * x + -3 * y = 3
h₁ :
  2 * (x + 1) + -3 * y = -3 ∨
    2 * (x + 1) + -3 * y = -1 ∨ 2 * (x + 1) + -3 * y = 0 ∨ 2 * (x + 1) + -3 * y = 1 ∨ 2 * (x + 1) + -3 * y = 3
h₂ :
  2 * x + -3 * (y - 1) = -3 ∨
    2 * x + -3 * (y - 1) = -1 ∨ 2 * x + -3 * (y - 1) = 0 ∨ 2 * x + -3 * (y - 1) = 1 ∨ 2 * x + -3 * (y - 1) = 3
h₃ :
  2 * (x + 1) + -3 * (y - 1) = -3 ∨
    2 * (x + 1) + -3 * (y - 1) = -1 ∨
      2 * (x + 1) + -3 * (y - 1) = 0 ∨ 2 * (x + 1) + -3 * (y - 1) = 1 ∨ 2 * (x + 1) + -3 * (y - 1) = 3
hA : A = -3
⊢ False