case h
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ v ∈ ↑f '' s -ᵥ ↑f '' t ↔ v ∈ ↑f.linear '' (s -ᵥ t)
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
⊢ ↑f '' s -ᵥ ↑f '' t = ↑f.linear '' (s -ᵥ t)
ext v
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v) ↔
    ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ v ∈ ↑f '' s -ᵥ ↑f '' t ↔ v ∈ ↑f.linear '' (s -ᵥ t)
simp only [(Set.mem_vsub), Set.mem_image,
  exists_exists_and_eq_and, exists_and_left, ← f.linearMap_vsub]
case h.mp
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v) →
    ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v

case h.mpr
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v) →
    ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v) ↔
    ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
constructor
case h.mp.intro.intro.intro.intro
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
x : P1
hx : x ∈ s
y : P1
hy : y ∈ t
hv : ↑f.linear (x -ᵥ y) = v
⊢ ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
case h.mp
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v) →
    ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
rintro ⟨x, hx, y, hy, hv⟩
no goals
case h.mp.intro.intro.intro.intro
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
x : P1
hx : x ∈ s
y : P1
hy : y ∈ t
hv : ↑f.linear (x -ᵥ y) = v
⊢ ∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v
exact ⟨x -ᵥ y, ⟨x, hx, y, hy, rfl⟩, hv⟩
case h.mpr.intro.intro.intro.intro.intro.intro
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
x : P1
hx : x ∈ s
y : P1
hy : y ∈ t
⊢ ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = ↑f.linear (x -ᵥ y)
case h.mpr
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ (∃ x, (∃ x_1, x_1 ∈ s ∧ ∃ x_2, x_2 ∈ t ∧ x_1 -ᵥ x_2 = x) ∧ ↑f.linear x = v) →
    ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = v
rintro ⟨-, ⟨x, hx, y, hy, rfl⟩, rfl⟩
no goals
case h.mpr.intro.intro.intro.intro.intro.intro
k : Type u_2
V1 : Type u_3
P1 : Type u_1
V2 : Type u_4
P2 : Type u_5
V3 : Type ?u.378511
P3 : Type ?u.378514
V4 : Type ?u.378517
P4 : Type ?u.378520
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
s t : Set P1
f : P1 →ᵃ[k] P2
x : P1
hx : x ∈ s
y : P1
hy : y ∈ t
⊢ ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ t ∧ ↑f.linear (a -ᵥ a_1) = ↑f.linear (x -ᵥ y)
exact ⟨x, hx, y, hy, rfl⟩