[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✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty { x // x ∈ E }
φ : P₁ →ᵃ[k] P₂
⊢ Nonempty { x // x ∈ map φ E }
[PROOFSTEP]
obtain ⟨x, hx⟩ := id Ene
[GOAL]
case intro.mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty { x // x ∈ E }
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty { x // x ∈ map φ E }
[PROOFSTEP]
refine' ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩
[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✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ { x // x ∈ E } →ᵃ[k] { x // x ∈ F }
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case refine'_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ { x // x ∈ E } → { x // x ∈ F }
[PROOFSTEP]
exact fun x => ⟨φ x, hEF <| AffineSubspace.mem_map.mpr ⟨x, x.property, rfl⟩⟩
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ { x // x ∈ AffineSubspace.direction E } →ₗ[k] { x // x ∈ AffineSubspace.direction F }
[PROOFSTEP]
refine' φ.linear.restrict (_ : E.direction ≤ F.direction.comap φ.linear)
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)
[PROOFSTEP]
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction (AffineSubspace.map φ E) ≤ AffineSubspace.direction F
[PROOFSTEP]
exact AffineSubspace.direction_le hEF
[GOAL]
case refine'_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ ∀ (p : { x // x ∈ E }) (v : { x // x ∈ AffineSubspace.direction E }),
    { val := ↑φ ↑(v +ᵥ p), property := (_ : ↑φ ↑(v +ᵥ p) ∈ ↑F) } =
      ↑(LinearMap.restrict φ.linear
              (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)))
          v +ᵥ
        { val := ↑φ ↑p, property := (_ : ↑φ ↑p ∈ ↑F) }
[PROOFSTEP]
intro p v
[GOAL]
case refine'_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
p : { x // x ∈ E }
v : { x // x ∈ AffineSubspace.direction E }
⊢ { val := ↑φ ↑(v +ᵥ p), property := (_ : ↑φ ↑(v +ᵥ p) ∈ ↑F) } =
    ↑(LinearMap.restrict φ.linear
            (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)))
        v +ᵥ
      { val := ↑φ ↑p, property := (_ : ↑φ ↑p ∈ ↑F) }
[PROOFSTEP]
simp only [Subtype.ext_iff, Subtype.coe_mk, AffineSubspace.coe_vadd]
[GOAL]
case refine'_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
p : { x // x ∈ E }
v : { x // x ∈ AffineSubspace.direction E }
⊢ ↑φ (↑v +ᵥ ↑p) =
    ↑(↑(LinearMap.restrict φ.linear
              (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)))
          v) +ᵥ
      ↑φ ↑p
[PROOFSTEP]
apply AffineMap.map_vadd
[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✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)
[PROOFSTEP]
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
[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✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction (AffineSubspace.map φ E) ≤ AffineSubspace.direction F
[PROOFSTEP]
exact AffineSubspace.direction_le hEF
[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✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ Function.Injective ↑(restrict φ hEF)
[PROOFSTEP]
intro x y h
[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✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑(restrict φ hEF) x = ↑(restrict φ hEF) y
⊢ x = y
[PROOFSTEP]
simp only [Subtype.ext_iff, Subtype.coe_mk, AffineMap.restrict.coe_apply] at h ⊢
[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✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑φ ↑x = ↑φ ↑y
⊢ ↑x = ↑y
[PROOFSTEP]
exact hφ h
[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✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
⊢ Function.Surjective ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F))
[PROOFSTEP]
rintro ⟨x, hx : x ∈ F⟩
[GOAL]
case mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
x : P₂
hx : x ∈ F
⊢ ∃ a, ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F)) a = { val := x, property := hx }
[PROOFSTEP]
rw [← h, AffineSubspace.mem_map] at hx 
[GOAL]
case mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
x : P₂
hx✝ : x ∈ F
hx : ∃ y, y ∈ E ∧ ↑φ y = x
⊢ ∃ a, ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F)) a = { val := x, property := hx✝ }
[PROOFSTEP]
obtain ⟨y, hy, rfl⟩ := hx
[GOAL]
case mk.intro.intro
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
y : P₁
hy : y ∈ E
hx : ↑φ y ∈ F
⊢ ∃ a, ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F)) a = { val := ↑φ y, property := hx }
[PROOFSTEP]
exact ⟨⟨y, hy⟩, rfl⟩
