mathlib-initiative/mathlib-tactics huggingface dataset:
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✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
this✝ : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := IsScalarTower.right
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := Algebra.to_smulCommClass
⊢ (LinearMap.mul R (⨂[R] (x : ι), R)).compr₂ toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun

Tactic:
]

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
this✝ : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := IsScalarTower.right
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := Algebra.to_smulCommClass
⊢ (LinearMap.mul R (⨂[R] (x : ι), R)).compr₂ toFun = (LinearMap.mul R R ∘ₗ toFun).compl₂ toFun
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝² : CommRing R
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
⊢ (Submodule.span R (Set.range fun j ↦ ⨂ₜ[R] (i : ι), g (j i))).mkQ = 0

Tactic:
]

Goal state after:
R : Type u_1
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝² : CommRing R
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
⊢ (Submodule.span R (Set.range fun j ↦ ⨂ₜ[R] (i : ι), g (j i))).mkQ = 0
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
b : { v // v ≠ 0 }
⊢ ⊥ = ⊥

Tactic:
]

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
inst✝ : Subsingleton V
⊢ IsEmpty (ℙ k V)

Tactic:
by
  have : IsEmpty { v : V // v ≠ 0 } := ⟨fun v ↦ v.2 (Subsingleton.elim v.1 0)⟩
  simpa using (nonZeroEquivProjectivizationProdUnits k V).symm.isEmpty

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 : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Infinite V

Tactic:
]

Goal state after:
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
⊢ Infinite V
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inl
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
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
← Fintype.card_eq_nat_card,

Goal state after:
case inl.inl
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
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Fintype.card V - 1 = Fintype.card (ℙ k V) * (Fintype.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inl
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
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Fintype.card (ℙ k V) * Fintype.card kˣ = Fintype.card (ℙ k V) * Fintype.card kˣ

Tactic:
]

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
inst✝ : Finite V
⊢ Nat.card V = Nat.card V - 1 + 1

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
⊢ Nat.card V = Nat.card V - 1 + 1
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
inst✝ : Finite k
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = Nat.card (ℙ k V)

pp: case H
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ 0 < Nat.card k - 1

Tactic:
]

Goal state after:
case H
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ 0 < Nat.card k - 1
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
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Finite V
⊢ Finite V

Tactic:
]

Goal state after:
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
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Finite V
⊢ Finite V
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
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite (ℙ k V)
⊢ Module.finrank k V = 0

Tactic:
]

Goal state after:
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
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
    Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite (ℙ k V)
⊢ Module.finrank k V = 0
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:
]

Goal state after:
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
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
g g' : G
x : ℙ K V
⊢ map ((DistribMulAction.toModuleEnd K V) g) ?hg (map ((DistribMulAction.toModuleEnd K V) g') ?hf x) =
    map ((DistribMulAction.toModuleEnd K V) g) ⋯ (map ((DistribMulAction.toModuleEnd K V) g') ⋯ x)

pp: case hf
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
g g' : G
x : ℙ K V
⊢ Function.Injective ⇑((DistribMulAction.toModuleEnd K V) g')

pp: case hg
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
g g' : G
x : ℙ K V
⊢ Function.Injective ⇑((DistribMulAction.toModuleEnd K V) g)

Tactic:
]

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
⊢ ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

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
⊢ ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
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 : 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
⊢ ∃ g, g • D = E ∧ g • D' = E'

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
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
⊢ ∃ g, g • D = E ∧ g • D' = E'
Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum

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✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv ((tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) =
    (lof R ((i : ι) → κ i) (fun i ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p) ((tprod R) fun i ↦ x i)

Tactic:
]

Goal state after:
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✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv ((tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) =
    (lof R ((i : ι) → κ i) (fun i ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p) ((tprod R) fun i ↦ x i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum

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✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv.symm ((lof R ((i : ι) → κ i) (fun p ↦ ⨂[R] (i : ι), M i (p i)) p) ((tprod R) x)) =
    (tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)

Tactic:
]

Goal state after:
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✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv.symm ((lof R ((i : ι) → κ i) (fun p ↦ ⨂[R] (i : ι), M i (p i)) p) ((tprod R) x)) =
    (tprod R) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h.left
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
⊢ ∃ a, a • E.rep = g • D.rep

Tactic:
]

Goal state after:
case h.left
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
⊢ ∃ a, a • E.rep = g • D.rep
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
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ
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
⊢ Independent 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)
⊢ Independent f

Tactic:
· rintro ⟨ff, hff, hh⟩
    choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
    convert! hh.units_smul a
    ext i
    exact (ha i).symm

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)
⊢ Independent f
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)
W : Subspace K V
⊢ W ⊔ span S = W ⊔ span S

Tactic:
]

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

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i ↦ (f i).submodule
⊢ LinearIndependent K (Projectivization.rep ∘ 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 : iSupIndep fun i ↦ (f i).submodule
⊢ LinearIndependent K (Projectivization.rep ∘ f)
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)
W : Subspace K V
⊢ span S ⊔ W = span S ⊔ W

Tactic:
]

Goal state after:
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)

Tactic:
rintro ⟨ff, hff, hh1⟩

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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : ¬LinearIndependent K ff
⊢ ¬LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)
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
⊢ ¬LinearIndependent K (Projectivization.rep ∘ f) ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
]

Goal state after:
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
⊢ Independent f ↔ Independent f

Tactic:
]

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

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v

Tactic:
]

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬u = v ↔ u ≠ v

Tactic:
]

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}
⊢ 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}
⊢ y ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ a, a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0

Tactic:
]

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ a, a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0
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 ∈ {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 ∈ {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}
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])) :=
  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
⊢ ∃ a, a • E'.rep = g • D'.rep

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])) :=
  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
⊢ ∃ a, a • E'.rep = g • D'.rep
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
S : Set (Projectivization K V)
⊢ (∃ M, Module.Finite K ↥(Subspace.submodule M) ∧ Module.finrank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M) ↔
    ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M

Tactic:
]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
⊢ (∃ M, Module.Finite K ↥(Subspace.submodule M) ∧ Module.finrank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M) ↔
    ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M