mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Monoid β
inst✝² : MulAction β α
inst✝¹ : Mul α
inst✝ : SMulCommClass β α α
⊢ ∀ (m_1 : β) (n_1 a : WithConv (Matrix m n α)), m_1 • n_1 • a = n_1 • m_1 • a

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Monoid β
inst✝² : MulAction β α
inst✝¹ : Mul α
inst✝ : IsScalarTower β α α
⊢ ∀ (x : β) (y z : WithConv (Matrix m n α)), (x • y) • z = x • y • z

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : CommSemiring α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝² x✝¹ : WithConv (Matrix m n α)
i✝ : n
x✝ : m
⊢ (((↑(congrLinearEquiv toLin')).toFun (x✝² * x✝¹)).ofConv ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝ =
    (((↑(congrLinearEquiv toLin')).toFun x✝² * (↑(congrLinearEquiv toLin')).toFun x✝¹).ofConv ∘ₗ
        LinearMap.single α (fun i ↦ α) i✝)
      1 x✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x y : Matrix m n α
i✝ : n
x✝ : m
⊢ (toLin' (x ⊙ y) ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝ =
    ((toConv (toLin' x) * toConv (toLin' y)).ofConv ∘ₗ LinearMap.single α (fun i ↦ α) i✝) 1 x✝

Tactic:
simp

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)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
i✝ : (i : ι) → κ 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))) ∘ₗ
              DFinsupp.lsingle p).compMultilinearMap
          (tprod R))
        x)
      i✝ =
    (((LinearMap.id ∘ₗ DFinsupp.lsingle p).compMultilinearMap (tprod R)) x) i✝

Tactic:
simp

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

Tactic:
simp

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✝ : Fintype ι
b : (i : ι) → Basis (κ i) R (M i)
x : (i : ι) → M i
p : (i : ι) → κ i
⊢ ((Finsupp.basisSingleOne.map
            (((PiTensorProduct.congr fun i ↦ (b i).repr).trans ofFinsuppEquiv).trans
                (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) ↑(constantBaseRingEquiv ι R))).symm).repr
        ((tprod R) x))
      p =
    ∏ i, ((b i).repr (x i)) (p i)

Tactic:
simp

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

Goal state before:
pp: case e_n
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
this :
  (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
⊢ (subsingletonEquiv ())
      ((tprod R) fun i₂ ↦
        m ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm (Sum.inr i₂)))) =
    m i₀

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
f : (i : ι) → Dual R (M i)
m : (i : ι) → M i
⊢ ((compRight R (constantBaseRingEquiv ι R).toLinearMap ∘ₗ piTensorHomMap) ((tprod R) fun i ↦ f i))
      (⨂ₜ[R] (i : ι), m i) =
    ∏ i, (f i) (m i)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
x✝ : (i : ι) → M i
⊢ (φ.compMultilinearMap (tprod R)) x✝ = (((φ ∘ₗ ↑e.symm) ∘ₗ ↑e).compMultilinearMap (tprod R)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), (ψ ∘ₗ ↑e) (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
x✝ : (i : ι) → M i
⊢ (φ'.compMultilinearMap (tprod R)) x✝ = (((φ' ∘ₗ ↑e.symm) ∘ₗ ↑e).compMultilinearMap (tprod R)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case smul_tprod
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r✝ : R
f✝ : (i : ι) → A i
⊢ (mul ((tprod R) 1)) (r✝ • (tprod R) f✝) = r✝ • (tprod R) f✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case smul_tprod
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r✝ : R
f✝ : (i : ι) → A i
⊢ (mul (r✝ • (tprod R) f✝)) ((tprod R) 1) = r✝ • (tprod R) f✝

Tactic:
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)
⊢ 1 • 1 = 1

Tactic:
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)
⊢ 0 • 1 = 0

Tactic:
simp

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

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h : Infinite k
this : Infinite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
simp

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

Goal state before:
pp: case inl.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Infinite V
this✝ : Infinite (ℙ k V) ↔ Infinite V
this : Infinite (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
simp

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
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
⊢ Fintype.card { v // v ≠ 0 } = Fintype.card V - 1

Tactic:
simp

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

Goal state before:
pp: k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
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
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ ↑(Nat.card k ^ n - 1) = ↑(Nat.card k) ^ n - 1

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D✝ D'✝ E E' : ℙ K V
hD✝ : D✝ ≠ D'✝
hE : E ≠ E'
D D' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
⊢ ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
D✝ D'✝ E E' : ℙ K V
hD✝ : D✝ ≠ D'✝
hE : E ≠ E'
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
D D' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
⊢ ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep

Tactic:
simp

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

Goal state before:
pp: case mk.mk
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
carrier✝¹ : Set (ℙ K V)
mem_add'✝¹ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝¹ →
      Projectivization.mk K w hw ∈ carrier✝¹ → Projectivization.mk K (v + w) hvw ∈ carrier✝¹
carrier✝ : Set (ℙ K V)
mem_add'✝ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝ →
      Projectivization.mk K w hw ∈ carrier✝ → Projectivization.mk K (v + w) hvw ∈ carrier✝
⊢ { carrier := carrier✝¹, mem_add' := mem_add'✝¹ }.carrier = { carrier := carrier✝, mem_add' := mem_add'✝ }.carrier →
    { carrier := carrier✝¹, mem_add' := mem_add'✝¹ } = { carrier := carrier✝, mem_add' := mem_add'✝ }

Tactic:
simp

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.rank K ↥⊥ ≤ 2 ∧ ∅ ⊆ ↑⊥

Tactic:
simp

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD✝ : D ≠ D'
hE✝ : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
h : V ≃ₗ[K] V
hdet : LinearEquiv.det h = (LinearEquiv.det g)⁻¹
hD : h • D = D
hE : h • D' = D'
⊢ ⟨g * h, ⋯⟩ • D = E ∧ ⟨g * h, ⋯⟩ • D' = E'

Tactic:
simp [specialLinearGroup_smul_def, toLinearEquiv_eq_coe, mul_smul, gD, hD, gE, hE]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
⊢ D.rep ∈ {D.rep, D'.rep}

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
⊢ D'.rep ∈ {D.rep, D'.rep}

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ IsUnit (1 + (b.coord ⟨D.rep, hD_mem⟩) ((↑a - 1) • b ⟨D.rep, hD_mem⟩))

Tactic:
simp

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

Goal state before:
pp: case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 0 1) ≤ ⨆ p, lineStab p.submodule

Tactic:
rw [← Projectivization.submodule_mk (K := F) _ (Pi.single_ne_zero_iff.2 one_ne_zero)]

Goal state after:
case refine_1
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 0 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (F ∙ Pi.single 1 1) ≤ ⨆ p, lineStab p.submodule

Tactic:
rw [← Projectivization.submodule_mk (K := F) _ (Pi.single_ne_zero_iff.2 one_ne_zero)]

Goal state after:
case refine_2
F : Type u_2
inst✝ : Field F
⊢ lineStab (Projectivization.mk F (Pi.single 1 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule
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)
⊢ 1 ∈ {A | ∀ (w : ι → F), A • w - w ∈ L}

Tactic:
simp

Goal state after:
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
p : ℙ F (ι → F)
⊢ (g • p).submodule = g • p.submodule

Tactic:
induction p using Projectivization.ind with

Goal state after:
case h
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : Matrix.SpecialLinearGroup ι F
v : ι → F
hv : v ≠ 0
⊢ (g • Projectivization.mk F v hv).submodule = g • (Projectivization.mk F v hv).submodule
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 : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), (g⁻¹ * A * g) • w - w ∈ L
w : ι → F
⊢ g • g⁻¹ • (A • w - w) = A • w - w

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → Kˣ
x✝ : ι
⊢ (if ↑(w x✝) = 0 then 0 else 1) = 1 x✝

Tactic:
simp

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
⊢ LinearEquiv.det 1 = 1

Tactic:
simp

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (Finsupp.single ⟨D.rep, hD_mem⟩ 1) ⟨D.rep, hD_mem⟩ = 1

Tactic:
simp

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
⊢ ↑⟨LinearEquiv.baseChange R S V V ↑1, ⋯⟩ = ↑1

Tactic:
simp

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
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
A B : SpecialLinearGroup n R
⊢ (fun a ↦ ↑a) ⟨toLin' (A * B), ⋯⟩ = (fun a ↦ ↑a) (⟨toLin' A, ⋯⟩ * ⟨toLin' B, ⋯⟩)

Tactic:
simp

Goal state after:
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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support, 0 • (⇑Q ∘ g) i = 0

Tactic:
simp

Goal state after:
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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support.sym2, 0 • (polarSym2 ⇑Q ∘ Sym2.map g) i = 0

Tactic:
simp

Goal state after:
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✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support, 0 • (⇑Q ∘ g) i = 0

Tactic:
simp

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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ ⟨LinearMap.equivOfIsUnitDet ⋯, ⋯⟩ ∈ Subgroup.center (SpecialLinearGroup R V)

Tactic:
simp only [mem_center_iff, LinearMap.coe_equivOfIsUnitDet]
    use r.val
    simp only [and_true]
    let ⟨r, hr⟩ := r
    by_cases hV : Module.finrank R V = 0
    · simp [hV]
    · rw [← ne_eq, ← Nat.one_le_iff_ne_zero] at hV
      rw [mem_rootsOfUnity', max_eq_left hV] at hr
      simpa [← Subtype.val_inj, ← Units.val_inj]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m✝ : Matrix.SpecialLinearGroup ι K
x✝ : ℙ K (ι → K)
⊢ id (m✝ • x✝) = (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι K))) m✝ • id x✝

Tactic:
simp

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m✝ : Matrix.SpecialLinearGroup ι K
x✝ : ℙ K (ι → K)
⊢ m✝ • x✝ = ↑m✝ • x✝
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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : ∀ (x : V), (H.choose • LinearMap.id) x = (↑↑r • LinearMap.id) x
x : V
⊢ ⋯.choose • x = ↑↑r • x

Tactic:
simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq] at this

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
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : ∀ (x : V), H.choose • x = ↑↑r • x
x : V
⊢ ⋯.choose • x = ↑↑r • x
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
x : V
⊢ centerEquivRootsOfUnity g • x = (centerEquivRootsOfUnity g • LinearMap.id) x

Tactic:
simp

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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ ↑(centerEquivRootsOfUnity g) = ↑1

Tactic:
OneMemClass.coe_one

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
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ ↑(centerEquivRootsOfUnity g) = 1