Why does this work?

Stream: new members

[Dominic Steinitz]

I expect h8 to give an error but it does not. Why? I checked that somehow that x was already 0 by trying

    have h7 : x = 0 := by exact?

between h6 and h8 but no proof could be found.

import Mathlib

example (x : EuclideanSpace ℝ (Fin 1))
 (f : PartialHomeomorph (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)
                        (EuclideanSpace ℝ (Fin 1))) :
  ((f.symm x).val (0 : Fin 2)) = 0 ↔ x 0 = 0 := by
  constructor
  · have h1 : f (f.symm 0) = 0 :=
      PartialHomeomorph.right_inv f (sorry : 0 ∈ f.target)
    have h2 : f (f.symm x) = x :=
      PartialHomeomorph.right_inv f (sorry : 0 ∈ f.target)
    exact sorry
  · exact sorry

instance : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
  ⟨(finrank_euclideanSpace_fin : Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2)⟩

def north' := (!₂[0, 1] : EuclideanSpace ℝ (Fin 2))

theorem hnorth : north' ∈ Metric.sphere 0 1 := by
  rw [EuclideanSpace.sphere_zero_eq 1 (by norm_num)]
  simp [north']

def north_pt := (⟨north', hnorth⟩ : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)

example (x : EuclideanSpace ℝ (Fin 1)) :
  ((stereographic' 1 north_pt).symm x).val 0 = 0 ↔ x 0 = 0 := by
  constructor
  · intro hx
    have h6 : (stereographic' 1 north_pt) ((stereographic' 1 north_pt).symm 0) = 0 :=
      PartialHomeomorph.right_inv (stereographic' 1 north_pt)
       (sorry : 0 ∈ (stereographic' 1 north_pt).target)
    have h8 : (stereographic' 1 north_pt) ((stereographic' 1 north_pt).symm x) = x :=
      PartialHomeomorph.right_inv (stereographic' 1 north_pt)
       -- Surely this should be
       -- (sorry : x ∈ (stereographic' 1 north_pt).target)
       -- ????
       (sorry : 0 ∈ (stereographic' 1 north_pt).target)
    exact sorry
  · intro hx
    exact sorry

[Dominic Steinitz]

I should have said that the first example fails with the error I would expect in the second example.

[Kevin Buzzard]

       (sorry : 37 • x ∈ (stereographic' 1 north_pt).target)

also works. Very surprising!

[Kyle Miller]

Maybe it doesn't matter because docs#stereographic'_target, which says the target is Set.univ?

It turns out this works:

    let h8 : (stereographic' 1 north_pt) ((stereographic' 1 north_pt).symm x) = x :=
      PartialHomeomorph.right_inv (stereographic' 1 north_pt)
       (And.intro trivial trivial)

(That's not meant to be a suggestion! Just an observation. Better is (by simp).)