From b7f8b57ddfe3c4077a0f36381af2d50702c552e3 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Tue, 12 May 2020 05:17:45 +0000
Subject: [PATCH] Remove a test

---
 tests/lean/123-2.lean              | 48 ------------------------------
 tests/lean/123-2.lean.expected.out | 13 --------
 2 files changed, 61 deletions(-)
 delete mode 100644 tests/lean/123-2.lean
 delete mode 100644 tests/lean/123-2.lean.expected.out

diff --git a/tests/lean/123-2.lean b/tests/lean/123-2.lean
deleted file mode 100644
index d458594303..0000000000
--- a/tests/lean/123-2.lean
+++ /dev/null
@@ -1,48 +0,0 @@
-open function
-
-class has_scalar' (R : Type*) (A : Type*) := (smul : R → A → A)
-
-infixr ` • `:73 := has_scalar'.smul
-
-structure ring_hom' (M : Type*) (N : Type*) [semiring M] [semiring N] :=
-(to_fun : M → N)
-(map_one' : to_fun 1 = 1)
-(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)
-(map_zero' : to_fun 0 = 0)
-(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)
-
-instance (α : Type*) (β : Type*) [semiring α] [semiring β] : has_coe_to_fun (ring_hom' α β) :=
-⟨_, λ f, ring_hom'.to_fun (f)⟩
-
-class algebra' (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
-  extends has_scalar' R A, ring_hom' R A :=
-(commutes' : ∀ r x, to_fun r * x = x * to_fun r)
-(smul_def' : ∀ r x, r • x = to_fun r * x)
-
-def algebra_map' (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra' R A] : ring_hom' R A :=
-algebra'.to_ring_hom'
-
-structure alg_hom' (R : Type*) (A : Type*) (B : Type*)
-  [comm_semiring R] [semiring A] [semiring B] [algebra' R A] [algebra' R B] extends ring_hom' A B :=
-(commutes' : ∀ r : R, to_fun (algebra_map' R A r) = algebra_map' R B r)
-
-variables {R : Type*} {A : Type*} {B : Type*}
-variables [comm_semiring R] [semiring A] [semiring B]
-variables [algebra' R A] [algebra' R B]
-
-instance : has_coe_to_fun (alg_hom' R A B) := ⟨_, λ f, f.to_fun⟩
-
-def quot.lift
-  {R : Type} [comm_ring R]
-  {A : Type} [comm_ring A] [algebra' R A]
-  {B : Type*} [comm_ring B] [algebra' R B]
-  {C : Type} [comm_ring C] [algebra' R C]
-  (f : alg_hom' R A B) (hf : surjective f)
-  (g : alg_hom' R A C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
-  alg_hom' R B C :=
-{ to_fun := λ b, _,
-  map_one' := _,
-  map_mul' := _,
-  map_zero' := _,
-  map_add' := _,
-  commutes' := _ }
diff --git a/tests/lean/123-2.lean.expected.out b/tests/lean/123-2.lean.expected.out
deleted file mode 100644
index 5349aad58c..0000000000
--- a/tests/lean/123-2.lean.expected.out
+++ /dev/null
@@ -1,13 +0,0 @@
-123-2.lean:48:15: error: type mismatch at field 'commutes''
-  ?m_1
-has type
-  ∀ (r : R), (λ (b : B), ?m_1[b] b) (⇑(algebra_map' R B) r) = ⇑(algebra_map' R C) r
-but is expected to have type
-  ∀ (r : R),
-    {to_fun := λ (b : B), ?m_1[b] b,
-       map_one' := ?map_one',
-       map_mul' := ?map_mul',
-       map_zero' := ?map_zero',
-       map_add' := ?map_add'}.to_fun
-        (⇑(algebra_map' R B) r) =
-      ⇑(algebra_map' R C) r