awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
hv : ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s
have rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hv : v = p₁ -ᵥ p₂), v +ᵥ p ∈ s
Tactic: rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ v +ᵥ p ∈ s
have rw : (p₁ -ᵥ p₂) +ᵥ p ∈ s
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ (p₁ -ᵥ p₂) +ᵥ p ∈ s
have h : p₁ -ᵥ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)
Tactic: convert! s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)
have h : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
hv : v ∈ s.direction
p : P
⊢ v +ᵥ p ∈ s ↔ p ∈ s
have refine : ∀ (h : v +ᵥ p ∈ s), p ∈ s
Tactic: refine ⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p ∈ s
have h₁ : p = -v +ᵥ v +ᵥ p
Tactic: convert! vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
⊢ (↑s.direction : Set V) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
have rw : (↑s : Set P) -ᵥ (↑s : Set P) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
Tactic: rw [coe_direction_eq_vsub_set ⟨p, hp⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
⊢ (↑s : Set P) -ᵥ (↑s : Set P) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
have refine_1 : (↑s : Set P) -ᵥ (↑s : Set P) ≤ (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
refine_1 : (↑s : Set P) -ᵥ (↑s : Set P) ≤ (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
⊢ (↑s : Set P) -ᵥ (↑s : Set P) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
have refine_2 : (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P) ≤ (↑s : Set P) -ᵥ (↑s : Set P)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
⊢ (↑s.direction : Set V) = (fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)
have h : ∀ (v : V), v ∈ (↑s.direction : Set V) ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
⊢ v ∈ (↑s.direction : Set V) ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v
have h : (∃ x ∈ (↑s : Set P), x -ᵥ p = -v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
Tactic: rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe,
    coe_direction_eq_vsub_set_right hp, Set.mem_image, Set.mem_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
| ∃ x ∈ (↑s : Set P), x -ᵥ p = -v
have p₁ : fun (x : P) ↦ x ∈ (↑s : Set P) ∧ x -ᵥ p = -v
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
| fun (x : P) ↦ x ∈ (↑s : Set P) ∧ x -ᵥ p = -v
have p₁ : ∀ (x : P), x ∈ (↑s : Set P) ∧ x -ᵥ p = -v
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
x : P
| x ∈ (↑s : Set P) ∧ x -ᵥ p = -v
have p₁ : x ∈ (↑s : Set P) ∧ p -ᵥ x = v
Tactic: rw [← neg_vsub_eq_vsub_rev, neg_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
| ∃ x ∈ (↑s : Set P), x -ᵥ p = -v
have p₁ : ∀ (x : P), x ∈ (↑s : Set P) ∧ p -ᵥ x = v
Tactic: congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
⊢ (∃ x ∈ (↑s : Set P), x -ᵥ p = -v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
have conv_lhs : (∃ x ∈ (↑s : Set P), x -ᵥ p = -v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
Tactic: conv_lhs =>
    congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
conv_lhs : (∃ x ∈ (↑s : Set P), x -ᵥ p = -v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
⊢ (∃ x ∈ (↑s : Set P), x -ᵥ p = -v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
have h : (∃ x ∈ (↑s : Set P), p -ᵥ x = v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
Tactic: conv_lhs =>
    congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
have rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
Tactic: rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
have rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
Tactic: rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
⊢ s₁ = s₂
have h : ∀ (p : P), p ∈ s₁ ↔ p ∈ s₂
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
⊢ p ∈ s₁ ↔ p ∈ s₂
have hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
Tactic: have hq1 := Set.mem_of_mem_inter_left hn.some_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
⊢ p ∈ s₁ ↔ p ∈ s₂
have hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
Tactic: have hq2 := Set.mem_of_mem_inter_right hn.some_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
⊢ p ∈ s₁ ↔ p ∈ s₂
have h : p ∈ s₁ → p ∈ s₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
h : p ∈ s₁ → p ∈ s₂
⊢ p ∈ s₁ ↔ p ∈ s₂
have h₁ : p ∈ s₂ → p ∈ s₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
⊢ p ∈ s₂
have h : (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂
Tactic: rw [← vsub_vadd p hn.some]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
⊢ (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂
have h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction
Tactic: refine vadd_mem_of_mem_direction ?_ hq2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction
have h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction
Tactic: rw [← hd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
⊢ p ∈ s₁
have h : (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁
Tactic: rw [← vsub_vadd p hn.some]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
⊢ (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁
have h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction
Tactic: refine vadd_mem_of_mem_direction ?_ hq1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction
have h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction
Tactic: rw [hd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
p : P
direction : Submodule k V
⊢ AffineSubspace.direction (mk' p direction) = direction
have h : ∀ (v : V), v ∈ AffineSubspace.direction (mk' p direction) ↔ v ∈ direction
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
p : P
direction : Submodule k V
v : V
⊢ v ∈ AffineSubspace.direction (mk' p direction) ↔ v ∈ direction
have h : (∃ (p₁ : P),
    Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
      ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) ↔
  v ∈ direction
Tactic: rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
p : P
direction : Submodule k V
v : V
⊢ (∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) ↔
    v ∈ direction
have h : (∃ (p₁ : P),
    Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
      ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) →
  v ∈ direction
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
p : P
direction : Submodule k V
v : V
h :
  (∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) →
    v ∈ direction
⊢ (∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) ↔
    v ∈ direction
have h₁ : v ∈ direction →
  ∃ (p₁ : P),
    Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
      ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
⊢ p ∈ (↑s₁ : Set P)
have rw : v +ᵥ p₁ ∈ (↑s₁ : Set P)
Tactic: rw [hp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
⊢ v +ᵥ p₁ ∈ (↑s₁ : Set P)
have hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
Tactic: have hp₁s₁ : p₁ ∈ (s₁ : Set P) := Set.mem_of_mem_of_subset hp₁ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
⊢ v +ᵥ p₁ ∈ (↑s₁ : Set P)
have refine : v ∈ s₁.direction
Tactic: refine vadd_mem_of_mem_direction ?_ hp₁s₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
⊢ v ∈ s₁.direction
have hs : vectorSpan k s ≤ s₁.direction
Tactic: have hs : vectorSpan k s ≤ s₁.direction := vectorSpan_mono k h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
hs : vectorSpan k s ≤ s₁.direction
⊢ v ∈ s₁.direction
have hs₁ : ∀ ⦃x : V⦄, Membership.mem (γ := Submodule k V) (vectorSpan k s) x → x ∈ s₁.direction
Tactic: rw [SetLike.le_def] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Submodule k V
⊢ s.toAffineSubspace.direction = s
have h : ∀ (x : V), x ∈ s.toAffineSubspace.direction ↔ x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
⊢ Eq (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)
have a : LE.le (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
a : LE.le (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)
⊢ Eq (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)
have a₁ : LE.le (α := Submodule k V) (vectorSpan k s) (AffineSubspace.direction (affineSpan k s))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
⊢ LE.le (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)
have a : (↑(affineSpan k s) : Set P) -ᵥ (↑(affineSpan k s) : Set P) ⊆ (↑(vectorSpan k s) : Set V)
Tactic: refine Submodule.span_le.2 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₃)
have a : Membership.mem (γ := Submodule k V) (vectorSpan k s) (v₁ + (p₂ -ᵥ p₄) - v₂)
Tactic: rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
⊢ (↑(vectorSpan k s) : Set V) + s = (↑(affineSpan k s) : Set V)
have h : ∀ (x : V), x ∈ (↑(vectorSpan k s) : Set V) + s ↔ x ∈ (↑(affineSpan k s) : Set V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
x : V
⊢ x ∈ (↑(vectorSpan k s) : Set V) + s ↔ x ∈ (↑(affineSpan k s) : Set V)
have h : (∃ (x_1 : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) x_1 ∧ ∃ y ∈ s, x_1 + y = x) ↔
  ∃ p₁ ∈ s, ∃ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v ∧ x = v + p₁
Tactic: simp [mem_add, spanPoints]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (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
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : Membership.mem (γ := Set P) (⋂ s' ∈ s, (↑s' : Set P)) p₁
hp₂ : Membership.mem (γ := Set P) (⋂ s' ∈ s, (↑s' : Set P)) p₂
hp₃ : Membership.mem (γ := Set P) (⋂ s' ∈ s, (↑s' : Set P)) p₃
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s₂ : Set P)
have rw : ∀ (hp₁ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₁ ∈ (↑i : Set P))
  (hp₂ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₂ ∈ (↑i : Set P))
  (hp₃ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₃ ∈ (↑i : Set P)) (s₂ : AffineSubspace k P) (hs₂ : s₂ ∈ s),
  c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s₂ : Set P)
Tactic: rw [Set.mem_iInter₂] at *
Cleared hypotheses: hp₁, hp₂, hp₃, s₂, hs₂