Merge pull request #129 from leanprover-community/more_example_updates

leanprover-community · Oct 14, 2022 · 92f188b · 92f188b
2 parents ebb498c + bdb33ea
commit 92f188b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/examples/Ext.lean b/src/examples/Ext.lean
@@ -92,7 +92,7 @@ rfl
 `Ext' 0 (X, Y) ≅ Hom(X,Y)`.
 -/
 example (X Y : 𝓐) : Ext' 0 (op X) Y ≅ AddCommGroup.of (X ⟶ Y) :=
-(Ext'_zero_flip_iso _ _).app _
+(Ext'_zero_flip_iso 𝓐 Y).app (op X)
 
 /-!
 The isomorphism above is functorial in the first variable, and the isomorphism of functors

diff --git a/src/examples/cond.lean b/src/examples/cond.lean
@@ -118,8 +118,8 @@ example
     (π : Π i, X i ⟶ B)
 -- such that `π` is jointly surjective,
     (hπ : ∀ b : B, ∃ i (x : X i), π i x = b)
--- and all families of elements `x i : F (op $ X i)`,
-    (x : Π i, F (op $ X i))
+-- and all families of elements `x i : F (op (X i))`,
+    (x : Π i, F (op (X i)))
 -- which are compatible on pullbacks `X i ×_{B} X j`
     (hx : ∀ i j : α,
       F.map (pullback.fst : pullback (π i) (π j) ⟶ X i).op (x i) =

diff --git a/src/examples/real.lean b/src/examples/real.lean
@@ -32,12 +32,12 @@ rfl
 /-!
 Any conditionally complete linear ordered field is isomorphic (as an ordered ring) to `ℝ`.
 -/
-example {R : Type*} [conditionally_complete_linear_ordered_field R] : R ≃+*o ℝ :=
+example {R : Type} [conditionally_complete_linear_ordered_field R] : R ≃+*o ℝ :=
 default
 
 /-!
 The isomorphism above is unique.
 -/
-example {R : Type*} [conditionally_complete_linear_ordered_field R] (e₁ e₂ : R ≃+*o ℝ) :
+example {R : Type} [conditionally_complete_linear_ordered_field R] (e₁ e₂ : R ≃+*o ℝ) :
   e₁ = e₂ :=
 subsingleton.elim _ _