mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos.refine_2
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
⊢ dilatransvection ⋯ • mk K D.rep ⋯ = mk K D.rep ⋯

pp: case pos.refine_3
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
⊢ dilatransvection ⋯ • mk K D'.rep ⋯ = mk K D'.rep ⋯

Tactic:
·

Goal state after:
case pos.refine_2
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
⊢ dilatransvection ⋯ • mk K D.rep ⋯ = mk K D.rep ⋯
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
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : x = 0
⊢ (fun x ↦ ↑u x) x = (fun x ↦ ↑v x) x

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
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : ¬x = 0
⊢ (fun x ↦ ↑u x) x = (fun x ↦ ↑v x) x

Tactic:
·

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
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : x = 0
⊢ (fun x ↦ ↑u x) x = (fun x ↦ ↑v x) x
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: case refine_1
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), ∃ b ∈ L, g • b = A • w - w
w : ι → F
⊢ (g⁻¹ * A * g) • w - w ∈ L

pp: case refine_2
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⁻¹ • (A • w - w) ∈ L

Tactic:
·

Goal state after:
case refine_1
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), ∃ b ∈ L, g • b = A • w - w
w : ι → F
⊢ (g⁻¹ * A * g) • w - w ∈ L
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: case refine_2
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⁻¹ • (A • w - w) ∈ L

Tactic:
·

Goal state after:
case refine_2
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⁻¹ • (A • w - w) ∈ L
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: case refine_1
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
a : R
hw : a • v ∈ R ∙ v
⊢ a • v ∈ Submodule.comap A (R ∙ v)

pp: case refine_2
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
x✝ : ↥(R ∙ v)
a : R
hw : a • v ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨a • v, hw⟩ = (c • id) ⟨a • v, hw⟩

Tactic:
·

Goal state after:
case refine_1
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
a : R
hw : a • v ∈ R ∙ v
⊢ a • v ∈ Submodule.comap A (R ∙ v)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ u ∈ Set.range ⇑toGeneralLinearGroup → LinearEquiv.det u.toLinearEquiv = 1

pp: case mpr
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ LinearEquiv.det u.toLinearEquiv = 1 → u ∈ Set.range ⇑toGeneralLinearGroup

Tactic:
·

Goal state after:
case mp
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ u ∈ Set.range ⇑toGeneralLinearGroup → LinearEquiv.det u.toLinearEquiv = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ LinearEquiv.det u.toLinearEquiv = 1 → u ∈ Set.range ⇑toGeneralLinearGroup

Tactic:
·

Goal state after:
case mpr
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ LinearEquiv.det u.toLinearEquiv = 1 → u ∈ Set.range ⇑toGeneralLinearGroup
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: case refine_2
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
x✝ : ↥(R ∙ v)
a : R
hw : a • v ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨a • v, hw⟩ = (c • id) ⟨a • v, hw⟩

Tactic:
·

Goal state after:
case refine_2
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
x✝ : ↥(R ∙ v)
a : R
hw : a • v ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨a • v, hw⟩ = (c • id) ⟨a • v, hw⟩
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos.refine_2
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
⊢ dilatransvection ⋯ • mk K D.rep ⋯ = mk K D.rep ⋯

Tactic:
rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]
      use a
      rw [← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]
      suffices (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1 by
        rw [this, Module.Basis.extend_apply_self, Units.smul_def]
        module
      nth_rewrite 1 [show D.rep = (⟨D.rep, hD_mem⟩ : s) by rfl]
      rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
      simp

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

Goal state before:
pp: case pos.refine_3
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
⊢ dilatransvection ⋯ • mk K D'.rep ⋯ = mk K D'.rep ⋯

Tactic:
·

Goal state after:
case pos.refine_3
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
⊢ dilatransvection ⋯ • mk K D'.rep ⋯ = mk K D'.rep ⋯
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 : SpecialLinearGroup n R
⊢ LinearEquiv.det (toLin' A) = 1

Tactic:
simp [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
        Matrix.SpecialLinearGroup.toLin'_to_linearMap]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
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 : SpecialLinearGroup R V
hR : Subsingleton R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

pp: case inr
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 : SpecialLinearGroup R V
hR : Nontrivial R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
·

Goal state after:
case inl
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 : SpecialLinearGroup R V
hR : Subsingleton R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
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)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1

pp: case inr
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)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
·

Goal state after:
case inl
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)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inr
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)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
·

Goal state after:
case inr
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)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case refine_1
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
⊢ ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m

pp: case refine_2
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
l : ℙ K (ι → K)
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
⊢ m • l = l

Tactic:
·

Goal state after:
case refine_1
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
⊢ ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos
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]

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:
·

Goal state after:
case pos
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]
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:
·

Goal state after:
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]
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)
r : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hV : Module.finrank R V = 0
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1

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)
r : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hV : ¬Module.finrank R V = 0
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1

Tactic:
·

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)
r : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hV : Module.finrank R V = 0
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
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)
r : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hV : ¬Module.finrank R V = 0
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1

Tactic:
·

Goal state after:
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)
r : Rˣ
hr : r ∈ rootsOfUnity (max (Module.finrank R V) 1) R
hV : ¬Module.finrank R V = 0
⊢ ↑↑⟨r, hr⟩ ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case refine_2
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
l : ℙ K (ι → K)
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
⊢ m • l = l

Tactic:
·

Goal state after:
case refine_2
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
l : ℙ K (ι → K)
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
⊢ m • l = l
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))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ IsUnit 1

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))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ max (Module.finrank R V) 1 ≠ 0

Tactic:
·

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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ IsUnit 1
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g

Tactic:
·

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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ ↑↑1 • LinearMap.id = ↑↑↑g
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g

Tactic:
·

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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑1 • LinearMap.id = ↑↑↑g
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g

Tactic:
·

Goal state after:
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
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g
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) +
      ∑ 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)

pp: 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

Tactic:
·

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)
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:
·

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