awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
e_f :
  f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) =
    AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f
⊢ map (f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁)) s =
    map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f) s

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
e_f :
  ∀ (p : P₁),
    Eq.{u_8 + 1} (α := P₂) ((f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) : (a : P₁) → P₂) p : P₂)
      ((AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f : (a : P₁) → P₂)
          p :
        P₂)
⊢ f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) =
    AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
p : P₁
⊢ Eq.{u_8 + 1} (α := P₂) ((f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) : (a : P₁) → P₂) p : P₂)
    ((AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f : (a : P₁) → P₂) p :
      P₂)

Tactic:
f.map_vadd _ _

Premises used: AffineMap.map_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
p : P₁
⊢ Eq.{u_8 + 1} (α := P₂) ((f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) : (a : P₁) → P₂) p : P₂)
    ((AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f : (a : P₁) → P₂) p :
      P₂)

Tactic:
exact f.map_vadd _ _

Premises used: AffineMap.map_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : DistribSMul M V
inst_4 : SMulCommClass M k V
a : M
s : AffineSubspace k V
⊢ (↑(a • s) : Set V) = a • (↑s : Set V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : DistribSMul M V
inst_4 : SMulCommClass M k V
a : M
s : AffineSubspace k V
⊢ a • s = map (LinearMap.toAffineMap (DistribSMul.toLinearMap k V a)) s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : AffineSubspace k V
p : V
G : Type u_9
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
⊢ a • p ∈ a • s ↔ p ∈ s

Tactic:
smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : DistribSMul M V
inst_4 : SMulCommClass M k V
a : M
h : ∀ (x : V), x ∈ HSMul.hSMul (β := AffineSubspace k V) a ⊥ ↔ Membership.mem (γ := AffineSubspace k V) ⊥ x
⊢ HSMul.hSMul (β := AffineSubspace k V) a ⊥ = ⊥

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : DistribSMul M V
inst_4 : SMulCommClass M k V
a : M
x : V
⊢ x ∈ HSMul.hSMul (β := AffineSubspace k V) a ⊥ ↔ Membership.mem (γ := AffineSubspace k V) ⊥ x

Tactic:
simp [smul_eq_map, map_bot]

Premises used: AffineSubspace.smul_eq_map, AffineSubspace.map_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : DistribSMul M V
inst_4 : SMulCommClass M k V
a : M
s : Set V
⊢ HSMul.hSMul (β := AffineSubspace k V) a (affineSpan k s) = affineSpan k (a • s)

Tactic:
map_span _ s

Premises used: AffineSubspace.map_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Monoid M
inst_4 : DistribMulAction M V
inst_5 : SMulCommClass M k V
a : M
s : AffineSubspace k V
p : V
ha : IsUnit a
⊢ a • p ∈ a • s ↔ p ∈ s

Tactic:
smul_mem_smul_iff (a := ha.unit)

Premises used: Units.copy, DistribSMul.toLinearMap, Set.Mem, AffineSubspace.smul_mem_smul_iff, IsUnit.unit
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : AffineSubspace k V
p : V
G₀ : Type u_9
inst_3 : GroupWithZero G₀
inst_4 : DistribMulAction G₀ V
inst_5 : SMulCommClass G₀ k V
a : G₀
ha : a ≠ 0
⊢ a • p ∈ a • s ↔ p ∈ s

Tactic:
smul_mem_smul_iff_of_isUnit ha.isUnit

Premises used: Ne.isUnit, AffineSubspace.smul_mem_smul_iff_of_isUnit
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Monoid M
inst_4 : DistribMulAction M V
inst_5 : SMulCommClass M k V
a : M
ha : IsUnit a
h : ∀ (x : V), x ∈ HSMul.hSMul (β := AffineSubspace k V) a ⊤ ↔ Membership.mem (γ := AffineSubspace k V) ⊤ x
⊢ HSMul.hSMul (β := AffineSubspace k V) a ⊤ = ⊤

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Monoid M
inst_4 : DistribMulAction M V
inst_5 : SMulCommClass M k V
a : M
ha : IsUnit a
x : V
⊢ x ∈ HSMul.hSMul (β := AffineSubspace k V) a ⊤ ↔ Membership.mem (γ := AffineSubspace k V) ⊤ x

Tactic:
simpa [smul_eq_map, map_top] using ⟨ha.unit⁻¹ • x, smul_inv_smul ha.unit _⟩

Premises used: AffineSubspace.smul_eq_map, TopHomClass.map_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
h :
  ∀ (x : V),
    Eq (α := V) ((DistribSMul.toLinearMap k V a : (a : V) → V) x : V)
      ((HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id : (a : V) → V) x : V)
⊢ DistribSMul.toLinearMap k V a = HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
x : V
⊢ Eq (α := V) ((DistribSMul.toLinearMap k V a : (a : V) → V) x : V)
    ((HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
⊢ DistribSMul.toLinearMap k V a = HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id

Tactic:
have : DistribSMul.toLinearMap k V a = a • LinearMap.id := by
    ext; simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise
Goal:
k : Type u_2
V : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
this : DistribSMul.toLinearMap k V a = HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id
⊢ (a • s).direction = s.direction

Tactic:
simp [smul_eq_map, map_direction, this, Submodule.map_smul, ha]

Premises used: AffineSubspace.map_direction, AffineSubspace.smul_eq_map, Submodule.map_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty.{u_3 + 1} ↥E
φ : P₁ →ᵃ[k] P₂
obtain : ∀ (x : P₁) (hx : x ∈ E), Nonempty.{u_5 + 1} ↥(map φ E)
⊢ Nonempty.{u_5 + 1} ↥(map φ E)

Tactic:
obtain ⟨x, hx⟩ := id Ene

Premises used: id
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty.{u_3 + 1} ↥E
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty.{u_5 + 1} ↥(map φ E)

Tactic:
⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩

Premises used: Iff.mpr, AffineSubspace.mem_map, Nonempty.intro, Subtype.mk, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty.{u_3 + 1} ↥E
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty.{u_5 + 1} ↥(map φ E)

Tactic:
exact ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
refine_1 : ↥E → ↥F
refine_2 : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction
refine_3 :
  ∀ (p : ↥E) (v : ↥E.direction),
    Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑(v +ᵥ p) : P₁)) ⋯ =
      HVAdd.hVAdd.{u_4, u_5, u_5} (α := ↥F.direction) (β := ↥F)
        (((φ.linear.restrict ⋯ : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
              (a : ↥E.direction) → ↥F.direction)
            v :
          ↥F.direction)
        (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑p : P₁)) ⋯ : ↥F)
⊢ AffineMap.{u_1, u_2, u_3, u_4, u_5} k ↥E ↥F

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ↥E → ↥F

Tactic:
exact fun x => ⟨φ x, hEF <| AffineSubspace.mem_map.mpr ⟨x, x.property, rfl⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
refine_2 : E.direction ≤ Submodule.comap φ.linear F.direction
⊢ LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction

Tactic:
refine φ.linear.restrict (?_ : E.direction ≤ F.direction.comap φ.linear)

Premises used: LinearMap.restrict, AffineMap.linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
refine_2 : (AffineSubspace.map φ E).direction ≤ F.direction
⊢ E.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]

Premises used: AffineSubspace.map_direction, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
AffineSubspace.direction_le hEF

Premises used: AffineSubspace.direction_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
exact AffineSubspace.direction_le hEF

Premises used: AffineSubspace.direction_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
p : ↥E
v : ↥E.direction
refine_3 :
  (φ : (a : P₁) → P₂) ((↑v : V₁) +ᵥ (↑p : P₁)) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂)
      (↑(((φ.linear.restrict ⋯ : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
              (a : ↥E.direction) → ↥F.direction)
            v) :
        V₂)
      ((φ : (a : P₁) → P₂) (↑p : P₁) : P₂)
⊢ Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑(v +ᵥ p) : P₁)) ⋯ =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := ↥F.direction) (β := ↥F)
      (((φ.linear.restrict ⋯ : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
            (a : ↥E.direction) → ↥F.direction)
          v :
        ↥F.direction)
      (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑p : P₁)) ⋯ : ↥F)

Tactic:
simp only [Subtype.ext_iff, AffineSubspace.coe_vadd]

Premises used: AffineSubspace.coe_vadd, Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
p : ↥E
v : ↥E.direction
⊢ (φ : (a : P₁) → P₂) ((↑v : V₁) +ᵥ (↑p : P₁)) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂)
      (↑(((φ.linear.restrict ⋯ : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
              (a : ↥E.direction) → ↥F.direction)
            v) :
        V₂)
      ((φ : (a : P₁) → P₂) (↑p : P₁) : P₂)

Tactic:
apply AffineMap.map_vadd

Premises used: AffineMap.map_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
x : ↥E
⊢ Eq.{u_5 + 1} (α := P₂) ((↑((φ.restrict hEF : (a : ↥E) → ↥F) x) : P₂) : P₂) ((φ : (a : P₁) → P₂) (↑x : P₁) : P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
rw : (AffineSubspace.map φ E).direction ≤ F.direction
⊢ E.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]

Premises used: AffineSubspace.map_direction, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
AffineSubspace.direction_le hEF

Premises used: AffineSubspace.direction_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
exact AffineSubspace.direction_le hEF

Premises used: AffineSubspace.direction_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineMap.linear (φ.restrict hEF) = φ.linear.restrict ⋯

Tactic:
rfl

Premises used: LinearMap.restrict, LinearMap.codRestrict, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑φ : (a : P₁) → P₂)
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : Eq.{u_5 + 1} (α := ↥F) ((φ.restrict hEF : (a : ↥E) → ↥F) x : ↥F) ((φ.restrict hEF : (a : ↥E) → ↥F) y : ↥F)
simp :
  ∀ (h : Eq.{u_5 + 1} (α := P₂) ((φ : (a : P₁) → P₂) (↑x : P₁) : P₂) ((φ : (a : P₁) → P₂) (↑y : P₁) : P₂)),
    (↑x : P₁) = (↑y : P₁)
⊢ x = y

Tactic:
simp only [Subtype.ext_iff, AffineMap.restrict.coe_apply] at h ⊢

Premises used: Subtype.ext_iff, AffineMap.restrict.coe_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑φ : (a : P₁) → P₂)
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : Eq.{u_5 + 1} (α := P₂) ((φ : (a : P₁) → P₂) (↑x : P₁) : P₂) ((φ : (a : P₁) → P₂) (↑y : P₁) : P₂)
⊢ (↑x : P₁) = (↑y : P₁)

Tactic:
hφ h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑φ : (a : P₁) → P₂)
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : Eq.{u_5 + 1} (α := P₂) ((φ : (a : P₁) → P₂) (↑x : P₁) : P₂) ((φ : (a : P₁) → P₂) (↑y : P₁) : P₂)
⊢ (↑x : P₁) = (↑y : P₁)

Tactic:
exact hφ h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
h : AffineSubspace.map φ E = F
x : P₂
hx : x ∈ F
⊢ ∃ y ∈ E, (φ : (a : P₁) → P₂) y = x

Tactic:
rw [← h, AffineSubspace.mem_map] at hx

Premises used: AffineSubspace.mem_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
h : AffineSubspace.map φ E = F
x : P₂
hx_1 : x ∈ F
hx : ∃ y ∈ E, (φ : (a : P₁) → P₂) y = x
obtain :
  ∀ (y : P₁) (hy : y ∈ E) (hx : Membership.mem (α := P₂) F ((φ : (a : P₁) → P₂) y : P₂)),
    ∃ (a : ↥E),
      Eq.{u_5 + 1} (α := ↥F) ((φ.restrict ⋯ : (a : ↥E) → ↥F) a : ↥F)
        (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) y) hx : ↥F)
⊢ ∃ (a : ↥E), (φ.restrict ⋯ : (a : ↥E) → ↥F) a = Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) x hx_1

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
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 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
h : AffineSubspace.map φ E = F
y : P₁
hy : y ∈ E
hx : Membership.mem (α := P₂) F ((φ : (a : P₁) → P₂) y : P₂)
⊢ ∃ (a : ↥E),
    Eq.{u_5 + 1} (α := ↥F) ((φ.restrict ⋯ : (a : ↥E) → ↥F) a : ↥F)
      (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) y) hx : ↥F)

Tactic:
⟨⟨y, hy⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl