Lemma placement in this vs other module

Stream: lean4

[Joseph Tooby-Smith]

I have a situation I am confused about. The directory and files I am working with are complicated, and it is unclear how to make a MWE for this, so let me try and explain with a simple example.

I have a file A.lean:

import AModule1

open ANamespace1

namespace thisNameSpace
...
Lots of defs and lemmas.
...

lemma alpha : alpha_statement  := by
    alpha_proof

end thisNameSpace

I have another file B.lean:

import A

open ANamespace1

namespace thisNameSpace

/-- exactly the same as alpha, just a different name --/
lemma alpha' : alpha_statement  := by
    alpha_proof
...
Lots of defs and lemmas.
...

lemma gamma :gamma_statement  := by
    gamma_proof

lemma beta : beta_statement  := by
    rw [alpha]
    rw [gamma] -- error here, but erw [gamma] works.

/-- exactly the same statement as beta. -/
lemma beta' : beta_statement  := by
    rw [alpha']
    rw [gamma] -- no error here.

end thisNameSpace

I would assume alpha and alpha' to be identical and interchangeable. The only difference between them is that one appears at the end of A.lean and the other at the start of B.lean. They are in the same namespaces with the same namespaces opened etc.

However, they have a different effect down the line. Using #check alpha and #check alpha' gives not difference.

I'm on Lean 4.12.0.

Is this expected behaviour?

[Kevin Buzzard]

I can only assume that at some point when you say "exactly the same" you actually mean "not exactly the same but look exactly the same to me". Try set_option pp.all true and take a good look at these exactly the same things and see if they're all still exactly the same.