awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
⊢ (cross (mk F v hv) (mk F w hw)).orthogonal (mk F v hv)
have h₁ : orthogonal
  (mk F
    ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
        (a : Fin 3 → F) → Fin 3 → F)
      w)
    sorry)
  (mk F v hv)
Tactic: rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
h₁ :
  orthogonal
    (mk F
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w)
      ⋯)
    (mk F v hv)
⊢ (cross (mk F v hv) (mk F w hw)).orthogonal (mk F v hv)
have h₂ : (((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
        (a : Fin 3 → F) → Fin 3 → F)
      w ⬝ᵥ
    v =
  0
Tactic: rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
h₁ :
  orthogonal
    (mk F
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w)
      ⋯)
    (mk F v hv)
h₂ :
  (((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w ⬝ᵥ
      v =
    0
⊢ (cross (mk F v hv) (mk F w hw)).orthogonal (mk F v hv)
have h₃ : v ⬝ᵥ
    (((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
        (a : Fin 3 → F) → Fin 3 → F)
      w =
  0
Tactic: rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)
h₁ :
  orthogonal
    (mk F
      ((((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w)
      ⋯)
    (mk F v hv)
h₂ :
  (((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w ⬝ᵥ
      v =
    0
h₃ :
  v ⬝ᵥ
      (((crossProduct : (a : Fin 3 → F) → (Fin 3 → F) →ₗ[F] Fin 3 → F) v : (Fin 3 → F) →ₗ[F] Fin 3 → F) :
          (a : Fin 3 → F) → Fin 3 → F)
        w =
    0
⊢ (cross (mk F v hv) (mk F w hw)).orthogonal (mk F v hv)
have h₄ : Eq.{u_1 + 1} (α := F) 0 0
Tactic: rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
w : ℙ F (Fin 3 → F)
v : Fin 3 → F
hv : v ≠ 0
h : mk F v hv ≠ w
⊢ (cross (mk F v hv) w).orthogonal (mk F v hv)
have h₁ : ∀ (w : Fin 3 → F) (hw : w ≠ 0) (h : Ne (α := ℙ F (Fin 3 → F)) (mk F v hv) (mk F w hw)),
  (cross (mk F v hv) (mk F w hw)).orthogonal (mk F v hv)
Tactic: induction w with | h w hw =>
  rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v
have h₁ : ∀ (v : Fin 3 → F) (hv : v ≠ 0) (h : mk F v hv ≠ w), (cross (mk F v hv) w).orthogonal (mk F v hv)
Tactic: induction v with | h v hv =>
  induction w with | h w hw =>
  rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w
have rw : (w.cross v).orthogonal w
Tactic: rw [cross_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.orthogonal (v.cross w)
have rw : (v.cross w).orthogonal v
Tactic: rw [orthogonal_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Constructions (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ w.orthogonal (v.cross w)
have rw : (v.cross w).orthogonal w
Tactic: rw [orthogonal_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
have refine_1 : Independent f → LinearIndependent K (Projectivization.rep ∘ f)
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
refine_1 : Independent f → LinearIndependent K (Projectivization.rep ∘ f)
⊢ Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
have refine_2 : ∀ (h : LinearIndependent K (Projectivization.rep ∘ f)), Independent f
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
⊢ LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
have refine_1 : ∀ (a : (i : ι) → Kˣ) (ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) sorry)),
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) sorry)
Tactic: choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
⊢ LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
have h : (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) sorry) = a • ff
Tactic: convert! hh.units_smul a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
⊢ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯) = a • ff
have h : ∀ (i : ι), Function.comp (β := ℙ K V) Projectivization.rep (fun (i : ι) ↦ mk K (ff i) sorry) i = (a • ff) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ Independent f
have h₁ : ∀ (x : ι), f x = mk K ((Projectivization.rep ∘ f) x) sorry
Tactic: convert! Independent.mk _ _ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
h₁ : ∀ (x : ι), f x = mk K ((Projectivization.rep ∘ f) x) ⋯
⊢ Independent f
have refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
Tactic: convert! Independent.mk _ _ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
have refine_1 : Independent f → iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
refine_1 : Independent f → iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
⊢ Independent f ↔ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
have refine_2 : ∀ (h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule), Independent f
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦
    Projectivization.submodule ((fun (i : ι) ↦ (mk K (f i) ⋯ : ℙ K V)) i)
have refine_1 : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ K ∙ f i
Tactic: simp only [submodule_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
⊢ Independent f
have refine_2 : LinearIndependent K (Projectivization.rep ∘ f)
Tactic: rw [independent_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
⊢ LinearIndependent K (Projectivization.rep ∘ f)
have refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i
Tactic: refine h.linearIndependent (Projectivization.submodule ∘ f) (fun i => ?_) fun i => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i
⊢ LinearIndependent K (Projectivization.rep ∘ f)
have refine_2₁ : ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
Tactic: refine h.linearIndependent (Projectivization.submodule ∘ f) (fun i => ?_) fun i => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
have refine_1 : Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
refine_1 : Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
have refine_2 : ∀ (h : ¬LinearIndependent K (Projectivization.rep ∘ f)), Dependent f
Tactic: refine ⟨?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : ¬LinearIndependent K ff
⊢ ¬LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
      (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
have refine_1 : ∀
  (hh1 :
    LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
      (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) sorry)),
  LinearIndependent K ff
Tactic: contrapose hh1
Cleared hypotheses: hh1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
⊢ LinearIndependent K ff
have refine_1 : ∀ (a : (i : ι) → Kˣ) (ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) sorry)), LinearIndependent K ff
Tactic: choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
⊢ LinearIndependent K ff
have h : ff = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) sorry)
Tactic: convert! hh1.units_smul a⁻¹
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
⊢ ff = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
have h : ∀ (i : ι),
  ff i = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) sorry) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f
have h₁ : ∀ (x : ι), f x = mk K ((Projectivization.rep ∘ f) x) sorry
Tactic: convert! Dependent.mk _ _ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
h₁ : ∀ (x : ι), f x = mk K ((Projectivization.rep ∘ f) x) ⋯
⊢ Dependent f
have refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
Tactic: convert! Dependent.mk _ _ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬Independent f
have rw : ¬LinearIndependent K (Projectivization.rep ∘ f) ↔ ¬Independent f
Tactic: rw [dependent_iff, independent_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
rw : ¬LinearIndependent K (Projectivization.rep ∘ f) ↔ ¬Independent f
⊢ Dependent f ↔ ¬Independent f
have rw₁ : ¬LinearIndependent K (Projectivization.rep ∘ f) ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
Tactic: rw [dependent_iff, independent_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ ¬Dependent f
have rw : Independent f ↔ ¬¬Independent f
Tactic: rw [dependent_iff_not_independent, Classical.not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
rw : Independent f ↔ ¬¬Independent f
⊢ Independent f ↔ ¬Dependent f
have rw₁ : Independent f ↔ Independent f
Tactic: rw [dependent_iff_not_independent, Classical.not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
⊢ Dependent ![u, v] ↔ u = v
have rw : ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
      ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
  u = v
Tactic: rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : 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
have dsimp : ¬(v.rep ≠ 0 ∧ ∀ (a : K), a • v.rep ≠ u.rep) ↔ u = v
Tactic: dsimp only [Function.comp_def, Matrix.cons_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
⊢ ¬(v.rep ≠ 0 ∧ ∀ (a : K), a • v.rep ≠ u.rep) ↔ u = v
have simp : v.rep ≠ 0 ∨ u = v
Tactic: simp only [not_and, not_forall, not_not, ← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v),
    mk_rep, Classical.imp_iff_right_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
⊢ Independent ![u, v] ↔ u ≠ v
have rw : ¬Dependent ![u, v] ↔ u ≠ v
Tactic: rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
rw : ¬Dependent ![u, v] ↔ u ≠ v
⊢ Independent ![u, v] ↔ u ≠ v
have rw₁ : ¬u = v ↔ u ≠ v
Tactic: rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ Independent ![mk K u hu, mk K v hv] ↔ LinearIndependent K ![u, v]
have rw : (¬∃ (a : K), a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0
Tactic: rw [independent_pair_iff_ne, ne_eq, mk_eq_mk_iff' K u v hu hv, linearIndependent_fin2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Independence (goal)
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ (a : K), a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0
have simp : (¬∃ (a : K), a • v = u) ↔ v ≠ 0 ∧ ∀ (a : K), a • v ≠ u
Tactic: simp only [Matrix.cons_val_zero, Matrix.cons_val_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A B : Subspace K V
⊢ A.carrier = B.carrier → A = B
have mk : ∀ (carrier : Set (ℙ K V))
  (mem_add' :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier →
        Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier),
  { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier = B.carrier →
    { carrier := carrier, mem_add' := mem_add' : Subspace K V } = B
Tactic: cases A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : Subspace K V
carrier : Set (ℙ K V)
mem_add' :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier →
      Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier
⊢ { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier = B.carrier →
    { carrier := carrier, mem_add' := mem_add' : Subspace K V } = B
have mk : ∀ (carrier_1 : Set (ℙ K V))
  (mem_add'_1 :
    ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
      Projectivization.mk K v hv ∈ carrier_1 →
        Projectivization.mk K w hw ∈ carrier_1 → Projectivization.mk K (v + w) hvw ∈ carrier_1),
  { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier =
      { carrier := carrier_1, mem_add' := mem_add'_1 }.carrier →
    { carrier := carrier, mem_add' := mem_add' : Subspace K V } = { carrier := carrier_1, mem_add' := mem_add'_1 }
Tactic: cases B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ x ∈ B
have of : ∀ x ∈ A, x ∈ B
Tactic: induction hx with
      | of => apply h; assumption
      | mem_add => apply B.mem_add; assumption'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ x ∈ B
have 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
Tactic: induction hx with
      | of => apply h; assumption
      | mem_add => apply B.mem_add; assumption'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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)
have 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
Tactic: refine fun s => ⟨fun a ha x hx => hx _ ⟨a, ha, rfl⟩, fun a ha x hx E => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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 Set.univ) ⊤
have rw : ∀ ⦃x : ℙ K V⦄, Membership.mem (γ := Subspace K V) ⊤ x → Membership.mem (γ := Subspace K V) (span Set.univ) x
Tactic: rw [eq_top_iff, SetLike.le_def]