Using theorems that only take implicit arguments

Stream: new members

[Ryan Smith]

I'm trying to convince lean that a group has nonzero cardinality. This should be easy since it has an identity element, but 'should' isn't a proof. There are a couple results which should be able to do this since we have Nonempty G but all of the arguments to these theorems are implicit .

theorem Fintype.card_ne_zero {α : Type u_1}  [Fintype α]  [Nonempty α] :
Fintype.card α ≠ 0

or

theorem Fintype.card_pos_iff {α : Type u_1}  [Fintype α] :
0 < Fintype.card α ↔ Nonempty α

Just struggling with syntax here. We have the hypothesis to show my cardinality is nonzero but how do I pass G to one of these theorems?

[Yaël Dillies]

You don't need to, just rw [Fintype.card_pos_iff] for example

[Ryan Smith]

In this case I need to construct a hypothesis that Nat.card G \ne 0 because the I'm trying to finish my result with

have h2 : z ^ (Nat.card G) = 1 := by sorry
have hnon : 0 < Nat.card G := by sorry
exact Complex.norm_eq_one_of_pow_eq_one h2 (by grind)

So I need to convince Complex.norm_eq_one_of_pow_eq_one that n \ne 0. Is the answer that I need to find a version of the theorem which takes explicit arguments instead to prove hnon?

[Yaël Dillies]

Have you tried using the positivity tactic? Note that Nat.card ℤ = 0, so you will need some extra conditions on G (that it is finite, specifically)

[Ryan Smith]

I've never herd of that tactic. G is finite, but that's really helpful to know about the integers. I guess it makes sense.

positivity offers to prove non-negative but can't do positive here

[Yaël Dillies]

Indeed! It seems that nobody ever got around to making positivity support Nat.card. Would you be interested in learning how to add the support?

[Ryan Smith]

Last night I proved my first lemma which wasn't from a tutorial. It was a marathon effort that I thought would be just two lines. So still climbing the learning curve.

It's frustrating that Fintype has the results I need here but I can't use them

[Yaël Dillies]

Learning Lean is a game of falling into many potholes :sweat_smile:

[Kevin Buzzard]

import Mathlib

example (G : Type*) [Group G] [Finite G] : 0 < Nat.card G := by exact?

works fine.

[Kenny Lau]

Ryan Smith said:

I'm trying to convince lean that a group has nonzero cardinality

a good first step would be to first isolate it out as a separate lemma (this is the philosophy of #mwe, which is not just useful for asking questions), which Kevin has done for you, at which point by exact? works

[Ryan Smith]

I didn't have Finite G in that file since I assumed infinite groups had nonzero cardinality before Yael told me otherwise.

[Matt Diamond]

it's an easy mistake to make

my advice is to make sure you read the docstrings carefully for the functions you're using... docs#Nat.card explicitly notes that it returns 0 for infinite types