example vs. theorem

Stream: lean4

[Nir Paz]

Why does this work

import Mathlib.SetTheory.Cardinal.Basic

open Cardinal

example (f : ℕ → A) (hf : Function.Bijective f) : ℵ₀ = #A := by
  rw [← mk_nat]
  exact mk_congr (Equiv.ofBijective _ hf)

but this doesn't?

import Mathlib.SetTheory.Cardinal.Basic

open Cardinal

theorem boof (f : ℕ → A) (hf : Function.Bijective f) : ℵ₀ = #A := by
  rw [← mk_nat] --fails
  exact mk_congr (Equiv.ofBijective _ hf)

A is autoImplicit, and in the theorem it's added as Type u_1 while in the example it's added as ?u.x. It makes sense that this wouldn't work if the universe level of A wasn't specified, so why does the example work? I don't really understand what ?u.x represents here.

[Nir Paz]

Oh, I see now that A changes to be Type after the first line, so I guess in examples the universe levels are set as tbd, and the final thing we are proving is only decided by the proof, but this obviously shouldn't happen for theorems. Is that right?

[Siddhartha Gadgil]

The main difference between example/defs and theorems is that the type of a theorem is fully inferred from the left-hand side alone. In the case of a def or example the types of the lhs and rhs are inferred together if possible to match.

[Kevin Buzzard]

It's concerning to see autoImplicits causing confusion even for people who are aware that autoImplicits exist :-( (I've also been picking up the pieces for this in my course recently, because the people taking it are beginners and I foolishly didn't turn them off project-wide initially).

[Nir Paz]

In my original code I had ℝ but didn't import the reals, which is a problem that's pretty hard to catch (I know it's colored differently but my brain doesn't really see that). Also maybe not the best place to ask, but how can I turn it off for all files in a project?

[Kevin Buzzard]

Just parroting some gobble-de-gook which I don't really understand from the lakefile.lean of my course:

package «formalising-mathematics-2024» where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`pp.proofs.withType, false⟩,
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ]

If it's just for one file then set_option autoImplicit false at the top will do it.

[Mario Carneiro]

this isn't an autoimplicit issue, you get the same behavior if you put {A} at the start of both

[Kevin Buzzard]

But if you wrote {A : Type u} then you wouldn't, right?

[Mario Carneiro]

right