awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ (↑B : Set (ℙ K V))
x : ℙ K V
hx : x ∈ span A
of : ∀ x ∈ A, x ∈ B
mem_add :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    spanCarrier A (Projectivization.mk K v hv) →
      spanCarrier A (Projectivization.mk K w hw) →
        Projectivization.mk K v hv ∈ B → Projectivization.mk K w hw ∈ B → Projectivization.mk K (v + w) hvw ∈ B
⊢ x ∈ B

Tactic:
induction hx with
      | of => apply h; assumption
      | mem_add => apply B.mem_add; assumption'

Premises used: Projectivization.Subspace.mem_add
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ span (↑W : Set (ℙ K V)) = W

Tactic:
GaloisInsertion.l_u_eq gi W

Premises used: Projectivization.Subspace.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set (Subspace K V)
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h1 : Projectivization.mk K v hv ∈ sInf (SetLike.coe '' A)
h2 : Projectivization.mk K w hw ∈ sInf (SetLike.coe '' A)
s : Subspace K V
hs : s ∈ A
⊢ Projectivization.mk K (v + w) hvw ∈ (↑s : Set (ℙ K V))

Tactic:
s.mem_add v w hv hw _ (h1 s ⟨s, hs, rfl⟩) (h2 s ⟨s, hs, rfl⟩)

Premises used: SetLike.coe, And.intro, Exists.intro, Projectivization.Subspace.mem_add, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set (Subspace K V)
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h1 : Projectivization.mk K v hv ∈ sInf (SetLike.coe '' A)
h2 : Projectivization.mk K w hw ∈ sInf (SetLike.coe '' A)
s : Subspace K V
hs : s ∈ A
⊢ Projectivization.mk K (v + w) hvw ∈ (↑s : Set (ℙ K V))

Tactic:
exact s.mem_add v w hv hw _ (h1 s ⟨s, hs, rfl⟩) (h2 s ⟨s, hs, rfl⟩)

Premises used: SetLike.coe, And.intro, Exists.intro, Projectivization.Subspace.mem_add, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ ∀ (s : Set (Subspace K V)), IsGLB s (sInf s)

Tactic:
fun s => ⟨fun a ha x hx => hx _ ⟨a, ha, rfl⟩, fun a ha x hx E => ?_⟩

Premises used: IsGreatest, SetLike.coe, IsGLB, And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
refine :
  ∀ (s : Set (Subspace K V)) (a : Subspace K V) (ha : a ∈ lowerBounds s) (x : ℙ K V) (hx : x ∈ a),
    ∀ E ∈ SetLike.coe '' s, x ∈ E
⊢ ∀ (s : Set (Subspace K V)), IsGLB s (sInf s)

Tactic:
refine fun s => ⟨fun a ha x hx => hx _ ⟨a, ha, rfl⟩, fun a ha x hx E => ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Subspace K V
hE : E ∈ s
⊢ x ∈ (↑E : Set (ℙ K V))

Tactic:
ha hE hx
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Subspace K V
hE : E ∈ s
⊢ x ∈ (↑E : Set (ℙ K V))

Tactic:
exact ha hE hx
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq.{u_2 + 1} (α := Subspace K V) (span ∅) ⊥

Tactic:
gi.gc.l_bot

Premises used: GaloisConnection.l_bot, Projectivization.Subspace.gi, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
rw : ∀ ⦃x : ℙ K V⦄, Membership.mem (γ := Subspace K V) ⊤ x → Membership.mem (γ := Subspace K V) (span Set.univ) x
⊢ Eq.{u_2 + 1} (α := Subspace K V) (span Set.univ) ⊤

Tactic:
rw [eq_top_iff, SetLike.le_def]

Premises used: eq_top_iff, SetLike.le_def
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : ℙ K V
_hx : Membership.mem (γ := Subspace K V) ⊤ x
⊢ Membership.mem (γ := Subspace K V) (span Set.univ) x

Tactic:
subset_span _ (Set.mem_univ x)

Premises used: Projectivization.Subspace.subset_span, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : ℙ K V
_hx : Membership.mem (γ := Subspace K V) ⊤ x
⊢ Membership.mem (γ := Subspace K V) (span Set.univ) x

Tactic:
exact subset_span _ (Set.mem_univ x)

Premises used: Projectivization.Subspace.subset_span, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ≤ W ↔ S ⊆ (↑W : Set (ℙ K V))

Tactic:
gi.gc S W

Premises used: Projectivization.Subspace.gi, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Monotone.{u_2, u_2} (α := Set (ℙ K V)) span

Tactic:
gi.gc.monotone_l

Premises used: Projectivization.Subspace.gi, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set (ℙ K V)
hst : s ⊆ t
⊢ span s ≤ span t

Tactic:
monotone_span hst

Premises used: Projectivization.Subspace.monotone_span
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S T U : Set (ℙ K V)
hST : S ⊆ (↑(span T) : Set (ℙ K V))
hTU : T ⊆ (↑(span U) : Set (ℙ K V))
⊢ S ⊆ (↑(span U) : Set (ℙ K V))

Tactic:
gi.gc.le_u_l_trans hST hTU

Premises used: GaloisConnection.le_u_l_trans, Projectivization.Subspace.gi, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S T : Set (ℙ K V)
⊢ span (S ∪ T) = span S ⊔ span T

Tactic:
(@gi K V _ _ _).gc.l_sup

Premises used: Projectivization.Subspace.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Sort u_3
s : ι → Set (ℙ K V)
⊢ Eq.{u_2 + 1} (α := Subspace K V) (span (⋃ (i : ι), s i)) (⨆ (i : ι), span (s i))

Tactic:
(@gi K V _ _ _).gc.l_iSup

Premises used: GaloisConnection.l_iSup, Projectivization.Subspace.gi, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
rw : W ⊔ span S = span (↑W : Set (ℙ K V)) ⊔ span S
rw₁ rw₂ : W ⊔ span S = W ⊔ span S
⊢ W ⊔ span S = span ((↑W : Set (ℙ K V)) ∪ S)

Tactic:
rw [span_union, span_coe]

Premises used: Projectivization.Subspace.span_coe, Projectivization.Subspace.span_union
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
rw : span S ⊔ W = span S ⊔ span (↑W : Set (ℙ K V))
rw₁ rw₂ : span S ⊔ W = span S ⊔ W
⊢ span S ⊔ W = span (S ∪ (↑W : Set (ℙ K V)))

Tactic:
rw [span_union, span_coe]

Premises used: Projectivization.Subspace.span_coe, Projectivization.Subspace.span_union
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
u : ℙ K V
simp_rw : u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → u ∈ W

Tactic:
simp_rw [← span_le_subspace_iff]

Premises used: Projectivization.Subspace.span_le_subspace_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W

Tactic:
⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩

Premises used: le_refl, Iff.intro, Projectivization.Subspace.span
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W

Tactic:
exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
carrier :
  ∀ (x : ℙ K V),
    x ∈ (span S).carrier ↔
      Membership.mem (γ := Set (ℙ K V)) (Subspace.carrier (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))})) x
⊢ span S = sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
carrier :
  (∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W) ↔
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
⊢ x ∈ (span S).carrier ↔
    Membership.mem (γ := Set (ℙ K V)) (Subspace.carrier (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))})) x

Tactic:
simp_rw [mem_carrier_iff, mem_span x]

Premises used: Projectivization.Subspace.mem_span, Projectivization.Subspace.mem_carrier_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W) ↔
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x

Tactic:
⟨fun hx => ?_, fun hx W hW => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
carrier :
  ∀ (hx : ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W),
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
carrier₁ :
  ∀ (hx : Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x) (W : Subspace K V)
    (hW : S ⊆ (↑W : Set (ℙ K V))), x ∈ W
⊢ (∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W) ↔
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x

Tactic:
refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W
T : Subspace K V
hT : Membership.mem (γ := Set (Subspace K V)) {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))} T
⊢ x ∈ (↑T : Set (ℙ K V))

Tactic:
hx T hT
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W
T : Subspace K V
hT : Membership.mem (γ := Set (Subspace K V)) {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))} T
⊢ x ∈ (↑T : Set (ℙ K V))

Tactic:
exact hx T hT
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
W : Subspace K V
hW : S ⊆ (↑W : Set (ℙ K V))
⊢ x ∈ W

Tactic:
(@sInf_le _ _ { W : Subspace K V | S ⊆ ↑W } W hW) hx

Premises used: sInf_le
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
W : Subspace K V
hW : S ⊆ (↑W : Set (ℙ K V))
⊢ x ∈ W

Tactic:
exact (@sInf_le _ _ { W : Subspace K V | S ⊆ ↑W } W hW) hx

Premises used: sInf_le
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
hS : S ⊆ (↑W : Set (ℙ K V))
hW : W ≤ span S
⊢ span S = W

Tactic:
le_antisymm (span_le_subspace_iff.mpr hS) hW

Premises used: Iff.mpr, le_antisymm, Projectivization.Subspace.span_le_subspace_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S T : Set (ℙ K V)
⊢ span S = span T ↔ S ⊆ (↑(span T) : Set (ℙ K V)) ∧ T ⊆ (↑(span S) : Set (ℙ K V))

Tactic:
⟨fun h => ⟨h ▸ subset_span S, h.symm ▸ subset_span T⟩, fun h =>
    le_antisymm (span_le_subspace_iff.2 h.1) (span_le_subspace_iff.2 h.2)⟩

Premises used: Iff.mpr, Eq.rec, Projectivization.Subspace.subset_span, le_antisymm, And.right, And.left, Projectivization.Subspace.span_le_subspace_iff, And.intro, Iff.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
inl :
  ∀ (hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0),
    Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (0 + y)
inr :
  ∀ (hx₂ : x ≠ 0), Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)

Tactic:
rcases eq_or_ne x 0 with rfl | hx₂

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
y : V
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0
inl inl₁ inl₂ inl₃ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (0 + y)

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
hx₂ : x ≠ 0
inr :
  ∀ (hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0),
    Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + 0)
inr₁ :
  ∀ (hy₂ : y ≠ 0), Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)

Tactic:
rcases eq_or_ne y 0 with rfl | hy₂

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hx₂ : x ≠ 0
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0
inr inr₁ inr₂ inr₃ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + 0)

Tactic:
rwa [add_zero]

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
hx₂ : x ≠ 0
hy₂ : y ≠ 0
hxy : x + y ≠ 0
⊢ Projectivization.mk K (x + y) hxy ∈ s.carrier

Tactic:
s.mem_add _ _ hx₂ hy₂ hxy (hx₁ hx₂) (hy₁ hy₂)

Premises used: Set.Mem, Projectivization.Subspace.mem_add
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
hx₂ : x ≠ 0
hy₂ : y ≠ 0
hxy : x + y ≠ 0
⊢ Projectivization.mk K (x + y) hxy ∈ s.carrier

Tactic:
exact s.mem_add _ _ hx₂ hy₂ hxy (hx₁ hx₂) (hy₁ hy₂)

Premises used: Projectivization.Subspace.mem_add
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
⊢ Projectivization.mk K x ⋯ ∈ s.carrier

Tactic:
h₁ (right_ne_zero_of_smul h₂)

Premises used: right_ne_zero_of_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
h : Eq (α := ℙ K V) (Projectivization.mk K (c • x) h₂) (Projectivization.mk K x ⋯)
⊢ Projectivization.mk K (c • x) h₂ ∈ s.carrier

Tactic:
convert! h₁ (right_ne_zero_of_smul h₂) using 1

Premises used: right_ne_zero_of_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
h : ∃ (a : K), a • x = c • x
⊢ Eq (α := ℙ K V) (Projectivization.mk K (c • x) h₂) (Projectivization.mk K x ⋯)

Tactic:
rw [Projectivization.mk_eq_mk_iff']

Premises used: Projectivization.mk_eq_mk_iff'
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
⊢ ∃ (a : K), a • x = c • x

Tactic:
⟨c, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
⊢ ∃ (a : K), a • x = c • x

Tactic:
exact ⟨c, rfl⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
y : V
property : y ≠ 0
c : K
h : c • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) y property) : V) ≠ 0
⊢ Eq (α := Prop)
    ((fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s)
      (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) (c • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) y property) : V)) h))
    ((fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) y property))

Tactic:
Iff.eq <| s.smul_mem_iff <| left_ne_zero_of_smul h

Premises used: left_ne_zero_of_smul, Submodule.smul_mem_iff, Iff.eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
y : V
property : y ≠ 0
c : K
h : c • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) y property) : V) ≠ 0
⊢ Eq (α := Prop)
    ((fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s)
      (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) (c • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) y property) : V)) h))
    ((fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) y property))

Tactic:
exact Iff.eq <| s.smul_mem_iff <| left_ne_zero_of_smul h

Premises used: left_ne_zero_of_smul, Submodule.smul_mem_iff, Iff.eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
carrier :
  ∀ (x : ℙ K V) (x : V) (hx : x ≠ 0),
    Membership.mem (γ := Set (ℙ K V))
        (Subspace.carrier
          ((fun (s : Submodule K V) ↦
              { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯),
                mem_add' := ⋯ : Subspace K V })
            ((fun (s : Subspace K V) ↦
                ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯,
                    zero_mem' := ⋯, smul_mem' := ⋯ } :
                  Submodule K V))
              s)))
        (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop)
          (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) x hx)) ↔
      Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop)
          (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) x hx) ∈
        s.carrier
⊢ (fun (s : Submodule K V) ↦
        { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯), mem_add' := ⋯ :
          Subspace K V })
      ((fun (s : Subspace K V) ↦
          ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
              smul_mem' := ⋯ } :
            Submodule K V))
        s) =
    s

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x_1 : ℙ K V
x : V
hx : x ≠ 0
⊢ Membership.mem (γ := Set (ℙ K V))
      (carrier
        ((fun (s : Submodule K V) ↦
            { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯), mem_add' := ⋯ :
              Subspace K V })
          ((fun (s : Subspace K V) ↦
              ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯,
                  zero_mem' := ⋯, smul_mem' := ⋯ } :
                Submodule K V))
            s)))
      (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop)
        (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) x hx)) ↔
    Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop)
        (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) x hx) ∈
      s.carrier

Tactic:
⟨fun h => h hx, fun h _ => h⟩

Premises used: Iff.intro