Theorem Order

Stream: lean4

[Marcus Rossel]

I have a bug in the egg tactic which I am absolutely mystified by. The detailed reproducible version is that the following MWE 1 works, while MWE 2 fails.

MWE 1

import Egg

class Magma (α : Type _) where
  op : α → α → α

infix:65 " ◇ " => Magma.op

variable (G : Type) [Magma G]

abbrev Equation387 := ∀ (x y : G), x ◇ y = (y ◇ y) ◇ x
abbrev Equation43  := ∀ (x y : G), x ◇ y = y ◇ x

set_option egg.explosion true in
theorem Equation1571_implies_Equation40' (h : ∀ (x y z : G), x = (y ◇ z) ◇ (y ◇ (x ◇ z))) :
    ∀ (x y : G), x ◇ x = y ◇ y := by
  egg [*]

theorem Equation387_implies_Equation43_calc (h : Equation387 G) : Equation43 G := by
  intro x y
  egg calc [*]
    x ◇ y
    _ = (y ◇ y) ◇ x
    _ = (x ◇ x) ◇ (y ◇ y)
    _ = ((y ◇ y) ◇ (y ◇ y)) ◇ (x ◇ x)
    _ = ((y ◇ y) ◇ y) ◇ (x ◇ x)
    _ = (y ◇ y) ◇ (x ◇ x)
    _ = (x ◇ x) ◇ y
    _ = y ◇ x

MWE 2

import Egg

class Magma (α : Type _) where
  op : α → α → α

infix:65 " ◇ " => Magma.op

variable (G : Type) [Magma G]

abbrev Equation387 := ∀ (x y : G), x ◇ y = (y ◇ y) ◇ x
abbrev Equation43  := ∀ (x y : G), x ◇ y = y ◇ x

theorem Equation387_implies_Equation43_calc (h : Equation387 G) : Equation43 G := by
  intro x y
  egg calc [*]
    x ◇ y
    _ = (y ◇ y) ◇ x
    _ = (x ◇ x) ◇ (y ◇ y)
    _ = ((y ◇ y) ◇ (y ◇ y)) ◇ (x ◇ x)
    _ = ((y ◇ y) ◇ y) ◇ (x ◇ x)
    _ = (y ◇ y) ◇ (x ◇ x)
    _ = (x ◇ x) ◇ y
    _ = y ◇ x

set_option egg.explosion true in
theorem Equation1571_implies_Equation40' (h : ∀ (x y z : G), x = (y ◇ z) ◇ (y ◇ (x ◇ z))) :
    ∀ (x y : G), x ◇ x = y ◇ y := by
  egg [*] -- never completes

The more high-level description of the problem is the following: I have two theorems, T1 and T2, which I want to solve using a tactic t. When I state and prove the theorems in the following order

theorem T1 ... := by t ...
theorem T2 ... := by t ...

... everything works as expected. But if I reverse the order to

theorem T2 ... := by t ...
theorem T1 ... := by t ...

... then the call to t in T1 behaves differently and fails to prove the theorem. How is this possible - that is, which kinds of contexts can lead to this difference in behavior?