Finding files to import

Stream: new members

[Nathan]

Screenshot 2025-09-23 at 6.31.33 PM.png
I'm working on this proof for practice. I wonder if I can get lemma l1 for free by importing something, but where do I look?

Also, I want to import logic.function.iterate but I get the error unknown module prefix 'logic'. I cloned the mathematics_in_lean repo, but am i supposed to clone a mathlib repo or something?

[Weiyi Wang]

(Tip: it is often better to post the code in text so people can copy it into editors)

[Nathan]

oh yeah, no problem

[Nathan]

import MIL.common

section open Set
  def orbit {α : Type} (σ : Equiv.Perm α) (x : α) :=
    {y | ∃ n : ℕ, y = σ^[n] x ∨ y = (Equiv.symm σ)^[n] x}

  lemma l1 {α : Type} {S : Set α} : S ≠ ∅ → ∃ x, x ∈ S :=
    have h₁ : (¬∃ x, x ∈ S) → S = ∅ :=
      λ h => Subset.antisymm
        (λ hx => λ xss => False.elim (h ⟨hx, xss⟩))
        (λ _ => λ xn => False.elim xn)
    λ h => Or.elim (em (∃ x, x ∈ S))
      (λ ex => ex)
      (λ nex => False.elim (h (h₁ nex)))

  lemma l2 {α : Type} {σ : Equiv.Perm α} {x y z : α}
    (p₁ : x ∈ orbit σ y) (p₂ : y ∈ orbit σ z) : x ∈ orbit σ z :=
    let ⟨n₁, h₁⟩ := p₁; let ⟨n₂, h₂⟩ := p₂
    sorry

  lemma l3 {α : Type} {σ : Equiv.Perm α} {x y : α}
    (p₁ : x ∈ orbit σ y) : y ∈ orbit σ x := sorry

  theorem t1 {α : Type} (σ : Equiv.Perm α) (x y : α) :
    (orbit σ x) ∩ (orbit σ y) ≠ ∅ → (orbit σ x) = (orbit σ y) :=
    λ h => let ⟨_, sox, soy⟩ := l1 h; Subset.antisymm
      (λ _ => λ ox => l2 ox (l2 (l3 sox) soy))
      (λ _ => λ oy => l2 oy (l2 (l3 soy) sox))
end

[Weiyi Wang]

is the Set here the one from Mathlib, or defined in your own project?

[Weiyi Wang]

If this is the one from Mathlib, you can do

• import the whole Mathlib
• use apply? to explore. In this case, I was able to find the proof with three lines

lemma l1 {α : Type} {S : Set α} : S ≠ ∅ → ∃ x, x ∈ S :=by
   intro S; -- sometimes it needs intro to help it to find lemma
   apply? -- found `refine Set.nonempty_def.mp ?_`
   apply? -- found `exact Set.nonempty_iff_ne_empty.mpr s`, finishing the proof

Of course, you can also one-shot this with

lemma l1 {α : Type} {S : Set α} : S ≠ ∅ → ∃ x, x ∈ S := by grind

[Nathan]

I'm not sure, does mathlib come with mathematics_in_lean?

[Aaron Liu]

yes it does

[Nathan]

ohh I see, in order to use logic.function.iterate I needed to open Function

[Nathan]

no import necessary

[Nathan]

can I use Classical.choice?

[Aaron Liu]

what do you mean by that?

[Nathan]

from (orbit σ x) ∩ (orbit σ y) ≠ ∅ i want to obtain an element and the proposition that the element is in (orbit σ x) ∩ (orbit σ y)

[Aaron Liu]

well no one's stopping you from using Classical.choice

[Nathan]

so I was wondering if I could use Classical.choice to do that

[Aaron Liu]

maybe consider also docs#Classical.choose or docs#Exists.choose

[Nathan]

where are the docs for Set.nonempty_def.mp, is that not part of mathlib?

[Aaron Liu]

docs#Set.nonempty_def docs#Iff.mp

[Nathan]

thanks :pray:

[Nathan]

Thanks again folks, I was able to completely remove lemma l1 by using Set.nonempty_def.

[Kenny Lau]

Nathan said:

where are the docs for Set.nonempty_def.mp, is that not part of mathlib?

You need to understand dot notation for this. Basically, it's a way to save a lot of characters when typing and abbreviate stuff.

If a term foo has type FooType and you have another function FooType.bar : FooType -> Nat, then you can write foo.bar and Lean will automatically match FooType to the type of one of the inputs of FooType.bar and figure out what you mean.

Toy example:

def Nat.fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | (n+2) => n.fib + (n+1).fib

def ten : Nat := 10

#eval ten.fib

[Nathan]

I see, it was just the combination of nonempty_def and mp

[Nathan]

I was able to complete this proof - if a permutation is acting on a set, and two orbits share an element, then the orbits are equal as sets. Feel free to offer feedback :thumbs_up:

import MIL.common

section open Set open Function open Equiv
  def orbit {α : Type} (σ : Perm α) (x : α) :=
    {y | ∃ n : ℕ, y = σ^[n] x ∨ y = (σ.symm)^[n] x}

  lemma o_trans {α : Type} {σ : Perm α} {x y z : α}
    (p₁ : x ∈ orbit σ y) (p₂ : y ∈ orbit σ z) : x ∈ orbit σ z :=
    have combine {n₁ n₂ : ℕ} {γ : Perm α} (hxy : x = γ^[n₁] y) (hyz : y = γ^[n₂] z) :
      x = γ^[n₁+n₂] z := by simp[hxy, hyz, iterate_add_apply γ]
    have cancel₁ {n₁ n₂ : ℕ} {γ : Perm α} (hcmp : n₁ ≥ n₂) (hxy : x = γ^[n₁] y)
      (hyz : y = γ.symm^[n₂] z) : x = γ^[n₁-n₂] z := calc
        x = γ^[n₁-n₂+n₂] (γ.symm^[n₂] z)       := by rw[hxy, hyz, Nat.sub_add_cancel hcmp]
        _ = γ^[n₁-n₂] (γ^[n₂] (γ.symm^[n₂] z)) := by rw[iterate_add_apply]
        _ = γ^[n₁-n₂] z                        := by rw[RightInverse.iterate γ.right_inv' n₂]
    have cancel₂ {n₁ n₂ : ℕ} {γ : Perm α} (hcmp : n₂ ≥ n₁) (hxy : x = γ^[n₁] y)
      (hyz : y = γ.symm^[n₂] z) : x = γ.symm^[n₂-n₁] z :=
      have hinv := RightInverse.iterate γ.right_inv' n₁; calc
        x = γ^[n₁] (γ.symm^[n₁+(n₂-n₁)] z) := by rw[hxy, hyz, Nat.add_sub_of_le hcmp]
        _ = γ.symm^[n₂-n₁] z               := by rw[iterate_add_apply, hinv]
    let ⟨n₁, h₁⟩ := p₁; let ⟨n₂, h₂⟩ := p₂; Or.elim h₁
      (λ oxp => Or.elim h₂
        (λ oyp => ⟨n₁+n₂, Or.inl (combine oxp oyp)⟩)
        (λ oyn => Or.elim (le_total n₂ n₁)
          (λ hng => ⟨n₁-n₂, Or.inl (cancel₁ hng oxp oyn)⟩)
          (λ hnl => ⟨n₂-n₁, Or.inr (cancel₂ hnl oxp oyn)⟩)))
      (λ oxn => Or.elim h₂
        (λ oyp => Or.elim (le_total n₁ n₂)
          (λ hng => ⟨n₂-n₁, Or.inl (cancel₂ hng oxn oyp)⟩)
          (λ hnl => ⟨n₁-n₂, Or.inr (cancel₁ hnl oxn oyp)⟩))
        (λ oyn => ⟨n₁+n₂, Or.inr (combine oxn oyn)⟩))

  lemma o_symm {α : Type} {σ : Perm α} {x y : α} (p₁ : x ∈ orbit σ y) : y ∈ orbit σ x :=
    have opp {n : ℕ} {γ : Perm α} (h : x = γ^[n] y) : y = γ.symm^[n] x :=
      by rw [h, LeftInverse.iterate γ.left_inv' n y]
    let ⟨n₁, h⟩ := p₁; Or.elim h
      (λ hh => ⟨n₁, Or.inr (opp hh)⟩)
      (λ hh => ⟨n₁, Or.inl (opp hh)⟩)

  theorem t1 {α : Type} (σ : Perm α) (x y : α) :
    (orbit σ x ∩ orbit σ y).Nonempty → (orbit σ x) = (orbit σ y) :=
    λ h => let ⟨_, sox, soy⟩ := nonempty_def.mp h; Subset.antisymm
      (λ _ => λ ox => o_trans ox (o_trans (o_symm sox) soy))
      (λ _ => λ oy => o_trans oy (o_trans (o_symm soy) sox))
end