grind が関数等式を上手く扱えないという例 / 関数等式を fully applied な形に直せば通る例

import Lean.LibrarySuggestions.Default

variable {A B : Type}

variable {C : Type}
variable {f : B → C} {g : A → B}

open Function

/-- If the composition is surjective, then so is the outer function. -/
theorem surj_of_comp_surj (h : Surjective (f ∘ g)) : Surjective f := by
  dsimp [Surjective] at *
  intro c
  have ⟨a, ha⟩ := h c
  exists g a

/-- If the composition is injective, then the inner function is injective. -/
theorem inj_of_comp_inj (h : Injective (f ∘ g)) : Injective g := by
  dsimp [Injective] at *
  intro a₁ a₂ g_eq
  replace h := @h a₁ a₂
  apply h
  congr 1

/-- モノ射 -/
@[grind]
def mono (f : A → B) : Prop :=
  ∀ C : Type, ∀ g₁ g₂ : C → A, f ∘ g₁ = f ∘ g₂ → g₁ = g₂

/-- An injective function is a monomorphism -/
theorem mono_of_inj {f : A → B} (h : Injective f) : mono f := by
  intro C g₁ g₂ g_eq
  ext c
  suffices f (g₁ c) = f (g₂ c) from by
    grind
  calc
    _ = (f ∘ g₁) c := rfl
    _ = (f ∘ g₂) c := by rw [g_eq]
    _ = f (g₂ c) := rfl

/-- A monomorphism is injective -/
theorem inj_of_mono {f : A → B} (h : mono f) : Injective f := by
  intro a₁ a₂ f_eq
  dsimp [mono] at h
  let C := Fin 2
  let g₁ : C → A := fun _ => a₁
  let g₂ : C → A := fun _ => a₂
  replace h := h C g₁ g₂
  grind

/-- Epimorphism -/
@[grind]
def epi (f : A → B) := ∀ C : Type, ∀ g₁ g₂ : B → C, g₁ ∘ f = g₂ ∘ f → g₁ = g₂

/-- A surjective function is an epimorphism -/
theorem epi_of_surj {f : A → B} (h : Surjective f) : epi f := by
  intro C g₁ g₂ g_eq
  dsimp [Surjective] at h
  ext b
  obtain ⟨a, ha⟩ := h b
  rw [← ha]
  -- Why does `grind` not succeed here?
  fail_if_success grind
  calc
    _ = (g₁ ∘ f) a := rfl
    _ = (g₂ ∘ f) a := by rw [g_eq]
    _ = g₂ (f a) := rfl

Start by running the complete snippet with Lean.LibrarySuggestions.Default and reproduce the fail_if_success grind case in epi_of_surj. Compare that case with the earlier composition examples and the fully applied form mentioned in the title. Done means explaining the differing grind behavior and resolving the reported example.