mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: case e_a
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₂
⊢ 1 * (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂)) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))

Tactic:
one_mul

Goal state after:
case e_a
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₂
⊢ (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂)) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))
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)
⊢ (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) 1 = 1

Tactic:
by
      dsimp [Algebra.TensorProduct.one_def]
      simp only [map_one, mul_one]

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 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:
finCongr_eq_equivCast,

Goal state after:
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) (Equiv.cast ⋯)) x) = GradedMonoid.mk n x
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

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

Tactic:
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : ∀ (b : ι), ↑n ∣ (f x) b
⊢ x ∈ nG

Tactic:
choose c hc using hx

Goal state after:
case refine_1
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
c : ι → ℤ
hc : ∀ (b : ι), (f x) b = ↑n * c b
⊢ x ∈ nG
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
i : I
a : A i
⊢ (((f ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} ↦ maps) ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a

Tactic:
simp_rw [AlgHom.ext_iff] at h

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : ∀ (i : I) (x : A i), (f ∘ₐ ι R A i) x = maps x
⊢ (((f ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a =
    (((((lift R A) fun {i} ↦ maps) ∘ₐ RingCon.mkₐ R (ringCon R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ
        DirectSum.lof R I A i)
      a
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast

Tactic:
rw [isTotallyUnimodular_iff] at hA
  simpa using hA 1 (fun _ => i) (fun _ => j)

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

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast

Tactic:
by
  rw [isTotallyUnimodular_iff] at hA
  simpa using hA 1 (fun _ => i) (fun _ => j)

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A

Tactic:
if_pos hc,

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A) =
    (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A

Tactic:
if_pos hc,

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ (if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A) =
    T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
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:
norm_mul,

Goal state after:
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
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‖ ≤ 1 * ‖v i‖

Tactic:
one_mul

Goal state after:
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‖
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T • B) ↔ C B

Tactic:
refine ⟨?_, hT _⟩

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T • B) → C B
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ.mpr
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 := ⋯
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ Nonempty { p // p.length = m + 1 } → 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j

Tactic:
rintro ⟨p, hp_len⟩
      cases p with
      | nil => simp [Quiver.Path.length] at hp_len
      | @cons b _ q e =>
        simp only [Quiver.Path.length_cons, Nat.succ.injEq] at hp_len
        have h_Am_pos : 0 < (A ^ m) i b := (ih i b).mpr ⟨q, hp_len⟩
        let h_A_pos := e
        have h_prod : 0 < (A ^ m) i b * A b j := mul_pos h_Am_pos h_A_pos.down
        exact
          (Finset.sum_pos_iff_of_nonneg
            (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))).2
            ⟨b, Finset.mem_univ b, h_prod⟩

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:
by
  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.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • (1 * x) = r • x

Tactic:
one_mul

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • x
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • (1 * x)

Tactic:
one_mul

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • x
Module: Mathlib.LinearAlgebra.Projectivization.Independence

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

Tactic:
convert! Independent.mk _ _ h
    · simp only [mk_rep, Function.comp_apply]
    · intro i
      apply rep_nonzero

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

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

Tactic:
· convert! Independent.mk _ _ h
    · simp only [mk_rep, Function.comp_apply]
    · intro i
      apply rep_nonzero

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

Goal state before:
pp: F : Type u_2
inst✝ : Field F
t : TransvectionStruct (Fin 2) F
⊢ t.toSpecialLinearGroup ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
obtain ⟨i, j, hij, c⟩ := t
  simp only [Fin.isValue, TransvectionStruct.toSpecialLinearGroup_mk]
  fin_cases i <;> fin_cases j <;> try tauto
  · exact Subgroup.mem_sup_left <| transvection_mem_lineStab zero_ne_one c
  · exact Subgroup.mem_sup_right <| transvection_mem_lineStab one_ne_zero c

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
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
⊢ LinearEquiv.det (e ≪≫ₗ ↑g ≪≫ₗ e.symm) = 1

Tactic:
← LinearEquiv.symm_symm e

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
⊢ LinearEquiv.det (e.symm.symm ≪≫ₗ ↑g ≪≫ₗ e.symm) = 1
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
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Subgroup.center (SpecialLinearGroup R V) = ⊥

Tactic:
have : Subsingleton (Module.Free.ChooseBasisIndex R V) := by
    rwa [← Finite.card_le_one_iff_subsingleton,
      Nat.card_eq_fintype_card, ← Module.finrank_eq_card_basis b]

Goal state after:
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
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Subsingleton (Module.Free.ChooseBasisIndex R V)
⊢ Subgroup.center (SpecialLinearGroup R V) = ⊥
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
v : ι → K
hv : ¬v = 0
⊢ ¬LinearIndependent K ![v, f v]

Tactic:
simpa [LinearIndependent.pair_iff' hv, mk_eq_mk_iff'] using! hm (.mk K v hv)

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

Goal state before:
pp: case refine_2.h
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
v : ι → K
hv : v ≠ 0
⊢ ∃ a, a • v = m • v

Tactic:
use r

Goal state after:
case h
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
v : ι → K
hv : v ≠ 0
⊢ r • v = m • v
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ (bm.repr x).support.offDiag,
        if x_1.1 = x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • Q (bm x_1.1)
        else if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Tactic:
rw [Finset.sum_ite_of_false, QuadraticMap.map_sum, ← Finset.sum_filter]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ a ∈ (bm.repr x).support.offDiag with a.1 < a.2,
        (bm.repr x) a.1 • (bm.repr x) a.2 • polar (⇑Q) (bm a.1) (bm a.2) =
    ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) +
      ∑ ij ∈ (bm.repr x).support.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map (fun a ↦ (bm.repr x) a • bm a) ij)

case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : Subsingleton R
⊢ 1 = r

pp: case pos
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r

pp: case neg
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r

Tactic:
· simp [Subsingleton.eq_one r]

Goal state after:
case pos
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ 1 = r

case neg
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ⟨⋯.unit, ⋯⟩ = r
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)

Tactic:
by
  nontriviality R
  by_cases hV : Subsingleton V
  · convert! Eq.refl (1 : Rˣ) <;>
    · apply rootsOfUnity.eq_one
      rw [← Module.finrank_eq_zero_iff_of_free (R := R)] at hV
      simp only [hV, sup_eq_right, zero_le_one, ← Module.finrank_eq_card_basis b]
  · have hι : ¬ IsEmpty ι := fun hι ↦ hV (by
      rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty])
    rw [not_subsingleton_iff_nontrivial] at hV
    have := Module.Free.instFaithfulSMulOfNontrivial R V
    suffices (((((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans
      centerEquivRootsOfUnity g).val : R) • LinearMap.id) : V →ₗ[R] V) =
        ((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g).val : R) • LinearMap.id by
      rw [← Units.val_inj]
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp only [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this
      rw [MulEquiv.trans_apply, this]
    simp only [MulEquiv.trans_apply]
    have hgg' := Subgroup.centerCongr_apply_coe (Matrix.SpecialLinearGroup.toLin_equiv b) g
    rw [← Subtype.coe_inj, ← LinearEquiv.toLinearMap_inj, LinearMap.ext_iff] at hgg'
    set g' := ((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)) g)
    ext x
    have := centerEquivRootsOfUnity_apply_apply g' x
    simp only [Subgroup.smul_def, Units.smul_def] at this
    simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq]
    rw [this, ← LinearEquiv.coe_toLinearMap, hgg',
      Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq,
      Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity g,
      Matrix.toLin_scalar]
    simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
a : R
x : M
hx : x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
⊢ a • x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}

Tactic:
by simp [QuadraticMap.map_smul, hx.1, hx.2]

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : ¬w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))

Tactic:
simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
⊢ h i ∈ ↑(Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R).range

Tactic:
h_eq_diagonal

Goal state after:
ι : 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✝ : DecidableEq ι
i : ↥b.support
⊢ Matrix.diagonal (0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑i)) ∈ ↑(Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R).range