# Re: [isabelle] Proving cardinality

```Dear John,

```
I can reproduce your problem but do not have an explanation. There is a thread about "using" in the mailing list archives:
```

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00019.html

```
which is interesting, but does not give an explanation for your case (since S is not polymorphic).
```
To make it easier for others to follow, here is the problem again:

definition S :: "nat set" where "S == {1, 2, 3}"
lemma "card S > 1" by (auto simp: S_def) (*this works*)
lemma "card S > 1" using S_def apply auto (*leaves the goal*)
1. S = {Suc 0, 2, 3} ⟹ Suc 0 < card S

cheers

chris

On 07/26/2012 10:06 AM, John Munroe wrote:
```
```I gave it with 'using S_def'. Do you know why 'using S_def; by auto'
wouldn't work?
```
```
```
```On Thu, Jul 26, 2012 at 12:57 AM, Christian Sternagel  wrote:
```
```For me, by (auto simp: S_def) did the job. So how did you give S_def/ax1 as
fact?
```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.