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

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

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)
⊢ Dependent f

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)
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)
⊢ Dependent f

Tactic:
·

Goal state after:
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)
⊢ Dependent f
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: ι : 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)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) x✝) ⋯

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)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0

Tactic:
·

Goal state after:
ι : 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)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) 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)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0

Tactic:
·

Goal state after:
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)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h.right
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 : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) := ⋯
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ g • D' = E'

Tactic:
·

Goal state after:
case h.right
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 : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) := ⋯
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ g • D' = E'
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
⊢ x ∈ sInf {W | S ⊆ ↑W}

pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
⊢ x ∈ sInf {W | S ⊆ ↑W}
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W
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 : Set (ℙ K V)
⊢ span S = sInf {W | S ⊆ ↑W}

Tactic:
by
  ext x
  simp_rw [mem_carrier_iff, mem_span x]
  refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
  · rintro W ⟨T, hT, rfl⟩
    exact hx T hT
  · exact (@sInf_le _ _ { W : Subspace K V | S ⊆ ↑W } W hW) hx

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

Goal state before:
pp: case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
y : V
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ 0 + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

pp: case inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

Tactic:
·

Goal state after:
case inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
y : V
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ 0 + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case inr.inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ x + 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

pp: case inr.inr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x y : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hy₁ : y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₂ : y ≠ 0
⊢ x + y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Subspace K V
x : V
hx₁ : x ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
hx₂ : x ≠ 0
hy₁ : 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
⊢ x + 0 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.Finite K ↥(Subspace.submodule M) ∧ Module.finrank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.Finite K ↥(Subspace.submodule M)
hM2 : Module.finrank K ↥(Subspace.submodule M) ≤ 2
hM3 : S ⊆ ↑M
⊢ Module.rank K ↥(Subspace.submodule M) ≤ 2

pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.Finite K ↥(Subspace.submodule M)

pp: case refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.finrank K ↥(Subspace.submodule M) ≤ 2

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.Finite K ↥(Subspace.submodule M) ∧ Module.finrank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.Finite K ↥(Subspace.submodule M)
hM2 : Module.finrank K ↥(Subspace.submodule M) ≤ 2
hM3 : S ⊆ ↑M
⊢ Module.rank K ↥(Subspace.submodule M) ≤ 2
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.Finite K ↥(Subspace.submodule M)

pp: case refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.finrank K ↥(Subspace.submodule M) ≤ 2

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.Finite K ↥(Subspace.submodule M)
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.finrank K ↥(Subspace.submodule M) ≤ 2

Tactic:
·

Goal state after:
case refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
x✝ : ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
M : Subspace K V
hM1 : Module.rank K ↥(Subspace.submodule M) ≤ 2
hM2 : S ⊆ ↑M
⊢ Module.finrank K ↥(Subspace.submodule M) ≤ 2
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
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 : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) := ⋯
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ 1 • E'.rep = g • D'.rep

Tactic:
simp only [one_smul, LinearEquiv.smul_def, ← qD' hD, ← hg, ← qD' hE]

Goal state after:
case h
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 : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 0 1)) = D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    ↑(hD.linearCombinationEquiv (Finsupp.single 1 1)) = D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg : ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))), ↑(f x) = g ↑x
⊢ ↑(hE.linearCombinationEquiv (Finsupp.single 1 1)) = ↑(f (hD.linearCombinationEquiv (Finsupp.single 1 1)))
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 ↥(Subspace.submodule (Submodule.projectivization (K ∙ v)))

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
⊢ Module.finrank K ↥(Subspace.submodule (Submodule.projectivization (K ∙ v))) ≤ 2

pp: case h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ {mk K v hv} ⊆ ↑(Submodule.projectivization (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 ↥(Subspace.submodule (Submodule.projectivization (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
⊢ Module.finrank K ↥(Subspace.submodule (Submodule.projectivization (K ∙ v))) ≤ 2

pp: case h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ {mk K v hv} ⊆ ↑(Submodule.projectivization (K ∙ v))

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
⊢ Module.finrank K ↥(Subspace.submodule (Submodule.projectivization (K ∙ v))) ≤ 2
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ {mk K v hv} ⊆ ↑(Submodule.projectivization (K ∙ v))

Tactic:
·

Goal state after:
case h.refine_3
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ {mk K v hv} ⊆ ↑(Submodule.projectivization (K ∙ v))
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 ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w})))

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 ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w}))) ≤ 2

pp: case h.h.refine_3
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]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s = mk K v hv → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

pp: case h.h.refine_4
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]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s ∈ {mk K w hw} → s ∈ ↑(Submodule.projectivization (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 ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w})))
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 : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
⊢ ∃ g, g • D = E ∧ g • D' = E'

pp: case neg
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
⊢ ∃ g, g • D = E ∧ g • D' = E'

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 : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
⊢ ∃ g, g • D = E ∧ g • D' = E'
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 ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w}))) ≤ 2

pp: case h.h.refine_3
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]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s = mk K v hv → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

pp: case h.h.refine_4
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]
s : ℙ K V
hs : s ∈ {mk K v hv, mk K w hw}
⊢ s ∈ {mk K w hw} → s ∈ ↑(Submodule.projectivization (Submodule.span K {v, w}))

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 ↥(Subspace.submodule (Submodule.projectivization (Submodule.span K {v, w}))) ≤ 2
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos.refine_1
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
⊢ LinearEquiv.det (dilatransvection ⋯) = a

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_1
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
⊢ LinearEquiv.det (dilatransvection ⋯) = a
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

pp: case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
·

Goal state after:
case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
·

Goal state after:
case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)