awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Set P)
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
right : r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁
⊢ ∃ (y : V),
    Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) y ∧ ∃ z ∈ s.direction, y + z = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Tactic:
use r • (p₂ -ᵥ p₁), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p₃ -ᵥ p₁,
      vsub_mem_direction hp₃ hp₁

Premises used: Iff.mpr, AffineSubspace.vsub_mem_direction, Submodule.mem_span_singleton, VSub.vsub, Exists.intro, 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
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
right right₁ : r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁)
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Tactic:
rw [vadd_vsub_assoc]

Premises used: vadd_vsub_assoc
-- 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₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
simp_rw :
  Eq (α := Submodule k V) (direction (affineSpan k (s₁ ∪ s₂)))
    (direction (affineSpan k s₁) ⊔ direction (affineSpan k s₂))
simp_rw₁ :
  Eq (α := Submodule k V) (direction (affineSpan k s₁ ⊔ affineSpan k s₂))
    (direction (affineSpan k s₁) ⊔ direction (affineSpan k s₂))
⊢ Eq (α := Submodule k V) (vectorSpan k (s₁ ∪ s₂)) (vectorSpan k s₁ ⊔ vectorSpan k s₂)

Tactic:
simp_rw [← direction_affineSpan, span_union,
    direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)]

Premises used: AffineSubspace.direction_sup_eq_sup_direction, direction_affineSpan, AffineSubspace.span_union, mem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ Submodule.map f.linear (vectorSpan k s) = vectorSpan.{u_1, u_4, u_5} k (P := P₂) ((⇑f : (a : P₁) → P₂) '' s)

Tactic:
simp [vectorSpan_def, f.image_vsub_image]

Premises used: vectorSpan_def, AffineMap.image_vsub_image
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
h :
  t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ Membership.mem (γ := Set P₂) ((⇑f : (a : P₁) → P₂) '' (↑s : Set P₁))
    (HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂))

Tactic:
use t • (p₁ -ᵥ p₂) +ᵥ p₃

Premises used: VSub.vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
simp :
  (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)

Tactic:
simp only [SetLike.mem_coe, true_and, this]

Premises used: SetLike.mem_coe, true_and
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
rw :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂) ((f.linear : (a : V₁) → V₂) (t • (p₁ -ᵥ p₂)) : V₂)
      ((f : (a : P₁) → P₂) p₃ : P₂) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
rw₁ :
  HVAdd.hVAdd (β := P₂) (HSMul.hSMul (β := V₂) t ((f.linear : (a : V₁) → V₂) (p₁ -ᵥ p₂) : V₂))
      ((f : (a : P₁) → P₂) p₃ : P₂) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
rw₂ rw₃ :
  HVAdd.hVAdd (β := P₂) (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)

Tactic:
rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]

Premises used: AffineMap.linearMap_vsub, AffineMap.map_vadd, map_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
simp :
  (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
    HVAdd.hVAdd (β := P₂)
      (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
      ((f : (a : P₁) → P₂) p₃ : P₂)
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)

Tactic:
{ simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }

Premises used: AffineMap.linearMap_vsub, AffineMap.map_vadd, SetLike.mem_coe, true_and, map_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
h : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s : Set P₁) ∧
    (f : (a : P₁) → P₂) (t • (p₁ -ᵥ p₂) +ᵥ p₃) =
      HVAdd.hVAdd (β := P₂)
        (t • VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P₁) → P₂) p₁ : P₂) ((f : (a : P₁) → P₂) p₂ : P₂))
        ((f : (a : P₁) → P₂) p₃ : P₂)

Tactic:
suffices t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s by
    { simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s

Tactic:
s.smul_vsub_vadd_mem t 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
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ (↑s : Set P₁)
p₂ : P₁
h₂ : p₂ ∈ (↑s : Set P₁)
p₃ : P₁
h₃ : p₃ ∈ (↑s : Set P₁)
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s

Tactic:
exact s.smul_vsub_vadd_mem t 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
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ (↑(map f s) : Set P₂) = (⇑f : (a : P₁) → P₂) '' (↑s : Set P₁)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
x : P₂
s : AffineSubspace k P₁
⊢ x ∈ map f s ↔ ∃ y ∈ s, (f : (a : P₁) → P₂) y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
x : P₁
s : AffineSubspace k P₁
h : x ∈ s
⊢ Membership.mem (α := P₂) (map f s) ((f : (a : P₁) → P₂) x : P₂)

Tactic:
Set.mem_image_of_mem _ h

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
x : P₁
s : AffineSubspace k P₁
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
⊢ Membership.mem (α := P₂) (map f s) ((f : (a : P₁) → P₂) x : P₂) ↔ x ∈ s

Tactic:
hf.mem_set_image

Premises used: Set.Mem, setOf, Set.image, Function.Injective.mem_set_image
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ map f ⊥ = ⊥

Tactic:
coe_injective <| image_empty f

Premises used: AffineSubspace.coe_injective, DFunLike.coe, Set.image_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ map f s = ⊥ ↔ s = ⊥

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

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
refine_1 : ∀ (h : map f s = ⊥), s = ⊥
refine_2 : ∀ (h : s = ⊥), map f s = ⊥
⊢ map f s = ⊥ ↔ s = ⊥

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
refine_1 : ∀ (h : (↑(map f s) : Set P₂) = ∅), s = ⊥
refine_1₁ : ∀ (h : Eq.{u_5 + 1} (α := Set P₂) ((⇑f : (a : P₁) → P₂) '' (↑s : Set P₁)) ∅), s = ⊥
refine_1₂ : ∀ (h : (↑s : Set P₁) = ∅), s = ⊥
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : ∀ (h : s = ⊥), s = ⊥
⊢ s = ⊥

Tactic:
rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h

Premises used: Set.image_eq_empty, AffineSubspace.coe_eq_bot_iff, AffineSubspace.coe_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : s = ⊥
refine_2 : map f ⊥ = ⊥
refine_2₁ refine_2₂ : Eq.{u_5 + 1} (α := AffineSubspace k P₂) ⊥ ⊥
⊢ map f s = ⊥

Tactic:
rw [h, map_bot]

Premises used: AffineSubspace.map_bot
-- 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₁
⊢ map (AffineMap.id k P₁) s = s

Tactic:
coe_injective <| image_id _

Premises used: AffineSubspace.coe_injective, Set.image_id
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : AddCommGroup V₃
inst_8 : Module k V₃
inst_9 : AffineSpace V₃ P₃
s : AffineSubspace k P₁
f : P₁ →ᵃ[k] P₂
g : P₂ →ᵃ[k] P₃
⊢ map g (map f s) = map (g.comp f) s

Tactic:
coe_injective <| image_image _ _ _

Premises used: Set.image_image, AffineSubspace.coe_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ (map f s).direction = Submodule.map f.linear s.direction

Tactic:
simp [direction_eq_vectorSpan, AffineMap.map_vectorSpan]

Premises used: AffineMap.map_vectorSpan, AffineSubspace.direction_eq_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
inl : map f (affineSpan k ∅) = affineSpan k (image.{u_3, u_5} (α := P₁) (⇑f : (a : P₁) → P₂) ∅)
inr : ∀ (p : P₁) (hp : p ∈ s), map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)
⊢ map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ map f (affineSpan k ∅) = affineSpan k (image.{u_3, u_5} (α := P₁) (⇑f : (a : P₁) → P₂) ∅)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
inr :
  (map f (affineSpan k s)).direction = direction.{u_1, u_4, u_5} (P := P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s))
inr₁ : ((↑(map f (affineSpan k s)) : Set P₂) ∩ (↑(affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) : Set P₂)).Nonempty
⊢ map f (affineSpan k s) = affineSpan k ((⇑f : (a : P₁) → P₂) '' s)

Tactic:
apply ext_of_direction_eq

Premises used: AffineSubspace.ext_of_direction_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ (map f (affineSpan k s)).direction = direction.{u_1, u_4, u_5} (P := P₂) (affineSpan k ((⇑f : (a : P₁) → P₂) '' s))

Tactic:
simp [direction_affineSpan]

Premises used: direction_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ ((↑(map f (affineSpan k s)) : Set P₂) ∩ (↑(affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) : Set P₂)).Nonempty

Tactic:
⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp),
          subset_affineSpan k _ (mem_image_of_mem f hp)⟩

Premises used: subset_affineSpan, Set.Nonempty, Set.mem_image_of_mem, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ ((↑(map f (affineSpan k s)) : Set P₂) ∩ (↑(affineSpan k ((⇑f : (a : P₁) → P₂) '' s)) : Set P₂)).Nonempty

Tactic:
exact ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp),
          subset_affineSpan k _ (mem_image_of_mem f hp)⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s₁ s₂ : AffineSubspace k P₁
h : s₁ ≤ s₂
⊢ map f s₁ ≤ map f s₂

Tactic:
Set.image_mono h

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s₁ s₂ : AffineSubspace k P₁
⊢ map f (s₁ ⊓ s₂) ≤ map f s₁ ⊓ map f s₂

Tactic:
le_inf (map_mono _ inf_le_left) (map_mono _ inf_le_right)

Premises used: inf_le_right, le_inf, inf_le_left, AffineSubspace.map_mono
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
s₁ s₂ : AffineSubspace k P₁
h : ∀ (p : P₂), p ∈ map f (s₁ ⊓ s₂) ↔ p ∈ map f s₁ ⊓ map f s₂
⊢ map f (s₁ ⊓ s₂) = map f s₁ ⊓ map f s₂

Tactic:
ext p
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑f : (a : P₁) → P₂)
s₁ s₂ : AffineSubspace k P₁
p : P₂
⊢ (∃ (y : P₁), (y ∈ s₁ ∧ y ∈ s₂) ∧ (f : (a : P₁) → P₂) y = p) ↔
    (∃ y ∈ s₁, (f : (a : P₁) → P₂) y = p) ∧ ∃ y ∈ s₂, (f : (a : P₁) → P₂) y = p

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
h :
  ∀ (q : P₂),
    q ∈ map f (mk' p direction) ↔
      Membership.mem (γ := AffineSubspace k P₂)
        (mk' ((f : (a : P₁) → P₂) p) (Submodule.map f.linear direction) : AffineSubspace k P₂) q
⊢ map f (mk' p direction) = mk' ((f : (a : P₁) → P₂) p) (Submodule.map f.linear direction)

Tactic:
ext q
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
q : P₂
h :
  (∃ (y : P₁), y -ᵥ p ∈ direction ∧ (f : (a : P₁) → P₂) y = q) ↔
    ∃ y ∈ direction, (f.linear : (a : V₁) → V₂) y = q -ᵥ (f : (a : P₁) → P₂) p
⊢ q ∈ map f (mk' p direction) ↔
    Membership.mem (γ := AffineSubspace k P₂)
      (mk' ((f : (a : P₁) → P₂) p) (Submodule.map f.linear direction) : AffineSubspace k P₂) q

Tactic:
simp only [mem_map, mem_mk', Submodule.mem_map]

Premises used: Submodule.mem_map, AffineSubspace.mem_map, AffineSubspace.mem_mk'