I don't know why this stopped working

leanprover-community · Oct 14, 2021 · d90a89f · d90a89f
1 parent 8e3f4f1
commit d90a89f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/normed_group/normed_with_aut.lean b/src/normed_group/normed_with_aut.lean
@@ -33,7 +33,7 @@ begin
   { rw [normed_with_aut.norm_T, inv_mul_cancel_left₀],
     apply ne_of_gt,
     rw nnreal.coe_pos,
-    exact fact.out _ },
+    exact _inst_2.out },
   { rw [← category_theory.comp_apply, T.inv_hom_id], refl }
 end