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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
c : K
x : V
h₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
h₂ : c • x ≠ 0
⊢ ∃ a, a • x = c • x

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
c : K
x : V
h₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
h₂ : c • x ≠ 0
⊢ ∃ a, a • x = c • x
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ ∅ ⊆ ↑M

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ ∅ ⊆ ↑M
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:
]

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.rank K ↥⊥ ≤ 2 ∧ ∅ ⊆ ↑⊥
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
e : V ≃ₗ[K] V
D : ℙ K V
⊢ mk K (e • D.rep) ⋯ = mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) ⋯

Tactic:
]

Goal state after:
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
e : V ≃ₗ[K] V
D : ℙ K V
⊢ mk K (e • D.rep) ⋯ = mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) ⋯
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Module.Finite K ↥(K ∙ v)

Tactic:
]

Goal state after:
case h.refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Module.Finite K ↥(K ∙ v)
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ 2

Tactic:
]

Goal state after:
case h.refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ 2
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
⊢ ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

Tactic:
]

Goal state after:
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
⊢ ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ¬v = 0

Tactic:
]

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ¬v = 0
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 : LinearIndependent K ![v, w]
⊢ IsCollinear {mk K v hv, mk K w hw}

Tactic:
]

Goal state after:
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 : LinearIndependent K ![v, w]
⊢ IsCollinear {mk K v hv, mk K w hw}
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
v✝ : V
h✝ : v✝ ≠ 0
⊢ v✝ ∈ s ↔ v✝ ∈ s

Tactic:
]

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

Goal state before:
pp: case h.h.refine_1
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 : LinearIndependent K ![v, w]
⊢ Module.Finite K ↥(Submodule.span K {v, w})

Tactic:
]

Goal state after:
case h.h.refine_1
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 : LinearIndependent K ![v, w]
⊢ Module.Finite K ↥(Submodule.span K {v, w})
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.h.refine_2
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 : LinearIndependent K ![v, w]
⊢ Module.finrank K ↥(Submodule.span K (Set.range ![v, w])) ≤ 2

Tactic:
]

Goal state after:
case h.h.refine_2
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 : LinearIndependent K ![v, w]
⊢ Module.finrank K ↥(Submodule.span K (Set.range ![v, w])) ≤ 2
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos
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ˣ
⊢ ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'

Tactic:
]

Goal state after:
case pos
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ˣ
⊢ ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
this : Module.Finite K ↥p
⊢ Module.finrank K ↥(Submodule.span K (Set.range ![u, v])) = 2

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
this : Module.Finite K ↥p
⊢ Module.finrank K ↥(Submodule.span K (Set.range ![u, v])) = 2
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos
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
⊢ ∃ h, LinearEquiv.det h = a ∧ h • mk K D.rep ⋯ = mk K D.rep ⋯ ∧ h • mk K D'.rep ⋯ = mk K D'.rep ⋯

Tactic:
]

Goal state after:
case pos
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
⊢ ∃ h, LinearEquiv.det h = a ∧ h • mk K D.rep ⋯ = mk K D.rep ⋯ ∧ h • mk K D'.rep ⋯ = mk K D'.rep ⋯
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 : LinearIndependent K ![v, w]
⊢ p = q

Tactic:
]

Goal state after:
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 : LinearIndependent K ![v, w]
⊢ p = q
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 : LinearIndependent K ![v, w]
⊢ Submodule.span K {v, w} = Submodule.span K {v, w}

Tactic:
]

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

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

Tactic:
]

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 (Projectivization.mk F (Pi.single 1 1) ⋯).submodule ≤ ⨆ p, lineStab p.submodule

Tactic:
]

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.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
⊢ iSup iwasawaT = ⨆ i, Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (lineStab i.submodule)

Tactic:
]

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

Goal state before:
pp: F : Type u_2
inst✝ : Field F
step1 : iSup iwasawaT = Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (⨆ p, lineStab p.submodule)
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) ⊤ = ⊤

Tactic:
]

Goal state after:
F : Type u_2
inst✝ : Field F
step1 : iSup iwasawaT = Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (⨆ p, lineStab p.submodule)
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) ⊤ = ⊤
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
⊢ IsMulCommutative ↥(lineStab (F ∙ p.rep))

Tactic:
]

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
⊢ IsMulCommutative ↥(lineStab (F ∙ p.rep))
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝³ : Field F
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i₁ i₂ : ι
hij : i₁ ≠ i₂
g : Matrix.SpecialLinearGroup ι F := SpecialLinearGroup.transvection hij 1
h : 1 = 0
⊢ 1 = 0

Tactic:
]

Goal state after:
ι : Type u_1
F : Type u_2
inst✝³ : Field F
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i₁ i₂ : ι
hij : i₁ ≠ i₂
g : Matrix.SpecialLinearGroup ι F := SpecialLinearGroup.transvection hij 1
h : 1 = 0
⊢ 1 = 0
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
⊢ ∃ a_1, a_1 • D.rep = (dilatransvection ⋯) 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
⊢ ∃ a_1, a_1 • D.rep = (dilatransvection ⋯) D.rep
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
this : Finite F
x : Fˣ
hF : 4 ≤ 2 + 1
hx : Function.Surjective fun x_1 ↦ x ^ x_1
h : ↑x ^ 2 = 1
⊢ False

Tactic:
]

Goal state after:
F : Type u_2
inst✝ : Field F
this : Finite F
x : Fˣ
hF : 4 ≤ 2 + 1
hx : Function.Surjective fun x_1 ↦ x ^ x_1
h : ↑x ^ 2 = 1
⊢ False
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
⊢ a • D.rep = D.rep + (b.repr D.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • b ⟨D.rep, hD_mem⟩

Tactic:
]

Goal state after:
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
⊢ a • D.rep = D.rep + (b.repr D.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • b ⟨D.rep, hD_mem⟩
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

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

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A B : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), A • w - w ∈ L
hB : ∀ (w : ι → F), B • w - w ∈ L
w : ι → F
⊢ A • (B • w - w) - (B • w - w) + (B • w - w) + (A • w - w) ∈ L
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

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

Tactic:
]

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 : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
⊢ A ∈ lineStab (g • L) ↔ (MulAut.conj g)⁻¹ • A ∈ lineStab L

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
⊢ A ∈ lineStab (g • L) ↔ (MulAut.conj g)⁻¹ • A ∈ lineStab L
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
i : ι
h : ¬w i = 0
⊢ w i ≠ 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ w i ≠ 0
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
this : (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1
⊢ ↑a • D.rep = D.rep + 1 • (↑a - 1) • ↑⟨D.rep, hD_mem⟩

Tactic:
]

Goal state after:
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
this : (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1
⊢ ↑a • D.rep = D.rep + 1 • (↑a - 1) • ↑⟨D.rep, hD_mem⟩
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
⊢ (weightedSumSquares K w).IsometryEquiv (weightedSumSquares K fun i ↦ if w i = 0 then 0 else 1)

Tactic:
refine isometryEquivWeightedSumSquaresWeightedSumSquares (fun i => if h : w i = 0 then 1 else
    Units.mk0 (IsAlgClosed.exists_eq_mul_self (w i)).choose (by
      rw [← mul_self_eq_zero.ne, ← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec]
      simpa using h)) ?_

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
⊢ ∀ (i : ι), (if w i = 0 then 0 else 1) * ↑(if h : w i = 0 then 1 else Units.mk0 ⋯.choose ⋯) ^ 2 = w i
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
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
⊢ ↑↑u x = LinearMap.id x

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
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
⊢ ↑↑u x = LinearMap.id x
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
v : SpecialLinearGroup R V
hv : toGeneralLinearGroup v = u
⊢ LinearEquiv.det (toLinearEquiv v) = 1

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
v : SpecialLinearGroup R V
hv : toGeneralLinearGroup v = u
⊢ LinearEquiv.det (toLinearEquiv v) = 1
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:
]

Goal state after:
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
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
g : SpecialLinearGroup R V
⊢ 1 = 1

Tactic:
]

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
f : SpecialLinearGroup R V
⊢ LinearEquiv.det (e.symm ≪≫ₗ ↑f ≪≫ₗ e) = 1

Tactic:
by simp [f.prop]

Goal state after: