awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
h : Subset (α := Set P) {p₃} {p₃, p₄}
⊢ Subset (α := Set P) {p₁, p₂, p₃} {p₁, p₂, p₃, p₄}

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₂
h₃ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₄, p₅}) p₃
⊢ Subset (α := Set P) {p₃} {p₃, p₄}

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
rw : ¬Collinear k (P := P) {p₁, p₂, p}
⊢ AffineIndependent k ![p₁, p₂, p]

Tactic:
rw [affineIndependent_iff_not_collinear_set]

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
by_contra : ∀ (h : Collinear k (P := P) {p₁, p₂, p}), False
⊢ ¬Collinear k (P := P) {p₁, p₂, p}

Tactic:
by_contra h
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₁
h₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₃
⊢ Collinear k (P := P) {p₁, p₃, p₂, p}

Tactic:
apply collinear_insert_insert_of_mem_affineSpan_pair

Premises used: collinear_insert_insert_of_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := Set P) {p₁, p₂, p} p₂

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := Set P) {p₁, p₂, p} p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := Set P) {p₁, p₂, p} p₁

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₁

Tactic:
apply Collinear.mem_affineSpan_of_mem_of_ne h (by simp) (by simp) (by simp) hne

Premises used: Collinear.mem_affineSpan_of_mem_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := Set P) {p₂, p₃, p} p₂

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := Set P) {p₂, p₃, p} p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := Set P) {p₂, p₃, p} p₃

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p}) p₃

Tactic:
apply Collinear.mem_affineSpan_of_mem_of_ne hcol (by simp) (by simp) (by simp) hne

Premises used: Collinear.mem_affineSpan_of_mem_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
⊢ Collinear k (P := P) {p₁, p₃, p₂, p}

Tactic:
have h1 : Collinear k {p₁, p₃, p₂, p} := by
    apply collinear_insert_insert_of_mem_affineSpan_pair
    · apply Collinear.mem_affineSpan_of_mem_of_ne h (by simp) (by simp) (by simp) hne
    · apply Collinear.mem_affineSpan_of_mem_of_ne hcol (by simp) (by simp) (by simp) hne
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
⊢ Subset (α := Set P) {p₁, p₂, p₃} {p₁, p₃, p₂, p}

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
⊢ Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
have h2 : Collinear k {p₁, p₂, p₃} := h1.subset (by grind)
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
⊢ ¬Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
rw [affineIndependent_iff_not_collinear_set] at ha

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
ha₁ : ¬Collinear k (P := P) {p₁, p₂, p₃}
⊢ Collinear k (P := P) {p₂, p₃, p}

Tactic:
rw [affineIndependent_iff_not_collinear_set] at ha

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
ha₁ : ¬Collinear k (P := P) {p₁, p₂, p₃}
hcol₁ : Collinear k (P := P) {p₂, p₃, p}
⊢ p₂ ≠ p

Tactic:
rw [affineIndependent_iff_not_collinear_set] at ha

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
ha₁ : ¬Collinear k (P := P) {p₁, p₂, p₃}
hcol₁ : Collinear k (P := P) {p₂, p₃, p}
hne₁ : p₂ ≠ p
⊢ Collinear k (P := P) {p₁, p₂, p}

Tactic:
rw [affineIndependent_iff_not_collinear_set] at ha

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
ha₁ : ¬Collinear k (P := P) {p₁, p₂, p₃}
hcol₁ : Collinear k (P := P) {p₂, p₃, p}
hne₁ : p₂ ≠ p
h₁ : Collinear k (P := P) {p₁, p₂, p}
⊢ Collinear k (P := P) {p₁, p₃, p₂, p}

Tactic:
rw [affineIndependent_iff_not_collinear_set] at ha

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
ha₁ : ¬Collinear k (P := P) {p₁, p₂, p₃}
hcol₁ : Collinear k (P := P) {p₂, p₃, p}
hne₁ : p₂ ≠ p
h₁ : Collinear k (P := P) {p₁, p₂, p}
h1₁ : Collinear k (P := P) {p₁, p₃, p₂, p}
⊢ Collinear k (P := P) {p₁, p₂, p₃}

Tactic:
rw [affineIndependent_iff_not_collinear_set] at ha

Premises used: affineIndependent_iff_not_collinear_set
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : ¬Collinear k (P := P) {p₁, p₂, p₃}
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
⊢ False

Tactic:
ha h2
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
ha : ¬Collinear k (P := P) {p₁, p₂, p₃}
hcol : Collinear k (P := P) {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k (P := P) {p₁, p₂, p}
h1 : Collinear k (P := P) {p₁, p₃, p₂, p}
h2 : Collinear k (P := P) {p₁, p₂, p₃}
⊢ False

Tactic:
exact ha h2
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
⊢ AffineIndependent k ![p₁, p₂, p] ↔ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
⟨fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h hcol hne2,
    fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h ?_ hne1⟩

Premises used: affineIndependent_of_affineIndependent_collinear_ne, Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
refine : ∀ (h : AffineIndependent k ![p₁, p₂, p₃]), Collinear k (P := P) {p₂, p₃, p}
⊢ AffineIndependent k ![p₁, p₂, p] ↔ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
refine ⟨fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h hcol hne2,
    fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h ?_ hne1⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ Collinear k (P := P) {p₂, p, p₃}

Tactic:
hcol
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
h : AffineIndependent k ![p₁, p₂, p₃]
h₁ : Eq (α := Set P) {p₂, p₃, p} {p₂, p, p₃}
⊢ Collinear k (P := P) {p₂, p₃, p}

Tactic:
convert! hcol using 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k (P := P) {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ Eq (α := Set P) {p₂, p₃, p} {p₂, p, p₃}

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)

Tactic:
IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h ?_))

Premises used: Iff.mpr, IsNoetherian.iff_rank_lt_aleph0, lt_of_le_of_lt, IsNoetherian.iff_fg, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Coplanar k s
refine : 2 < Cardinal.aleph0
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)

Tactic:
refine IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h ?_))

Premises used: Iff.mpr, IsNoetherian.iff_rank_lt_aleph0, lt_of_le_of_lt, IsNoetherian.iff_fg, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ 2 < Cardinal.aleph0

Tactic:
Cardinal.lt_aleph0.2 ⟨2, rfl⟩

Premises used: Iff.mpr, Exists.intro, Cardinal.lt_aleph0, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ 2 < Cardinal.aleph0

Tactic:
exact Cardinal.lt_aleph0.2 ⟨2, rfl⟩

Premises used: Iff.mpr, Exists.intro, Cardinal.lt_aleph0, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (affineSpan k s))

Tactic:
(direction_affineSpan k s).symm ▸ h.finiteDimensional_vectorSpan

Premises used: direction_affineSpan, Eq.rec, Coplanar.finiteDimensional_vectorSpan, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
⊢ Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2

Tactic:
have h : Coplanar k s ↔ Module.rank k (vectorSpan k s) ≤ 2 := Iff.rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 2

Tactic:
rw [← finrank_eq_rank] at h

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Coplanar k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 2
⊢ Coplanar k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 2

Tactic:
mod_cast h

Premises used: congrArg, cast, Nat.cast_le._simp_1, Iff, Coplanar
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
h : Coplanar k s ↔ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} k ↥(vectorSpan k s)) : Cardinal.{u_2}) 2
⊢ Coplanar k s ↔ finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ 2

Tactic:
exact mod_cast h
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : Set P
hs : s₁ ⊆ s₂
h : Coplanar k s₂
⊢ Coplanar k s₁

Tactic:
(Submodule.rank_mono (vectorSpan_mono k hs)).trans h

Premises used: Submodule.rank_mono, vectorSpan_mono, LE.le.trans, Coplanar
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
⊢ Coplanar k s

Tactic:
le_trans h one_le_two

Premises used: one_le_two, Coplanar, le_trans
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
⊢ Coplanar.{u_1, u_2, u_3} k (P := P) ∅

Tactic:
(collinear_empty k P).coplanar

Premises used: Collinear.coplanar, collinear_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : P
⊢ Coplanar k (P := P) {p}

Tactic:
(collinear_singleton k p).coplanar

Premises used: collinear_singleton, Collinear.coplanar
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ : P
⊢ Coplanar k (P := P) {p₁, p₂}

Tactic:
(collinear_pair k p₁ p₂).coplanar

Premises used: collinear_pair, Collinear.coplanar
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
rw : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Coplanar k s
rw₁ : Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
rw₂ rw₃ : Module.rank k ↥(vectorSpan k s) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k (insert p s) ↔ Coplanar k s

Tactic:
rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]

Premises used: vectorSpan_insert_eq_vectorSpan, Coplanar
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
pos :
  ∀ (hf : FiniteDimensional.{u_1, u_2} k ↥s.direction),
    finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
neg :
  ∀ (hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction),
    finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1

Tactic:
by_cases hf : FiniteDimensional k s.direction

Premises used: Membership.mem, Subtype, FiniteDimensional, AffineSubspace.direction
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
h : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P)))
⊢ LE.le (α := Submodule k V) (vectorSpan k (↑s : Set P)) (vectorSpan k (insert p (↑s : Set P)))

Tactic:
vectorSpan_mono k (Set.subset_insert _ _)

Premises used: vectorSpan_mono, Set.subset_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
h : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P)))
⊢ LE.le (α := Submodule k V) (vectorSpan k (↑s : Set P)) (vectorSpan k (insert p (↑s : Set P)))

Tactic:
exact vectorSpan_mono k (Set.subset_insert _ _)

Premises used: vectorSpan_mono, Set.subset_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional.{u_1, u_2} k ↥s.direction
h : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P)))
⊢ s.direction ≤ vectorSpan k (insert p (↑s : Set P))

Tactic:
have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
        conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
        exact vectorSpan_mono k (Set.subset_insert _ _)