awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp₁ : p₁ ∈ s
inr : (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) → ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
⊢ (∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀
have inr₁ : (∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₀) → ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
⊢ ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
have h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
Tactic: use v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ (r : k), p₂ = r • v +ᵥ p₁
have h : ∀ (r : k) (hp₂ : r • v +ᵥ p ∈ s), ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ p₁
Tactic: rcases hv p₂ hp₂ with ⟨r, rfl⟩
Cleared hypotheses: p₂, hp₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ p₁
have h : ∀ (r₁ : k) (hp₁ : r₁ • v +ᵥ p ∈ s), ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ r₁ • v +ᵥ p
Tactic: rcases hv p₁ hp₁ with ⟨r₁, rfl⟩
Cleared hypotheses: p₁, hp₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
v : V
hv : ∀ p_1 ∈ s, ∃ (r : k), p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ ∃ (r_1 : k), r • v +ᵥ p = r_1 • v +ᵥ r₁ • v +ᵥ p
have h : r • v +ᵥ p = (r - r₁) • v +ᵥ r₁ • v +ᵥ p
Tactic: use r - r₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ Collinear k (P := P) {p₁, p₂}
have rw : ∃ (p₀ : P) (v : V), ∀ (p : P), Membership.mem (γ := Set P) {p₁, p₂} p → ∃ (r : k), p = r • v +ᵥ p₀
Tactic: rw [collinear_iff_exists_forall_eq_smul_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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) (v : V), ∀ (p : P), Membership.mem (γ := Set P) {p₁, p₂} p → ∃ (r : k), p = r • v +ᵥ p₀
have h : ∀ (p : P), Membership.mem (γ := Set P) {p₁, p₂} p → ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: use p₁, p₂ -ᵥ p₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
hp : Membership.mem (γ := Set P) {p₁, p₂} p
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
have hp₁ : p = p₁ ∨ p = p₂
Tactic: rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp : p = p₁ ∨ p = p₂
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
have h : ∀ (hp : p = p₁), ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: rcases hp with hp | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp : p = p₁ ∨ p = p₂
h : ∀ (hp : p = p₁), ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
have h₁ : ∀ (hp : p = p₂), ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: rcases hp with hp | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp : p = p₁
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
have h : p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: use 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp : p = p₂
⊢ ∃ (r : k), p = r • (p₂ -ᵥ p₁) +ᵥ p₁
have h : p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: use 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
⊢ AffineIndependent k p ↔ ¬Collinear k (Set.range p)
have rw : AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1
Tactic: rw [collinear_iff_finrank_le_one,
    affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
rw : AffineIndependent k p ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1
⊢ AffineIndependent k p ↔ ¬Collinear k (Set.range p)
have rw₁ : ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1 ↔ ¬finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1
Tactic: rw [collinear_iff_finrank_le_one,
    affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
⊢ Collinear k (Set.range p) ↔ ¬AffineIndependent k p
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1 ↔ ¬AffineIndependent k p
Tactic: rw [collinear_iff_finrank_le_one,
    finrank_vectorSpan_le_iff_not_affineIndependent k p (Fintype.card_fin 3)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
rw : finrank.{u_1, u_2} k ↥(vectorSpan k (Set.range p)) ≤ 1 ↔ ¬AffineIndependent k p
⊢ Collinear k (Set.range p) ↔ ¬AffineIndependent k p
have rw₁ : ¬AffineIndependent k p ↔ ¬AffineIndependent k p
Tactic: rw [collinear_iff_finrank_le_one,
    finrank_vectorSpan_le_iff_not_affineIndependent k p (Fintype.card_fin 3)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
have rw : ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
Tactic: rw [affineIndependent_iff_not_collinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
have simp_rw : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ Set.range ![]))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
Tactic: simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_empty_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
simp_rw : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ Set.range ![]))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
have simp_rw₁ : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ ∅))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
Tactic: simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_empty_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
simp_rw : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ Set.range ![]))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
simp_rw₁ : ¬Collinear k (P := P) ({p₁} ∪ ({p₂} ∪ ({p₃} ∪ ∅))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
have simp_rw₂ : ¬Collinear k (P := P) (insert p₁ (insert p₂ (insert p₃ ∅))) ↔ ¬Collinear k (P := P) {p₁, p₂, p₃}
Tactic: simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_empty_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
Tactic: have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by decide +revert
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₄ : ¬Collinear k (p '' insert i₁ (↑{i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₄ : ¬Collinear k (p '' insert i₁ (↑{i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₅ : ¬Collinear k (p '' insert i₁ (insert i₂ (↑{i₃} : Set (Fin 3)))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₄ : ¬Collinear k (p '' insert i₁ (↑{i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₅ : ¬Collinear k (p '' insert i₁ (insert i₂ (↑{i₃} : Set (Fin 3)))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₆ : ¬Collinear k (p '' {i₁, i₂, i₃}) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₄ : ¬Collinear k (p '' insert i₁ (↑{i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₅ : ¬Collinear k (p '' insert i₁ (insert i₂ (↑{i₃} : Set (Fin 3)))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₆ : ¬Collinear k (p '' {i₁, i₂, i₃}) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₇ : ¬Collinear k (insert (p i₁) (p '' {i₂, i₃})) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
rw : ¬Collinear k (Set.range p) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₁ : ¬Collinear k (p '' Set.univ) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₂ : ¬Collinear k (p '' (↑Finset.univ : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₃ : ¬Collinear k (p '' (↑{i₁, i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₄ : ¬Collinear k (p '' insert i₁ (↑{i₂, i₃} : Set (Fin 3))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₅ : ¬Collinear k (p '' insert i₁ (insert i₂ (↑{i₃} : Set (Fin 3)))) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₆ : ¬Collinear k (p '' {i₁, i₂, i₃}) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
rw₇ : ¬Collinear k (insert (p i₁) (p '' {i₂, i₃})) ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
have rw₈ : ¬Collinear k (P := P) {p i₁, p i₂, p i₃} ↔ ¬Collinear k (P := P) {p i₁, p i₂, p i₃}
Tactic: rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
have rw : ∀ (h : ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁) {p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
  (hp₁p₂ : p₁ ≠ p₂), Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
Tactic: rw [collinear_iff_of_mem hp₁] at h
Cleared hypotheses: h, p₂, p₃, hp₁, hp₂, hp₃, hp₁p₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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 : ∃ (v : V), ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
have rcases : ∀ (v : V) (h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁), Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
Tactic: rcases h with ⟨v, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
have rcases : ∀ (r₂ : k) (hp₂ : r₂ • v +ᵥ p₁ ∈ s) (hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) p₃
Tactic: rcases h p₂ hp₂ with ⟨r₂, rfl⟩
Cleared hypotheses: p₂, hp₂, hp₁p₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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₃ : P
hp₁ : p₁ ∈ s
hp₃ : p₃ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) p₃
have rcases : ∀ (r₃ : k) (hp₃ : r₃ • v +ᵥ p₁ ∈ s),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) (r₃ • v +ᵥ p₁)
Tactic: rcases h p₃ hp₃ with ⟨r₃, rfl⟩
Cleared hypotheses: p₃, hp₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, r₂ • v +ᵥ p₁}) (r₃ • v +ᵥ p₁)
have rw : ∃ (r : k), r • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
Tactic: rw [vadd_left_mem_affineSpan_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ ∃ (r : k), r • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
have refine : (r₃ / r₂) • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
Tactic: refine ⟨r₃ / r₂, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ (r : k), p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ (r₃ / r₂) • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
have h₂ : r₂ ≠ 0
Tactic: have h₂ : r₂ ≠ 0 := by
    rintro rfl
    simp at hp₁p₂