to_additive thinks it's in a namespace

Stream: mathlib4

[Heather Macbeth]

The following to_additive issue is showing up in mathlib4#608: error

The declaration mul_eq_one_iff' depends on the declaration mul_eq_one_iff'.match_1 which is in the namespace mul_eq_one_iff', but does not have the `@[to_additive]` attribute. This is not supported.
Workaround: move mul_eq_one_iff'.match_1 to a different namespace.

on the first of the following examples, and similar on the second if you comment the first (for some reason they interfere with each other so you can't get the same error on both simultaneously).

import Mathlib.Algebra.Group.Defs

variable [MulOneClass α]

@[to_additive]
theorem mul_eq_one_iff' {a b : α} :
    a * b = 1 ↔ a = 1 ∧ b = 1 :=
  Iff.intro sorry
    fun ⟨ha', hb'⟩ => by rw [ha', hb', mul_one]

@[to_additive]
theorem mul_eq_one_of_eq_one' {a b : α} :
    a = 1 ∧ b = 1 → a * b = 1 := by
  intro ⟨ha', hb'⟩
  rw [ha', hb', mul_one]

[Heather Macbeth]

The problem seems to be something like: to_additive thinks it's in a namespace when it's taking apart a composite term like a = 1 ∧ b = 1 using fun ⟨ha', hb'⟩ or intro ⟨ha', hb'⟩.

[Heather Macbeth]

cross-reference: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20and.20iffs.20with.20Exists