awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
c : k
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
refine : c • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ (↑s : Set P)
⊢ (c • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p₂ ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
refine vsub_mem_vsub ?_ hp₂

Premises used: Set.vsub_mem_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
c : k
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ (↑s : Set P)

Tactic:
s.smul_vsub_vadd_mem c hp₁ hp₂ hp₂

Premises used: Set.Mem, AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
c : k
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ (↑s : Set P)

Tactic:
exact s.smul_vsub_vadd_mem c hp₁ hp₂ hp₂

Premises used: AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
⊢ directionOfNonempty h = s.direction

Tactic:
le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)

Premises used: Iff.mpr, le_antisymm, Set.Subset.rfl, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
refine : directionOfNonempty h ≤ s.direction
⊢ directionOfNonempty h = s.direction

Tactic:
refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)

Premises used: Iff.mpr, le_antisymm, Set.Subset.rfl, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
⊢ (↑{ carrier := (↑s : Set P) -ᵥ (↑s : Set P), add_mem' := ⋯ : AddSubsemigroup V } : Set V) ⊆
    (↑(vectorSpan k (↑s : Set P)) : Set V)

Tactic:
vsub_set_subset_vectorSpan k _

Premises used: setOf, Set.image2, vsub_set_subset_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
⊢ (↑{ carrier := (↑s : Set P) -ᵥ (↑s : Set P), add_mem' := ⋯ : AddSubsemigroup V } : Set V) ⊆
    (↑(vectorSpan k (↑s : Set P)) : Set V)

Tactic:
exact vsub_set_subset_vectorSpan k _

Premises used: vsub_set_subset_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
⊢ (↑s.direction : Set V) = (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
directionOfNonempty_eq_direction h ▸ rfl

Premises used: Eq.rec, AffineSubspace.directionOfNonempty_eq_direction, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
v : V
rw : (∃ x ∈ (↑s : Set P), ∃ y ∈ (↑s : Set P), x -ᵥ y = v) ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
⊢ v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h, Set.mem_vsub]

Premises used: Set.mem_vsub, AffineSubspace.coe_direction_eq_vsub_set, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (↑s : Set P).Nonempty
v : V
⊢ (∃ x ∈ (↑s : Set P), ∃ y ∈ (↑s : Set P), x -ᵥ y = v) ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Tactic:
simp only [SetLike.mem_coe, eq_comm]

Premises used: eq_comm, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
hp : p ∈ s
rw : ∀ (hv : ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂) {p : P} (hp : p ∈ s), v +ᵥ p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv

Premises used: AffineSubspace.mem_direction_iff_eq_vsub, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ s) (p₂ : P) (hp₂ : p₂ ∈ s) (hv : v = p₁ -ᵥ p₂), v +ᵥ p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂
rw : (p₁ -ᵥ p₂) +ᵥ p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
rw [hv]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂) +ᵥ p ∈ s.carrier

Tactic:
s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp

Premises used: AffineSubspace.smul_vsub_vadd_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂
h : p₁ -ᵥ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)
⊢ (p₁ -ᵥ p₂) +ᵥ p ∈ s

Tactic:
convert! s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp

Premises used: AffineSubspace.smul_vsub_vadd_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂
h h₁ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ -ᵥ p₂ ∈ s.direction

Tactic:
vsub_mem_vectorSpan k hp₁ hp₂

Premises used: vsub_mem_vectorSpan, Set.Mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : v +ᵥ p ∈ s
⊢ v ∈ s.direction

Tactic:
simpa using vsub_mem_direction h hp

Premises used: AffineSubspace.vsub_mem_direction
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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

Tactic:
⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩

Premises used: AffineSubspace.vadd_mem_of_mem_direction, Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
refine : ∀ (h : v +ᵥ p ∈ s), p ∈ s
⊢ v +ᵥ p ∈ s ↔ p ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ -v +ᵥ v +ᵥ p ∈ s

Tactic:
vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h

Premises used: Submodule.neg_mem, AffineSubspace.vadd_mem_of_mem_direction
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h₁ : p = -v +ᵥ v +ᵥ p
⊢ p ∈ s

Tactic:
convert! vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h

Premises used: Submodule.neg_mem, AffineSubspace.vadd_mem_of_mem_direction
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 = -v +ᵥ v +ᵥ p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
rw : (↑s : Set P) -ᵥ (↑s : Set P) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)
⊢ (↑s.direction : Set V) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)

Tactic:
rw [coe_direction_eq_vsub_set ⟨p, hp⟩]

Premises used: AffineSubspace.coe_direction_eq_vsub_set, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
refine_2 : (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P) ≤ (↑s : Set P) -ᵥ (↑s : Set P)
⊢ (↑s : Set P) -ᵥ (↑s : Set P) = (fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂)

Tactic:
⟨(p₁ -ᵥ p₂) +ᵥ p,
      vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩

Premises used: Set.Mem, AffineSubspace.vsub_mem_direction, setOf, VSub.vsub, HVAdd.hVAdd, AffineSubspace.vadd_mem_of_mem_direction, And.intro, Exists.intro, Set.image, vadd_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂)

Tactic:
exact ⟨(p₁ -ᵥ p₂) +ᵥ p,
      vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
hp₂ : p₂ ∈ (↑s : Set P)
⊢ (fun (x : P) ↦ x -ᵥ p) p₂ ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
⟨p₂, hp₂, p, hp, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
hp₂ : p₂ ∈ (↑s : Set P)
⊢ (fun (x : P) ↦ x -ᵥ p) p₂ ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
exact ⟨p₂, hp₂, p, hp, rfl⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : ∀ (v : V), v ∈ (↑s.direction : Set V) ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v
⊢ (↑s.direction : Set V) = (fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (∃ x ∈ (↑s : Set P), x -ᵥ p = -v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
⊢ v ∈ (↑s.direction : Set V) ↔ Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) 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]

Premises used: Set.mem_image, Submodule.neg_mem_iff, SetLike.mem_coe, AffineSubspace.coe_direction_eq_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
p₁ : fun (x : P) ↦ x ∈ (↑s : Set P) ∧ x -ᵥ p = -v
| ∃ x ∈ (↑s : Set P), x -ᵥ p = -v

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
p₁ : ∀ (x : P), x ∈ (↑s : Set P) ∧ x -ᵥ p = -v
| fun (x : P) ↦ x ∈ (↑s : Set P) ∧ x -ᵥ p = -v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
p₁ : x ∈ (↑s : Set P) ∧ p -ᵥ x = v
| x ∈ (↑s : Set P) ∧ x -ᵥ p = -v

Tactic:
rw [← neg_vsub_eq_vsub_rev, neg_inj]

Premises used: neg_inj, neg_vsub_eq_vsub_rev
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
p₁ : ∀ (x : P), x ∈ (↑s : Set P) ∧ p -ᵥ x = v
| ∃ x ∈ (↑s : Set P), x -ᵥ p = -v

Tactic:
congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]

Premises used: neg_inj, neg_vsub_eq_vsub_rev
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : (∃ x ∈ (↑s : Set P), p -ᵥ x = v) ↔ ∃ x ∈ (↑s : Set P), p -ᵥ x = v
⊢ (∃ 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]

Premises used: neg_inj, neg_vsub_eq_vsub_rev
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp]

Premises used: SetLike.mem_coe, AffineSubspace.coe_direction_eq_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

Premises used: Membership.mem, Exists, _private.0.AffineSubspace.mem_direction_iff_eq_vsub_right.match_1, _private.0.AffineSubspace.mem_direction_iff_eq_vsub_right.match_2, VSub.vsub, And, SetLike.coe, And.intro, Iff.intro, Exists.intro, Set.image, Eq.symm, Eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]

Premises used: SetLike.mem_coe, AffineSubspace.coe_direction_eq_vsub_set_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

Premises used: _private.0.AffineSubspace.mem_direction_iff_eq_vsub_left.match_2, Membership.mem, Exists, VSub.vsub, And, SetLike.coe, And.intro, Iff.intro, Exists.intro, Set.image, _private.0.AffineSubspace.mem_direction_iff_eq_vsub_left.match_1, Eq.symm, Eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' (↑s : Set P)) v ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ Function.Injective (α := AffineSubspace k P) SetLike.coe

Tactic:
SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 q : AffineSubspace k P
h : ∀ (x : P), x ∈ p ↔ x ∈ q
⊢ p = q

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ s₁ = s₂ ↔ (↑s₁ : Set P) = (↑s₂ : Set P)

Tactic:
SetLike.ext'_iff

Premises used: SetLike.ext'_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : ∀ (p : P), p ∈ s₁ ↔ p ∈ s₂
⊢ s₁ = s₂

Tactic:
ext p
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)

Tactic:
have hq1 := Set.mem_of_mem_inter_left hn.some_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
⊢ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)

Tactic:
have hq2 := Set.mem_of_mem_inter_right hn.some_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂
h₁ : p ∈ s₂ → p ∈ s₁
⊢ p ∈ s₁ ↔ p ∈ s₂

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₁
h : (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂
⊢ p ∈ s₂

Tactic:
rw [← vsub_vadd p hn.some]

Premises used: vsub_vadd, Set.Nonempty.some
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂

Tactic:
vadd_mem_of_mem_direction ?_ hq2

Premises used: AffineSubspace.vadd_mem_of_mem_direction