awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 (α := (a : k) → P1 →ᵃ[k] P1) (⇑(homothetyHom c) : (a : k) → P1 →ᵃ[k] P1) (homothety c)

Tactic:
rfl

Premises used: AffineMap.homothety, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 (α := (a : k) → P1 →ᵃ[k] P1) (⇑(homothetyAffine c) : (a : k) → P1 →ᵃ[k] P1) (homothety c)

Tactic:
rfl

Premises used: AffineMap.homothety, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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)
⊢ (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)

Tactic:
simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]

Premises used: Convex.combo_eq_smul_sub_add, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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) (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:
f.apply_lineMap _ _ _

Premises used: AffineMap.apply_lineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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) (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:
exact f.apply_lineMap _ _ _

Premises used: AffineMap.apply_lineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
v : V
⊢ Eq (α := Submodule k V) (vectorSpan k (v +ᵥ s)) (vectorSpan k s)

Tactic:
simp [vectorSpan]

Premises used: vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
rw : (∃ p₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s
⊢ p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub_right hp]

Premises used: AffineSubspace.mem_direction_iff_eq_vsub_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
rw : (∃ p₂_1 ∈ s, p -ᵥ p₂ = p -ᵥ p₂_1) ↔ p₂ ∈ s
⊢ p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub_left hp]

Premises used: AffineSubspace.mem_direction_iff_eq_vsub_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂_1 ∈ s, p -ᵥ p₂ = p -ᵥ p₂_1) ↔ p₂ ∈ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁ : (↑((a + b) +ᵥ c) : P) = (↑(a +ᵥ b +ᵥ c) : P)
⊢ (a + b) +ᵥ c = a +ᵥ b +ᵥ c

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) : P) = (↑(a +ᵥ b +ᵥ c) : P)

Tactic:
apply add_vadd

Premises used: AddSemigroupAction.add_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
a₁ : (↑(HVAdd.hVAdd.{u_2, u_3, u_3} (α := ↥s.direction) 0 a) : P) = (↑a : P)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := ↥s.direction) 0 a = a

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) : P) = (↑a : P)

Tactic:
zero_vadd _ _

Premises used: zero_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) : P) = (↑a : P)

Tactic:
exact zero_vadd _ _

Premises used: zero_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
a₁ : (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑a : P) -ᵥ (↑b : P)) ⋯ +ᵥ b) : P) = (↑a : P)
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑a : P) -ᵥ (↑b : P)) ⋯ +ᵥ b = a

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) : P) = (↑a : P)

Tactic:
apply AddTorsor.vsub_vadd'

Premises used: AddTorsor.vsub_vadd'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
a₁ : (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑(a +ᵥ b) : P) -ᵥ (↑b : P)) ⋯) : V) = (↑a : V)
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ s.direction) ((↑(a +ᵥ b) : P) -ᵥ (↑b : P)) ⋯ = a

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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)) ⋯) : V) = (↑a : V)

Tactic:
apply AddTorsor.vadd_vsub'

Premises used: AddTorsor.vadd_vsub'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ (↑(a -ᵥ b) : V) = (↑a : P) -ᵥ (↑b : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ (↑(a +ᵥ b) : P) = (↑a : V) +ᵥ (↑b : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ AffineMap.linear s.subtype = s.direction.subtype

Tactic:
rfl

Premises used: Submodule.subtype, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
p : ↥s
⊢ (s.subtype : (a : ↥s) → P) p = (↑p : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥s) (β := P) (⇑s.subtype : (a : ↥s) → P)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ Eq.{u_3 + 1} (α := (a : ↥s) → P) (⇑s.subtype : (a : ↥s) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
rw : c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q
⊢ Membership.mem (α := P) Q ((lineMap p₀ p₁ : (a : k) → P) c : P)

Tactic:
rw [AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q

Tactic:
Q.smul_vsub_vadd_mem c h₁ h₀ h₀

Premises used: Set.Mem, AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q

Tactic:
exact Q.smul_vsub_vadd_mem c h₁ h₀ h₀

Premises used: AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
rw : Membership.mem (α := P) s ((lineMap c p : (a : k) → P) r : P)
⊢ Membership.mem (α := P) s ((homothety c r : (a : P) → P) p : P)

Tactic:
rw [AffineMap.homothety_eq_lineMap]

Premises used: AffineMap.homothety_eq_lineMap
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 ((lineMap c p : (a : k) → P) r : P)

Tactic:
lineMap_mem r hc hp

Premises used: AffineMap.lineMap_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 ((lineMap c p : (a : k) → P) r : P)

Tactic:
exact lineMap_mem r hc hp

Premises used: AffineMap.lineMap_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : ∀ (x : P), x ∈ (↑(affineSpan k {p}) : Set P) ↔ Membership.mem (γ := Set P) {p} x
⊢ (↑(affineSpan k {p}) : Set P) = {p}

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p}) (x -ᵥ p) ↔ Membership.mem (γ := Set P) {p} x
⊢ x ∈ (↑(affineSpan k {p}) : Set 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]

Premises used: Set.mem_singleton, direction_affineSpan, mem_affineSpan, AffineSubspace.vsub_right_mem_direction_iff_mem, AffineSubspace.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p}) (x -ᵥ p) ↔ Membership.mem (γ := Set P) {p} x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂}) p₁ ↔ p₁ = p₂

Tactic:
simp [← mem_coe]

Premises used: AffineSubspace.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
x : P
⊢ Eq (α := Set ↥(affineSpan k {x}))
    (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k {x}) x_1) ⁻¹' {x}) univ

Tactic:
eq_univ_of_forall fun y => (AffineSubspace.mem_affineSpan_singleton _ _).1 y.2

Premises used: Set.eq_univ_of_forall, Iff.mp, AffineSubspace.mem_affineSpan_singleton, Subtype.property
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) ⊤
obtain : ∀ (p : P) (hp : p ∈ s), Subsingleton P
⊢ Subsingleton P

Tactic:
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂

Premises used: AffineSubspace.nonempty_of_affineSpan_eq_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ {p} ⊆ s

Tactic:
simp [hp]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 = {p}

Tactic:
have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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}
⊢ 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₂

Premises used: eq_comm, AffineSubspace.ext_iff, AffineSubspace.top_coe, Set.subsingleton_iff_singleton, Set.mem_univ, AffineSubspace.coe_affineSpan_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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}
h₃ : Set.Subsingleton.{u_3} (α := P) univ
⊢ p ∈ s

Tactic:
rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
    AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂

Premises used: eq_comm, AffineSubspace.ext_iff, AffineSubspace.top_coe, Set.subsingleton_iff_singleton, Set.mem_univ, AffineSubspace.coe_affineSpan_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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}
h₃ : Set.Subsingleton.{u_3} (α := P) univ
hp₁ : p ∈ s
⊢ s = {p}

Tactic:
rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
    AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂

Premises used: eq_comm, AffineSubspace.ext_iff, AffineSubspace.top_coe, Set.subsingleton_iff_singleton, Set.mem_univ, AffineSubspace.coe_affineSpan_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
p : P
h₂ : Set.Subsingleton.{u_3} (α := P) univ
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
subsingleton_of_univ_subsingleton h₂

Premises used: Set.subsingleton_of_univ_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
p : P
h₂ : Set.Subsingleton.{u_3} (α := P) univ
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
exact subsingleton_of_univ_subsingleton h₂

Premises used: Set.subsingleton_of_univ_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) ⊤
obtain : ∀ (p : P) (hp : p ∈ s), s = univ
⊢ s = univ

Tactic:
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂

Premises used: AffineSubspace.nonempty_of_affineSpan_eq_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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}
rw : Subsingleton P
⊢ s = univ

Tactic:
rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff]

Premises used: Set.subsingleton_univ_iff, eq_comm, Set.subsingleton_iff_singleton, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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

Tactic:
subsingleton_of_subsingleton_span_eq_top h₁ h₂

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

Tactic:
exact subsingleton_of_subsingleton_span_eq_top h₁ h₂

Premises used: AffineSubspace.subsingleton_of_subsingleton_span_eq_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
obtain : ∀ (p : P) (hp : p ∈ (↑s₁ : Set P)), s₁.direction < s₂.direction
⊢ s₁.direction < s₂.direction

Tactic:
obtain ⟨p, hp⟩ := hn
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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)
rw : ∀ (h : s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁) (p : P) (hp : p ∈ (↑s₁ : Set P)), s₁.direction < s₂.direction
⊢ s₁.direction < s₂.direction

Tactic:
rw [lt_iff_le_and_exists] at h

Premises used: AffineSubspace.lt_iff_le_and_exists
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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)
rcases : ∀ (hle : s₁ ≤ s₂) (p₂ : P) (hp₂ : p₂ ∈ s₂) (hp₂s₁ : p₂ ∉ s₁), s₁.direction < s₂.direction
⊢ s₁.direction < s₂.direction

Tactic:
rcases h with ⟨hle, p₂, hp₂, hp₂s₁⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
rw : s₁.direction ≤ s₂.direction ∧ ∃ x ∈ s₂.direction, x ∉ s₁.direction
⊢ s₁.direction < s₂.direction

Tactic:
rw [SetLike.lt_iff_le_and_exists]

Premises used: SetLike.lt_iff_le_and_exists
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
right : p₂ -ᵥ p ∉ s₁.direction
⊢ s₁.direction ≤ s₂.direction ∧ ∃ x ∈ s₂.direction, x ∉ s₁.direction

Tactic:
use direction_le hle, p₂ -ᵥ p, vsub_mem_direction hp₂ (hle hp)

Premises used: AffineSubspace.direction_le, AffineSubspace.vsub_mem_direction
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ p₂ ∈ s₁

Tactic:
rw [vsub_right_mem_direction_iff_mem hp p₂] at hm

Premises used: AffineSubspace.vsub_right_mem_direction_iff_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂ ∈ s₁
⊢ False

Tactic:
hp₂s₁ hm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂ ∈ s₁
⊢ False

Tactic:
exact hp₂s₁ hm