Some small fixes for latest Lean version. Move set builder to separate file

Author: kaleidawave

.gitignore

@@ -4,4 +4,4 @@
 .lake
 TODO.md
 .vscode
-**/*/private_*.lean
+**/private_*.lean

Mathematics/Algebra/Group.lean

@@ -25,8 +25,8 @@ theorem multiply.associative: ∀ a b c: T, a * (b * c) = (a * b) * c := Group.a
 theorem inv.double : (a⁻¹)⁻¹ = a := by
   rw [←multiply.one (a⁻¹)⁻¹, ←(Group.inverse a).left, Group.associativity, (Group.inverse _).left, one.multiply]
 
-theorem one.inverse : (1⁻¹) = (1: T) := by
-  rw [←multiply.one 1⁻¹, (Group.inverse 1).1]
+theorem one.inverse : (1⁻¹: T) = (1: T) := by
+  rw [←multiply.one (1⁻¹: T), (Group.inverse 1).1]
 
 theorem multiply.eq_one_implies_eq (h : a * b = 1) : a⁻¹ = b := by
   rw [←multiply.one a⁻¹, ←h, Group.associativity, (Group.inverse a).left, one.multiply]

Mathematics/Structures/Set.lean

@@ -37,12 +37,3 @@ def Set.includes (z: Set A) (a: A) : Prop := z a
 
 @[simp, reducible]
 instance { A: Type }: Membership A (Set A) := ⟨fun z a => z a⟩
-
--- syntax (name := emptyset) "s{}" : term
--- syntax (name := set) "s{" term,+ "}" : term
-
--- macro_rules (kind := emptyset) | `(s{}) => `(Set.empty)
-
--- macro_rules (kind := set)
---   | `(s{ $x }) => `(Set.singleton $x)
---   | `(s{ $x, $xs,* }) => `(operators.Set.union (Set.singleton $x) (s{ $[$xs: term],* }))

Mathematics/Structures/Set/Builder.lean

@@ -0,0 +1,13 @@
+import Mathematics.Structures.Set
+import Mathematics.Structures.Set.Operations
+
+syntax (name := emptyset) "s{}" : term
+syntax (name := set) "s{" term,+ "}" : term
+
+macro_rules (kind := emptyset) | `(s{}) => `(Set.empty)
+
+macro_rules (kind := set)
+  | `(s{ $x }) => `(Set.singleton $x)
+  | `(s{ $x, $xs,* }) => `(Set.union (Set.singleton $x) (s{ $[$xs: term],* }))
+
+-- def first_three: Set Nat := s{1, 2, 3}

Mathematics/Structures/Set/Relations.lean

@@ -6,7 +6,6 @@ variable { X: Type }
 -- Non strict
 @[reducible]
 def Set.subset (s₁ s₂: Set X) : Prop := ∀ {a: X}, a ∈ s₁ → a ∈ s₂
--- Non strict
 
 @[reducible]
 def Set.subset.strict (s₁ s₂: Set X) : Prop := s₁ ≠ s₂ ∧ Set.subset s₁ s₂

Mathematics/Structures/Set/Theorems.lean

@@ -19,6 +19,15 @@ theorem singleton.includes (a b: A) : b ∈ Set.singleton a ↔ a = b := by
   intro h1
   exact h1 ▸ singleton.includes.self b
 
+theorem singleton.eq (a b: A) : Set.singleton a = Set.singleton b ↔ a = b := by
+  constructor
+  intro h1
+  rw [Set.extensionality] at h1
+  exact (h1 a).mp (rfl)
+  intro h2
+  ext c
+  rw [h2]
+
 theorem empty.no_members' (a: A): a ∈ Set.empty A → False := by intro h1; contradiction
 
 theorem empty.no_members : ¬(∃a, a ∈ Set.empty A) := fun ⟨a, p⟩ => empty.no_members' a p

README.md

@@ -11,4 +11,3 @@ Mathematics
 ### About
 
 Proofs can definitely be shorter and clearer. (feel free to PR)
-