Theorem: AffineMap.preimage_convexHull (src/Pre.lean)

State before:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
⊢ ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)
Tactic:
have h1 := Set.image_preimage_eq_of_subset hs
State after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
⊢ ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)

State before:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
⊢ ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)
Tactic:
ext x
State after:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
x : E
⊢ x ∈ ⇑f ⁻¹' (convexHull 𝕜) s ↔ x ∈ (convexHull 𝕜) (⇑f ⁻¹' s)

State before:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
x : E
⊢ x ∈ ⇑f ⁻¹' (convexHull 𝕜) s ↔ x ∈ (convexHull 𝕜) (⇑f ⁻¹' s)
Tactic:
rw [Set.mem_preimage, ← Function.Injective.mem_set_image hf, AffineMap.toFun_eq_coe, AffineMap.image_convexHull, h1]
State after:
no goals