case w
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑(f ≫
          let_fun this := g;
          this)
      a =
    ↑(f ≫
          let_fun this := h;
          this)
      a
A B : GroupCat
f : A ⟶ B
⊢ (f ≫
      let_fun this := g;
      this) =
    f ≫
      let_fun this := h;
      this
ext a
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑g (↑f a) = ↑h (↑f a)
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑(f ≫
          let_fun this := g;
          this)
      a =
    ↑(f ≫
          let_fun this := h;
          this)
      a
change g (f a) = h (f a)
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
this : ↑f a ∈ {b | ↑h b = ↑g b}
⊢ ↑g (↑f a) = ↑h (↑f a)
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑g (↑f a) = ↑h (↑f a)
have : f a ∈ { b | h b = g b } := by
  rw [←agree]
  use a
no goals
case w
A B : GroupCat
f : A ⟶ B
a : ↑A
this : ↑f a ∈ {b | ↑h b = ↑g b}
⊢ ↑g (↑f a) = ↑h (↑f a)
rw [this]
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ {b | ↑h b = ↑g b}
rw [←agree]
no goals
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
use a