feat(set_theory/ordinal_notation): correctness of ordinal power

algebra/order.lean

@@ -29,7 +29,7 @@ lemma le_of_not_lt [linear_order α] {a b : α} : ¬ a < b → b ≤ a := not_lt
 @[simp] lemma not_le [linear_order α] {a b : α} : ¬ a ≤ b ↔ b < a := (lt_iff_not_ge b a).symm
 
 lemma lt_or_le [linear_order α] : ∀ a b : α, a < b ∨ b ≤ a := lt_or_ge
-lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ a > b := le_or_gt
+lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ b < a := le_or_gt
 
 lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
 not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl

data/pnat.lean

@@ -17,6 +17,8 @@ def to_pnat (n : ℕ) (h : n > 0 . exact_dec_trivial) : ℕ+ := ⟨n, h⟩
 
 def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩
 
+@[simp] theorem succ_pnat_coe (n : ℕ) : (succ_pnat n : ℕ) = succ n := rfl
+
 def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)
 
 end nat
@@ -26,17 +28,34 @@ instance coe_nat_pnat : has_coe ℕ ℕ+ := ⟨nat.to_pnat'⟩
 namespace pnat
 
 open nat
+@[simp] theorem pos (n : ℕ+) : (n : ℕ) > 0 := n.2
+
+theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq
 
-instance : has_one ℕ+ := ⟨succ_pnat 0⟩
+@[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl
 
-instance : has_add ℕ+ := ⟨λ m n, ⟨m.1 + n.1, add_pos m.2 n.2⟩⟩
+instance : has_add ℕ+ := ⟨λ m n, ⟨m + n, add_pos m.2 n.2⟩⟩
 
-instance : has_mul ℕ+ := ⟨λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩⟩
+@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl
 
-@[simp] theorem ne_zero (n : ℕ+) : n.1 ≠ 0 := ne_of_gt n.2
+@[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := ne_of_gt n.2
 
-@[simp] theorem to_pnat'_val {n : ℕ} : n > 0 → n.to_pnat'.val = n := succ_pred_eq_of_pos
-@[simp] theorem nat_coe_val  {n : ℕ} : n > 0 → (n : ℕ+).val = n := succ_pred_eq_of_pos
+@[simp] theorem nat_coe_coe  {n : ℕ} : n > 0 → ((n : ℕ+) : ℕ) = n := succ_pred_eq_of_pos
 @[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
 
+instance : comm_monoid ℕ+ :=
+{ mul       := λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩,
+  mul_assoc := λ a b c, subtype.eq (mul_assoc _ _ _),
+  one       := succ_pnat 0,
+  one_mul   := λ a, subtype.eq (one_mul _),
+  mul_one   := λ a, subtype.eq (mul_one _),
+  mul_comm  := λ a b, subtype.eq (mul_comm _ _) }
+
+@[simp] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl
+
+@[simp] theorem mul_coe (m n : ℕ+) : ((m * n : ℕ+) : ℕ) = m * n := rfl
+
+@[simp] def pow (m : ℕ+) (n : ℕ) : ℕ+ :=
+⟨nat.pow m n, nat.pos_pow_of_pos _ m.pos⟩
+
 end pnat

logic/basic.lean

@@ -31,6 +31,12 @@ instance : decidable_eq empty := λa, a.elim
   {α} [subsingleton α] : decidable_eq α
 | a b := is_true (subsingleton.elim a b)
 
+/- Add an instance to "undo" coercion transitivity into a chain of coercions, because
+   most simp lemmas are stated with respect to simple coercions and will not match when
+   part of a chain. -/
+@[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]
+  (a : α) : (a : γ) = (a : β) := rfl
+
 end miscellany
 
 /-