awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst_8 : Nonempty ι
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
inhabited_h : Inhabited ι
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
have rw : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) default 0) : P2)
  ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) default 0) : P2)
Tactic: rw [← Pi.single_zero default]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst_8 : Nonempty ι
h :
  ∀ (i : ι),
    Eq (α := φv i →ᵃ[k] P2) (f.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
      (g.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
⊢ f = g
have refine : ∀ (i : ι) (x : φv i),
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
Tactic: refine pi_ext_nonempty fun i x => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
⊢ Eq (α := P1 →ᵃ[k] P1) (homothety c 1) (id k P1)
have h : ∀ (p : P1), Eq (α := P1) ((homothety c 1 : (a : P1) → P1) p : P1) ((id k P1 : (a : P1) → P1) p : P1)
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
⊢ Eq (α := P1 →ᵃ[k] P1) (homothety c 0) (const k P1 c)
have h : ∀ (p : P1), Eq (α := P1) ((homothety c 0 : (a : P1) → P1) p : P1) ((const k P1 c : (a : P1) → P1) p : P1)
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
⊢ (homothety c r₁ : (a : P1) → P1) p = q ↔ (homothety c r₂ : (a : P1) → P1) q = p
have h' : r₂ * r₁ = 1
Tactic: obtain h' : r₂ * r₁ = 1 := mul_eq_one_comm.mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
⊢ (homothety c r₁ : (a : P1) → P1) p = q ↔ (homothety c r₂ : (a : P1) → P1) q = p
have refine_1 : ∀ (h1 : (homothety c r₁ : (a : P1) → P1) p = q), (homothety c r₂ : (a : P1) → P1) q = p
Tactic: refine ⟨fun h1 ↦ ?_, fun h1 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
refine_1 : ∀ (h1 : (homothety c r₁ : (a : P1) → P1) p = q), (homothety c r₂ : (a : P1) → P1) q = p
⊢ (homothety c r₁ : (a : P1) → P1) p = q ↔ (homothety c r₂ : (a : P1) → P1) q = p
have refine_2 : ∀ (h1 : (homothety c r₂ : (a : P1) → P1) q = p), (homothety c r₁ : (a : P1) → P1) p = q
Tactic: refine ⟨fun h1 ↦ ?_, fun h1 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₁ : (a : P1) → P1) p = q
⊢ (homothety c r₂ : (a : P1) → P1) q = p
have refine_1 : (homothety c (r₂ * r₁) : (a : P1) → P1) p = p
Tactic: rw [← h1, ← homothety_mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₂ : (a : P1) → P1) q = p
⊢ (homothety c r₁ : (a : P1) → P1) p = q
have refine_2 : (homothety c (r₁ * r₂) : (a : P1) → P1) q = q
Tactic: rw [← h1, ← homothety_mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ (f : (a : E) → F) (a • x + b • y) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
have simp : (f : (a : E) → F) (b • (y -ᵥ x) + x) =
  HAdd.hAdd (β := F) (b • VSub.vsub (P := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F))
    ((f : (a : E) → F) x : F)
Tactic: simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s
have rw : (∃ p₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s
Tactic: rw [mem_direction_iff_eq_vsub_right hp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s
have rw : (∃ p₂_1 ∈ s, p -ᵥ p₂ = p -ᵥ p₂_1) ↔ p₂ ∈ s
Tactic: rw [mem_direction_iff_eq_vsub_left hp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : Nonempty.{u_3 + 1} ↥s
a b : ↥s.direction
c : ↥s
⊢ (a + b) +ᵥ c = a +ᵥ b +ᵥ c
have a₁ : (↑((a + b) +ᵥ c) : P) = (↑(a +ᵥ b +ᵥ c) : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : Nonempty.{u_3 + 1} ↥s
a : ↥s
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := ↥s.direction) 0 a = a
have a₁ : (↑(HVAdd.hVAdd.{u_2, u_3, u_3} (α := ↥s.direction) 0 a) : P) = (↑a : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : Nonempty.{u_3 + 1} ↥s
a b : ↥s
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑a : P) -ᵥ (↑b : P)) ⋯ +ᵥ b = a
have a₁ : (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑a : P) -ᵥ (↑b : P)) sorry +ᵥ b) : P) = (↑a : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
inst_4 : Nonempty.{u_3 + 1} ↥s
a : ↥s.direction
b : ↥s
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑(a +ᵥ b) : P) -ᵥ (↑b : P)) ⋯ = a
have a₁ : (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑(a +ᵥ b) : P) -ᵥ (↑b : P)) sorry) : V) = (↑a : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ Membership.mem (α := P) Q ((lineMap p₀ p₁ : (a : k) → P) c : P)
have rw : c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q
Tactic: rw [AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
c : P
hc : c ∈ s
r : k
p : P
hp : p ∈ s
⊢ Membership.mem (α := P) s ((homothety c r : (a : P) → P) p : P)
have rw : Membership.mem (α := P) s ((lineMap c p : (a : k) → P) r : P)
Tactic: rw [AffineMap.homothety_eq_lineMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
p : P
⊢ (↑(affineSpan k {p}) : Set P) = {p}
have h : ∀ (x : P), x ∈ (↑(affineSpan k {p}) : Set P) ↔ Membership.mem (γ := Set P) {p} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
p x : P
⊢ x ∈ (↑(affineSpan k {p}) : Set P) ↔ Membership.mem (γ := Set P) {p} x
have h : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p}) (x -ᵥ p) ↔ Membership.mem (γ := Set P) {p} x
Tactic: rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _,
    direction_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ Subsingleton P
have obtain : ∀ (p : P) (hp : p ∈ s), Subsingleton P
Tactic: obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
p : P
hp : p ∈ s
⊢ Subsingleton P
have this : s = {p}
Tactic: have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
have h₃ : Set.Subsingleton.{u_3} (α := P) univ
Tactic: rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
    AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂
Cleared hypotheses: h₂, hp, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ s = univ
have obtain : ∀ (p : P) (hp : p ∈ s), s = univ
Tactic: obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
p : P
hp : p ∈ s
⊢ s = univ
have this : s = {p}
Tactic: have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ
have rw : Subsingleton P
Tactic: rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ < s₂
hn : (↑s₁ : Set P).Nonempty
⊢ s₁.direction < s₂.direction
have obtain : ∀ (p : P) (hp : p ∈ (↑s₁ : Set P)), s₁.direction < s₂.direction
Tactic: obtain ⟨p, hp⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ < s₂
p : P
hp : p ∈ (↑s₁ : Set P)
⊢ s₁.direction < s₂.direction
have rw : ∀ (h : s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁) (p : P) (hp : p ∈ (↑s₁ : Set P)), s₁.direction < s₂.direction
Tactic: rw [lt_iff_le_and_exists] at h
Cleared hypotheses: h, p, hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
p : P
hp : p ∈ (↑s₁ : Set P)
⊢ s₁.direction < s₂.direction
have rcases : ∀ (hle : s₁ ≤ s₂) (p₂ : P) (hp₂ : p₂ ∈ s₂) (hp₂s₁ : p₂ ∉ s₁), s₁.direction < s₂.direction
Tactic: rcases h with ⟨hle, p₂, hp₂, hp₂s₁⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
hp : p ∈ (↑s₁ : Set P)
hle : s₁ ≤ s₂
p₂ : P
hp₂ : p₂ ∈ s₂
hp₂s₁ : p₂ ∉ s₁
⊢ s₁.direction < s₂.direction
have rw : s₁.direction ≤ s₂.direction ∧ ∃ x ∈ s₂.direction, x ∉ s₁.direction
Tactic: rw [SetLike.lt_iff_le_and_exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
hp : p ∈ (↑s₁ : Set P)
hle : s₁ ≤ s₂
p₂ : P
hp₂ : p₂ ∈ s₂
hp₂s₁ : p₂ ∉ s₁
⊢ s₁.direction ≤ s₂.direction ∧ ∃ x ∈ s₂.direction, x ∉ s₁.direction
have right : p₂ -ᵥ p ∉ s₁.direction
Tactic: use direction_le hle, p₂ -ᵥ p, vsub_mem_direction hp₂ (hle hp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
hp : p ∈ (↑s₁ : Set P)
hle : s₁ ≤ s₂
p₂ : P
hp₂ : p₂ ∈ s₂
hp₂s₁ : p₂ ∉ s₁
hm : p₂ -ᵥ p ∈ s₁.direction
⊢ False
have hm₁ : p₂ ∈ s₁
Tactic: rw [vsub_right_mem_direction_iff_mem hp p₂] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))
have refine_1 : LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))
Tactic: refine le_antisymm ?_ (Submodule.span_mono ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
refine_1 : LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))
have refine_2 : (fun (x : P) ↦ p -ᵥ x) '' s ⊆ s -ᵥ s
Tactic: refine le_antisymm ?_ (Submodule.span_mono ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))
have refine_1 : s -ᵥ s ⊆ (↑(Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s)) : Set V)
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring 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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = v
⊢ v ∈ (↑(Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s)) : Set V)
have hv₁ : p -ᵥ p₂ - (p -ᵥ p₁) = v
Tactic: simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring 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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ v ∈ (↑(Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s)) : Set V)
have refine_1 : ∀ (p_1 : Submodule k V), (fun (x : P) ↦ p -ᵥ x) '' s ⊆ (↑p_1 : Set V) → p -ᵥ p₂ - (p -ᵥ p₁) ∈ p_1
Tactic: rw [← hv, SetLike.mem_coe, Submodule.mem_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))
have refine_1 : LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))
Tactic: refine le_antisymm ?_ (Submodule.span_mono ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
refine_1 : LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))
have refine_2 : (fun (x : P) ↦ x -ᵥ p) '' s ⊆ s -ᵥ s
Tactic: refine le_antisymm ?_ (Submodule.span_mono ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))
have refine_1 : s -ᵥ s ⊆ (↑(Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s)) : Set V)
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring 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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = v
⊢ v ∈ (↑(Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s)) : Set V)
have hv₁ : p₁ -ᵥ p - (p₂ -ᵥ p) = v
Tactic: simp_rw [← vsub_sub_vsub_cancel_right p₁ p₂ p] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring 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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ v ∈ (↑(Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s)) : Set V)
have refine_1 : ∀ (p_1 : Submodule k V), (fun (x : P) ↦ x -ᵥ p) '' s ⊆ (↑p_1 : Set V) → p₁ -ᵥ p - (p₂ -ᵥ p) ∈ p_1
Tactic: rw [← hv, SetLike.mem_coe, Submodule.mem_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
have rw : Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))
Tactic: rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (vectorSpan k s) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))
have conv_lhs : Eq (α := Submodule k V) (Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p}))))
  (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))
Tactic: conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s
have rw : Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))
Tactic: rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (vectorSpan k s) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))
have conv_lhs : Eq (α := Submodule k V) (Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p}))))
  (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))
Tactic: conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
have rw : Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i})))
Tactic: rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
      Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]