lean-tui 0.0.9

Standalone TUI infoview for Lean 4 theorem prover
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

import Mathlib.Data.Set.Basic
import Paperproof

theorem commutativityOfIntersections
    (s t : Set Nat) : s ∩ t = t ∩ s := by
  ext x
  apply Iff.intro

  intro h1

  rw [Set.mem_inter_iff, and_comm] at h1

  exact h1
  intro h2
  rw [Set.mem_inter_iff, and_comm] at h2

  -- exact h2