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 }
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))
rintro ⟨x, hx : x ∈ F⟩
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✝ }
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 }
rw [← h, AffineSubspace.mem_map] at hx
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 }
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✝ }
obtain ⟨y, hy, rfl⟩ := hx
no goals
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 }
exact ⟨⟨y, hy⟩, rfl⟩