Help me check my style in MIL 4.3

Stream: new members

[Linus Tang]

Here are my solutions for the exercises in Mathematics in Lean Section 4.3.
They all pass, but I'd appreciate if someone would help me check my code for style, for example:

• Where I introduce new hypotheses, am I using good names?
• Are there any places where it would be better (for readability, or for my own learning) to write the proof in a different way
  -- For the constructor in 1A, is there a direct proof of the form <something, hx>?
  -- Is it necessary to introduce hxeq' in 2C? Or can(/should) I avoid this by using a tactic that applies a function to both sides of an existing hypothesis?

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import MIL.Common

open Set
open Function

noncomputable section
open Classical
variable {α β : Type*} [Nonempty β]

section
variable (f : α → β) (g : β → α)

def sbAux : ℕ → Set α
  | 0 => univ \ g '' univ
  | n + 1 => g '' (f '' sbAux n)

def sbSet :=
  ⋃ n, sbAux f g n

def sbFun (x : α) : β :=
  if x ∈ sbSet f g then f x else invFun g x

theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
  have : x ∈ g '' univ := by
    contrapose! hx
    rw [sbSet, mem_iUnion]
    use 0
    rw [sbAux, mem_diff]
    -- vvvvvvvv 1A
    constructor
    · trivial
    exact hx
    -- ^^^^^^^^
  have : ∃ y, g y = x := by
     -- vvvvvvvv 1B
    rcases this with ⟨y, hy⟩
    use y
    exact hy.right
    -- ^^^^^^^^
   -- vvvvvvvv 1C
  exact invFun_eq this
  -- ^^^^^^^^


theorem sb_injective (hf : Injective f) : Injective (sbFun f g) := by
  set A := sbSet f g with A_def
  set h := sbFun f g with h_def
  intro x₁ x₂
  intro (hxeq : h x₁ = h x₂)
  show x₁ = x₂
  simp only [h_def, sbFun, ← A_def] at hxeq
  by_cases xA : x₁ ∈ A ∨ x₂ ∈ A
  · wlog x₁A : x₁ ∈ A generalizing x₁ x₂ hxeq xA
    · symm
      apply this hxeq.symm xA.symm (xA.resolve_left x₁A)
    have x₂A : x₂ ∈ A := by
      apply _root_.not_imp_self.mp
      intro (x₂nA : x₂ ∉ A)
      rw [if_pos x₁A, if_neg x₂nA] at hxeq
      rw [A_def, sbSet, mem_iUnion] at x₁A
      have x₂eq : x₂ = g (f x₁) := by
        -- vvvvvvvv 2A
        rw [hxeq, sb_right_inv f g x₂nA]
        -- ^^^^^^^^
      rcases x₁A with ⟨n, hn⟩
      rw [A_def, sbSet, mem_iUnion]
      use n + 1
      simp [sbAux]
      exact ⟨x₁, hn, x₂eq.symm⟩
    -- vvvvvvvv 2B
    simp [x₁A, x₂A] at hxeq
    exact hf hxeq
    -- ^^^^^^^^
  push_neg at xA
  -- vvvvvvvv 2C
  simp [xA] at hxeq
  rcases xA with ⟨xA1, xA2⟩
  have hxeq' : g (invFun g x₁) = g (invFun g x₂) := by
    rw [hxeq]
  rw [sb_right_inv f g xA1, sb_right_inv f g xA2] at hxeq'
  exact hxeq'
  -- ^^^^^^^^








theorem sb_surjective (hg : Injective g) : Surjective (sbFun f g) := by
  set A := sbSet f g with A_def
  set h := sbFun f g with h_def
  intro y
  by_cases gyA : g y ∈ A
  · rw [A_def, sbSet, mem_iUnion] at gyA
    rcases gyA with ⟨n, hn⟩
    rcases n with _ | n
    · simp [sbAux] at hn
    simp [sbAux] at hn
    rcases hn with ⟨x, xmem, hx⟩
    use x
    have : x ∈ A := by
      rw [A_def, sbSet, mem_iUnion]
      exact ⟨n, xmem⟩
    rw [h_def, sbFun, if_pos this]
    apply hg hx
  -- vvvvvvvv 3A
  rw [h_def]
  unfold sbFun
  use g y
  rw [← A_def]
  simp [gyA]
  exact leftInverse_invFun hg y
  -- ^^^^^^^^
end

theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) :
    ∃ h : α → β, Bijective h :=
  ⟨sbFun f g, sb_injective f g hf, sb_surjective f g hg⟩

-- Auxiliary information
section
variable (g : β → α) (x : α)

#check (invFun g : α → β)
#check (leftInverse_invFun : Injective g → LeftInverse (invFun g) g)
#check (leftInverse_invFun : Injective g → ∀ y, invFun g (g y) = y)
#check (invFun_eq : (∃ y, g y = x) → g (invFun g x) = x)

end

[Aaron Liu]

Do you know about docs#Set.range

[Jireh Loreaux]

I don't really want to look through everything, but for some perspective, here's the proof I would give of sb_right_inv

theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
  apply invFun_eq
  contrapose! hx
  apply Set.mem_iUnion_of_mem 0
  apply Set.mem_compl
  simpa

[Jireh Loreaux]

(oh, I redefined sbAux as this:)

def sbAux : ℕ → Set α
  | 0 => (Set.range g)ᶜ
  | n + 1 => (g ∘ f) '' sbAux n

[Jireh Loreaux]

without that, you need to add the line:

  apply Set.mem_diff_of_mem (mem_univ _)

before apply Set.mem_compl.

[Linus Tang]

@Aaron Liu @Jireh Loreaux Thank you, this is helpful!
MIL provided most of the code, so I didn't think about using range to redefine sbAux
But I will go through your code on my own Lean editor to learn from it.

[Jireh Loreaux]

aha, I should have looked at #mil first. I see now where you got much of the structure of your proofs and why you were only looking at certain pieces.

[Jireh Loreaux]

1A: exact ⟨mem_univ _, hx⟩

[Jireh Loreaux]

1B: what you have is fine. I'll note that grind works to prove that have though. :laughing: I understand this may not be conducive to learning necessarily.

[Jireh Loreaux]

2C: You could do simply: rw [← sb_right_inv f g xA1, ← sb_right_inv f g xA2, hxeq] in place of:

  have hxeq' : g (invFun g x₁) = g (invFun g x₂) := by
    rw [hxeq]
  rw [sb_right_inv f g xA1, sb_right_inv f g xA2] at hxeq'
  exact hxeq'

Or alternatively, you could do:

  replace hxeq := congr(g $hxeq)
  rw [sb_right_inv f g xA1, sb_right_inv f g xA2] at hxeq

assuming the congr term elaborator is available at this point in MIL. Otherwise you could do: replace hxeq := congrArg g hxeq.

[Linus Tang]

Thank you, this is helpful!
Ah I think #mil taught me how to apply congr backwards from the goal, not to the hypothesis.