spheres

Stream: new members

[Greg Langmead]

I am trying to construct unit n-spheres and prove they are smooth manifolds. I'm stuck at proving that stereographic projection is continuous. The chat room has already helped me prove continuity of a similar function on a subset of ℝ×ℝ (over in 'noob questions') but adding fin to the mix has me lost again. The function now has two arguments: a point on the sphere and the fin from the codomain of euclidean space, hence continuous.mul does not apply directly ("does not unify"). (Meta: I feel like I'm lacking some general principles to get myself unstuck in these situations!)

import geometry.manifold.real_instances

noncomputable theory

-- note: def euclidean_space (n : ℕ) : Type := (fin n → ℝ)

-- Unit sphere of dimension n, inside euclidean space of dimension n + 1
def unit_sphere (n : ℕ) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}
instance sphere_top_space (n : ℕ) : topological_space (unit_sphere n) := subtype.topological_space
instance sphere_has_coe_to_euclidean_space (n : ℕ) : has_coe (unit_sphere n) (euclidean_space (n + 1)) := coe_subtype

-- The unit sphere minus its north pole will be a coordinate chart via stereographic projection
def unit_sphere_minus_north_pole (n : ℕ) := { x : unit_sphere n // ((x : (euclidean_space (n + 1))) n) ≤ 1 }
instance sphere_minus_np_top_space (n : ℕ) : topological_space (unit_sphere_minus_north_pole n) := subtype.topological_space
instance sphere_minus_np_has_coe_to_sphere (n : ℕ) : has_coe (unit_sphere_minus_north_pole n) (unit_sphere n) := coe_subtype
instance sphere_minus_np_has_coe_to_euclidean_space (n : ℕ) : has_coe (unit_sphere_minus_north_pole n) (euclidean_space (n + 1)) := sorry

def stereographic_projection_north (n : ℕ) : (unit_sphere_minus_north_pole (n + 1)) → (euclidean_space (n + 1)) :=
  λ sphere i, ((sphere : euclidean_space (n + 2)) i) * (1 - ((sphere : euclidean_space (n + 2)) (n + 1)))⁻¹

lemma continuous_sp_north (n:ℕ) : continuous (stereographic_projection_north n) :=
begin
  unfold stereographic_projection_north,
  apply continuous.mul, -- fails to unify
end

[Sebastien Gouezel]

Currently, there is only one explicit example of a smooth manifold in mathlib. It is the closed interval, endowed with a manifold with boundary structure, in the file real_instances.lean. You could take this as an example to see how things go. To define a smooth manifold structure, you need two things: an atlas (i.e., a set of local homeomorphisms between parts of your space and parts of euclidean space), and then a proof that the change of coordinates of member of this atlas are smooth. So, the first thing you need is the atlas.

An atlas is made of local homeos, called charts. For the closed interval, the first chart is defined at https://github.com/leanprover-community/mathlib/blob/b36831204c0db0c18b35918b56ffd3df55707c9e/src/geometry/manifold/real_instances.lean#L202 . There, you can see that there is a subtlety in the definition of local homeos: to avoid subtype problems that you are running into, they are not defined on subtypes of the space, but on subsets (and then the function defining your local homeo is defined everywhere, not only on your subset, but the values outside of it are just garbage). So, you should change your code to define unit_sphere_minus_north_pole as a subset of the sphere (which means that you can avoid some instances you are declaring). Of course, the functions will only be continuous on the subset where they make sense, which means that you will use continuous_on instead of continuous in most your proofs.

Here is a skeleton of what your construction might look like, with a lot of sorries that you would need to fill in:

variable (n : ℕ)

def unit_sphere := {x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}
instance sphere_top_space : topological_space (unit_sphere n) := subtype.topological_space
instance sphere_has_coe_to_euclidean_space : has_coe (unit_sphere n) (euclidean_space (n + 1)) := coe_subtype

-- The unit sphere minus its north pole will be a coordinate chart via stereographic projection
def unit_sphere_minus_north_pole (n : ℕ) : set (unit_sphere n) :=
  {x | (x : (euclidean_space (n + 1))) n < 1}

def stereographic_projection_north_local_equiv : local_equiv (unit_sphere n) (euclidean_space n) :=
{ source := unit_sphere_minus_north_pole n,
  target := univ,
  to_fun := λ sphere, (λi, ((sphere : euclidean_space (n + 1)) i) * (1 - ((sphere : euclidean_space (n + 1)) (n + 1)))⁻¹),
  inv_fun := λx, sorry, -- put the formula for the element of the sphere which is the inverse of
    -- x under the stereographic projection
  map_source := sorry, -- all these fields say that the functions `to_fun` and `inv_fun` are inverse
  map_target := sorry, -- to each other on the sets `source` and `target`
  left_inv := sorry,
  right_inv := sorry }

def stereographic_projection_north : local_homeomorph (unit_sphere n) (euclidean_space n) :=
{
  ..stereographic_projection_north_local_equiv n }

If you put your cursor in vscode on the opening brace of stereographic_projection_north, you will see that there are fields in local_homeomorph that I have not mentioned but that need filling (i.e., open_source, open_target, continuous_to_fun, continuous_inv_fun). But before trying to do the continuity proofs, I think you should try to complete the definition of the local equivalence, i.e., give the formula for the inverse of the stereographic projection and check that you indeed have a bijection.

[Yury G. Kudryashov]

BTW, why do we need the atlas? Why not say "for any point its chart satisfies" instead of "for any member of the atlas"?

[Sebastien Gouezel]

Right now, we have an atlas, and for each point x in the manifold we have a chosen member of the atlas that contains x in its domain, and that we call chart_at x. We could definitely replace the atlas by the set of all chart_at x for x in the manifold, and it wouldn't change anything (essentially no gain or no loss from what I could tell). The usual math approach is to have an atlas, though, so I decided to stick with it just for familiarity reasons.

[Patrick Massot]

Let me write once again that our current definition of manifold is nothing familiar to mathematicians, and should be called charted_space so I'd be open to modifying the definition if Yuri thinks it would make things simpler.

[Sebastien Gouezel]

I would agree to rename it charted_space. But still, I would keep the atlas to help mathematicians.

[Johan Commelin]

Will that change implicitly mean that there will typically be infinitely many charts?

[Johan Commelin]

If so, I would prefer to keep the atlas. For some definitions it is important to have a finite atlas.

[Johan Commelin]

(And to be able to talk about this finiteness)

[Sebastien Gouezel]

Many points can have the same chart, so no it does not imply that there are typically infinitely many charts. But in any case this kind of discussion is easier to do with the atlas, so this is one more reason to keep it.

[Yury G. Kudryashov]

Then I propose to add a constructor setting atlas to be there range of chart_at

[Yury G. Kudryashov]

@Patrick Massot Is it not "manifold" because we fix the best chart for each point or because of something else?

[Yury G. Kudryashov]

Then I propose to add a constructor setting atlas to be there range of chart_at

[Patrick Massot]

The best chart function is a tiny implementation detail that is not visible in the real world where we simply choose a chart whenever we need one. The reason mathlib manifold is not a manifold structure is much deeper. There is no maximality condition on the atlas (and no equivalence class of atlases). Adding a compatible chart to a mathlib manifold gives you a new manifold.

[Yury G. Kudryashov]

The best chart function contributes to this.

[Greg Langmead]

If a smooth manifold is a topological manifold together with its atlas then you do get a new one by adding a compatible chart, but of course they are diffeomorphic. Sometimes we have some equivalence class in mind and this detail is a distraction. Could Lean's quotients help define the equivalence class in a way that lets us work in both approaches? (Having a multiplicity of approaches feels right to me -- many equivalent definitions and proofs that they are equivalent.)

[Greg Langmead]

I took the suggestions of @Sebastien Gouezel, and have a new question. I'm defining the inverse of stereographic projection, the function that maps euclidean space of dimension n back into the sphere of dimension n, living in euclidean space of dimension n+1. The lambda doesn't typecheck -- where, in what structure, do I provide the proof that the image of this map is in fact contained in the sphere?

def unit_sphere_minus_north_pole (n) : set (unit_sphere n) :=
  {x | (x : (euclidean_space (n + 1))) n < 1}

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, (λ(i : fin (n + 1)), if lt : i.val < n
    then 2 * (x (fin_upgrade n i lt)) / (1 + finset.univ.sum (λ i, (x i) ^ 2))
    else (-1 + finset.univ.sum (λ i, (x i) ^ 2)) / (1 + finset.univ.sum (λ i, (x i) ^ 2)))

This doesn't typecheck, it says

type mismatch, term
  λ (x : euclidean_space n) (i : fin (n + 1)),
    dite (i.val < n)
      (λ (lt : i.val < n), 2 * x (fin_upgrade n i lt) / (1 + finset.sum finset.univ (λ (i : fin n), x i ^ 2)))
      (λ (lt : ¬i.val < n),
         (-1 + finset.sum finset.univ (λ (i : fin n), x i ^ 2)) /
           (1 + finset.sum finset.univ (λ (i : fin n), x i ^ 2)))
has type
  euclidean_space n → fin (n + 1) → ℝ
but is expected to have type
  euclidean_space n → unit_sphere n

[Mario Carneiro]

unit_sphere is a subtype, right? So you need to have a proof after it:

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), if lt : i.val < n
    then 2 * (x (fin_upgrade n i lt)) / (1 + finset.univ.sum (λ i, (x i) ^ 2))
    else (-1 + finset.univ.sum (λ i, (x i) ^ 2)) / (1 + finset.univ.sum (λ i, (x i) ^ 2)),
sorry⟩

[Greg Langmead]

Yes unit_sphere is a subtype

def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

I added the sorry and it's a variation on the above error, but this gives me something to follow up on so I'll keep at it, thanks!

[Greg Langmead]

Currently I am trying to supply the proof that the inverse of stereographic projection lands in the sphere, but because it's a summation I don't know what sort of tools to use. The new hint tactic lists a few tactics that make progress but it's not really actionable since I can't assemble them into a proof so far. Am I looking for a combination of standard tactics like field_simp/norm_num/ring or is something additional needed due to the sum?

And as a meta-question, what techniques am I missing that would enable me to understand at least a sketch of what I need to do next? My only methods are to try a few tactics I know and see if they magically work. I don't know how to incrementally build something.

import geometry.manifold.real_instances
import tactic.hint

noncomputable theory

variable (n : ℕ)

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
  val := i.val,
  is_lt := lt
}

-- Unit sphere of dimension n, inside euclidean space of dimension n + 1
def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), (if lt : i.val < n
    then (2 * (x (fin_upgrade n i lt)) / (finset.univ.sum (λ j, (x j) ^ 2) + 1))
    else (((finset.univ.sum (λj, (x j)^2) - 1) / (finset.univ.sum (λ j, (x j)^2) + 1)))),
begin
  sorry,
  -- hint recommends: ring, norm_num, simp at *, dsimp at *
end
⟩

[Kevin Buzzard]

I would not take what hint recommends too seriously. It's supposed to be used for "simple" problems, and if you think this is simple then you're miscalibrated.

[Kevin Buzzard]

Looking at what you have, it seems to me that the first step is to break up the sum from 0 to n as a sum from 0 to n-1, plus the n'th term. This will enable you to get rid of the "if". Then you want to take the division outside the sum.

[Kevin Buzzard]

Then the question should become a question in ring theory, and you'll still have some work to do. But step 1 should be getting rid of the if and step 2 getting rid of the denominators.

[Kevin Buzzard]

finset.sum_range_succ :
  ∀ (f : ℕ → ?M_1) (n : ℕ), finset.sum (finset.range (nat.succ n)) f = f n + finset.sum (finset.range n) f

finset.sum_mul : finset.sum ?M_3 ?M_4 * ?M_5 = finset.sum ?M_3 (λ (x : ?M_1), ?M_4 x * ?M_5)

div_eq_mul_inv : ?M_3 / ?M_4 = ?M_3 * ?M_4⁻¹

[Kevin Buzzard]

This is kind of annoying because you don't have f : ℕ → ?M_1, you have f : fin n → ℝ

[Greg Langmead]

I'm not clear how I can get rid of the if. The codomain of this function is unit_sphere n which is in R^(n+1), so I need a lambda on fin (n + 1) which has two cases with different formulas. Here's the formula from R^2 to R^3:
pasted image
Once I have the function I need to prove its values have norm 1. Does Lean know that I should sum the square of all the cases of the if? Could I express the function in the first place as being divided by its own norm? Ooh maybe I should break this up into the composition of two functions: a nonzero function followed by dividing that function by its own norm.

[Kevin Buzzard]

Right. So your job is to prove that the sum of the squares of those entries is 1. My proposal is to write the sum as (the sum of the first $n$ things) plus (the last thing), then take out the factor $1+\sum_{i=0}^{n-1}X_i^2$, then you're reduced to proving $(-1+\sum_{i=0}^{n-1}X_i^2)^2+\sum_{i=0}^{n-1}(2X_i)^2=(1+\sum_{i=0}^{n-1}(X_i)^2)^2$, which you can do using $(a+b)^2=a^2+b^2+2ab$.

[Kevin Buzzard]

import geometry.manifold.real_instances

noncomputable theory

variable (n : ℕ)

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
  val := i.val,
  is_lt := lt
}

theorem finset.sum_univ_fin_eq_sum_range (n : ℕ) (f : fin n → ℝ) :
  finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f ⟨i, hi⟩ else 0) :=
begin
  set F : ℕ → ℝ := λ i, if hi : i < n then f ⟨i, hi⟩ else 0 with hF,
  have H : f = λ (i : fin n), F (i.val),
  { ext i,
    rw hF,
    show f i = dite (i.val < n) (λ (hi : i.val < n), f ⟨i.val, hi⟩) (λ (hi : ¬i.val < n), 0),
    rw dif_pos i.is_lt,
    cases i, refl,
  },
  rw H,
  rw ←finset.sum_image,
  { congr',
    -- ⊢ finset.image (λ (x : fin n), x.val) finset.univ = finset.range n
    ext j, -- sigh
    rw [finset.mem_range, finset.mem_image],
    split,
      rintro ⟨⟨j,hj⟩, _, rfl⟩,
      exact hj,
    intro hj,
    use ⟨j, hj⟩,
    split, apply finset.mem_univ, refl
  },
  intros _ _ _ _,
  exact fin.eq_of_veq,
end

theorem finset.sum_div {α : Type*} {s : finset α} (f : α → ℝ) (d : ℝ) : finset.sum s (λ a, f a / d) = finset.sum s f / d :=
begin
  by_cases hd : d = 0,
    rw [hd, div_zero],
    convert finset.sum_const_zero,
    ext _,
    rw div_zero,
  rw [div_eq_mul_inv, finset.sum_mul],
  congr',
end

def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

open finset

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), (if lt : i.val < n
    then (2 * (x (fin_upgrade n i lt)) / (finset.univ.sum (λ j, (x j) ^ 2) + 1))
    else (((finset.univ.sum (λj, (x j)^2) - 1) / (finset.univ.sum (λ j, (x j)^2) + 1)))),
begin
  rw [sum_univ_fin_eq_sum_range, sum_range_succ, dif_pos (nat.lt_succ_self n), dif_neg (lt_irrefl n)],
  suffices : ((sum univ (λ (j : fin n), x j ^ 2) - 1) / (sum univ (λ (j : fin n), x j ^ 2) + 1)) ^ 2 +
    (sum (range n) (λ (i : ℕ), if hi : i < n then (2 * x ⟨i, hi⟩)^2  else 0) / (sum univ (λ (j : fin n), x j ^ 2) + 1) ^ 2)
    = 1,
  { convert this using 2, clear this,
    rw ←sum_div,
    apply finset.sum_congr, refl,
    intros i hi,
    rw finset.mem_range at hi,
    rw dif_pos (lt_trans hi (nat.lt_succ_self n)),
    rw dif_pos hi,
    rw dif_pos hi,
    rw pow_div,
    congr',
  },
  rw pow_div,
  rw ←add_div,
  rw div_eq_one_iff_eq,
  swap, sorry, -- (sum univ (λ (j : fin n), x j ^ 2) + 1) ^ 2 ≠ 0
  rw [sub_eq_add_neg, pow_two, pow_two, add_mul_self_eq, add_mul_self_eq],
  rw [neg_mul_neg, mul_neg_one, mul_one, mul_one],
  rw add_comm,
  repeat {rw ←add_assoc},
  congr' 1,
  rw [add_assoc, add_left_comm],
  apply congr_arg,
  apply add_neg_eq_of_eq_add,
  rw [mul_sum, ←sum_add_distrib],
  rw sum_univ_fin_eq_sum_range,
  apply sum_congr, refl,
  intros i hi,
  rw mem_range at hi,
  rw [dif_pos hi, dif_pos hi],
  ring,
end
⟩

One sorry left: I need that $1+X^2+Y^2\not=0$ otherwise the result is false. Hang on...

[Patrick Massot]

example (x y : ℝ) : 1 + x^2 + y^2 ≠ 0 :=
by linarith [pow_two_nonneg x, pow_two_nonneg y]

[Kevin Buzzard]

yeah but it's a sum over fin n really. I've done it, I'm just editing.

[Patrick Massot]

I had read only the line after the code block...

[Kevin Buzzard]

Aren't you proud of sum_div? I didn't need d non-zero :-) However I needed it later on anyway :-(

[Kevin Buzzard]

import geometry.manifold.real_instances

noncomputable theory

variable (n : ℕ)

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
  val := i.val,
  is_lt := lt
}

theorem finset.image_val_univ_eq_range (n : ℕ) : finset.image (λ (x : fin n), x.val) finset.univ = finset.range n :=
begin
  ext j, -- sigh
  rw [finset.mem_range, finset.mem_image],
  split,
    rintro ⟨⟨j,hj⟩, _, rfl⟩,
    exact hj,
  intro hj,
  use ⟨j, hj⟩,
  split, apply finset.mem_univ, refl
end

theorem finset.sum_univ_fin_eq_sum_range (n : ℕ) (f : fin n → ℝ) :
  finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f ⟨i, hi⟩ else 0) :=
begin
  set F : ℕ → ℝ := λ i, if hi : i < n then f ⟨i, hi⟩ else 0 with hF,
  have H : f = λ (i : fin n), F (i.val),
  { ext i,
    rw hF,
    show f i = dite (i.val < n) (λ (hi : i.val < n), f ⟨i.val, hi⟩) (λ (hi : ¬i.val < n), 0),
    rw dif_pos i.is_lt,
    cases i, refl,
  },
  rw H,
  rw ←finset.sum_image,
  { congr',
    apply finset.image_val_univ_eq_range,
  },
  intros _ _ _ _,
  exact fin.eq_of_veq,
end

theorem finset.sum_div {α : Type*} {s : finset α} (f : α → ℝ) (d : ℝ) : finset.sum s (λ a, f a / d) = finset.sum s f / d :=
begin
  by_cases hd : d = 0,
    rw [hd, div_zero],
    convert finset.sum_const_zero,
    ext _,
    rw div_zero,
  rw [div_eq_mul_inv, finset.sum_mul],
  congr',
end

def unit_sphere (n) := { x : euclidean_space (n + 1) // finset.univ.sum (λ i, (x i) ^ 2) = 1}

open finset

def stereographic_projection_inv_north (n) : (euclidean_space n) → (unit_sphere n) :=
λx, ⟨λ(i : fin (n + 1)), (if lt : i.val < n
    then (2 * (x (fin_upgrade n i lt)) / (finset.univ.sum (λ j, (x j) ^ 2) + 1))
    else (((finset.univ.sum (λj, (x j)^2) - 1) / (finset.univ.sum (λ j, (x j)^2) + 1)))),
begin
  rw [sum_univ_fin_eq_sum_range, sum_range_succ, dif_pos (nat.lt_succ_self n), dif_neg (lt_irrefl n)],
  suffices : ((sum univ (λ (j : fin n), x j ^ 2) - 1) / (sum univ (λ (j : fin n), x j ^ 2) + 1)) ^ 2 +
    (sum (range n) (λ (i : ℕ), if hi : i < n then (2 * x ⟨i, hi⟩)^2  else 0) / (sum univ (λ (j : fin n), x j ^ 2) + 1) ^ 2)
    = 1,
  { convert this using 2, clear this,
    rw ←sum_div,
    apply finset.sum_congr, refl,
    intros i hi,
    rw finset.mem_range at hi,
    rw dif_pos (lt_trans hi (nat.lt_succ_self n)),
    rw dif_pos hi,
    rw dif_pos hi,
    rw pow_div,
    congr',
  },
  rw pow_div,
  rw ←add_div,
  rw div_eq_one_iff_eq,
  swap,
  { apply ne_of_gt,
    apply pow_pos,
    apply lt_of_lt_of_le zero_lt_one,
    apply le_add_of_nonneg_left',
    apply sum_nonneg,
    intros,
    rw pow_two,
    apply mul_self_nonneg,
  },
  rw [sub_eq_add_neg, pow_two, pow_two, add_mul_self_eq, add_mul_self_eq],
  rw [neg_mul_neg, mul_neg_one, mul_one, mul_one],
  rw add_comm,
  repeat {rw ←add_assoc},
  congr' 1,
  rw [add_assoc, add_left_comm],
  apply congr_arg,
  apply add_neg_eq_of_eq_add,
  rw [mul_sum, ←sum_add_distrib],
  rw sum_univ_fin_eq_sum_range,
  apply sum_congr, refl,
  intros i hi,
  rw mem_range at hi,
  rw [dif_pos hi, dif_pos hi],
  ring,
end
⟩

It looks to me like there are a couple of holes in the finset library, which made life a bit harder.

[Kevin Buzzard]

My Lean is rather amateurish at times, but I understand the system well enough to be able to muddle through. It would not surprise me at all if someone who knows how to code could halve the size of this code. There used to be something called the @Mario Carneiro ratio, where the game was that you wrote some code, and then Mario rewrote it, and your ratio was the number of lines of your code divided by the number of lines of his code. We mathematicians used to work on trying to get the ratio down below 5.

[Patrick Massot]

I haven't read the proof carefully, but clearly this is the opportunity to get some new sum lemmas. Maybe also use indicator?

[Sebastien Gouezel]

Kevin Buzzard said:

def fin_upgrade (n) (i : fin (n + 1)) (lt : i.val < n) : (fin n) := {
  val := i.val,
  is_lt := lt
}

This is called fin.cast_lt, I think.

[Greg Langmead]

Wow this is fantastic, huge thanks Kevin! I'll digest this post haste. @Sebastien Gouezel that fin_upgrade was mine, I didn't find fin.cast_lt. That's my ongoing problem. I neither know what steps Lean wants from me, nor how to find them when I happen to understand.

[Kevin Buzzard]

The rule is this: if it looks basic, it's there already. It might be heavily disguised (e.g. earlier today I was asking how to take a finite union of finite sets and it turns out that the answer has something to do with monads) but it will be there. The trick is working out what the right question is. If it's there, it might well have a fabulous API (e.g. checking that making each set bigger makes the union bigger might be just some crazy one line incomprehensible monad or filter proof, but it might also have a sensible name).

After a while you just realise exactly what the computer is asking you to do, and you become a precision user of the tools which are available to you. I just learnt by doing a wide range of mathematics at all levels and running into myriads of different problems and having them all solved for me by others here.

[Kevin Buzzard]

That code I posted earlier took me a couple of hours to write, but I never really got stuck. It would be great if a CS person could review it because then you might also be able to witness how the experts can write it in half the space and in a way which sometimes can be far far harder to understand.

[Kevin Buzzard]

All my proofs are in tactic mode and you can just step through them.

[Kevin Buzzard]

You can even step through the rewrites term by term, by clicking near the commas.

[Daniel Keys]

I have a statement that a set is non-empty and need to produce a statement that a member of that set exists. Something along this line:

variable {X  : Type u}
variable set1 : set X
variable nonEmptySetProp : ¬ (set1 = ∅)

and need to produce ∃ x, x ∈ set1. The only thing I can find in data/set/basic is set.exists_mem_of_nonempty which doesn't work here. Any idea how to proceed appreciated!

[Alex J. Best]

import data.set.basic

variable {X  : Type}
variable set1 : set X
variable nonEmptySetProp : ¬ (set1 = ∅)

example : ∃ a, a ∈ set1 :=
set.ne_empty_iff_nonempty.mp nonEmptySetProp

[Alex J. Best]

As of quite recently set1.nonempty which literally means ∃ a, a ∈ set1 is the preferred way of expressing the sentiment that s \ne \emptyset

[Daniel Keys]

This is exactly what I needed and I just realized I awkwardly posted in a totally unrelated topic. :upside_down:
I'll blame it on the late hour!