Zulip Chat Archive

Stream: lean4

Topic: How to extract the only element of a set?

aprilgrimoire (Dec 08 2024 at 08:17):

Hi!

def comap_pullback (F : Type) [Field F] (G : Type) [Field G] (f : G →+* F) (H : Subfield F)
    (x : H) (hx : (x : F) ∈ (f '' ⊤)) : (Subfield.comap f H) :=
  let preimage :=  f ⁻¹' {↑x}
  have preimage_nonempty : Set.Nonempty preimage := by
    apply Set.preimage_singleton_nonempty.mpr
    simp only [Set.top_eq_univ, Set.image_univ, Set.mem_range] at hx
    simp only [Set.mem_range]
    exact hx
  by
    apply Set.nonempty_def.mp at preimage_nonempty
    let (y : preimage) := Inhabited.default (self := sorry)

Here I have an injection, and I want to write a function to express the preimage of some element in its image. However, I didn't find any needed tools in the library. For example, there isn't a function to make a Singleton from a set and a proof that there is exact one element in it. How should I do this?

Kim Morrison (Dec 08 2024 at 08:53):

Please post an #mwe.

aprilgrimoire (Dec 08 2024 at 09:00):

Kim Morrison said:

Please post an #mwe.

Sure, thanks. I posted the full definition I was working on to see if I was doing it the wrong way.

Here is a #mwe (or lack thereof):

import Mathlib

def f (α : Type) (A : Set α) (f : ∀ x ∈ A, ∀ y ∈ A, x = y) (g : ∃ (x : α), x ∈ A) : A :=
  sorry

Kevin Buzzard (Dec 08 2024 at 10:00):

g.choose is the element and g.choose_spec is the proof.

aprilgrimoire (Dec 08 2024 at 10:05):

Kevin Buzzard said:

g.choose is the element and g.choose_spec is the proof.

Thanks. I used to use

def f (α : Type) (A : Set α) (f : ∀ x ∈ A, ∀ y ∈ A, x = y) (g : ∃ (x : α), x ∈ A) : A :=
  let ⟨x, hx⟩ := g

However this style sometimes doesn't work:

def comap_pullback (F : Type) [Field F] (G : Type) [Field G] (f : G →+* F) (H : Subfield F)
    (x : H) (hx : (x : F) ∈ (f '' ⊤)) : (Subfield.comap f H) :=
  let preimage :=  f ⁻¹' {↑x}
  have preimage_nonempty : Set.Nonempty preimage := by
    apply Set.preimage_singleton_nonempty.mpr
    simp only [Set.top_eq_univ, Set.image_univ, Set.mem_range] at hx
    simp only [Set.mem_range]
    exact hx
  by
    apply Set.nonempty_def.mp at preimage_nonempty
    let (y : preimage) := Inhabited.default (self := sorry)
    let ⟨x, hx⟩ := preimage_nonempty

Why do I get the tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop error?

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop

F : Type
inst✝¹ : Field F
G : Type
inst✝ : Field G
f : G →+* F
H : Subfield F
x : ↥H
preimage : Set G := ⇑f ⁻¹' {↑x}
motive : (∃ x, x ∈ preimage) → Sort ?u.97844
h_1 : (x : G) → (hx : x ∈ preimage) → motive ⋯
preimage_nonempty✝ : ∃ x, x ∈ preimage
⊢ motive preimage_nonempty✝
 after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil