difference between apply with holes and without

Stream: new members

[Xipan Xiao]

I have two rings and submonoids of them respectively, and a lemma saying "the product of two invertible elements are still invertible", like:

variable (A B : Type*) [CommRing A] [CommRing B]
variable (S : Submonoid A) (T : Submonoid B)

lemma units_mul {a : A} {b : B} (ha : IsUnit a) (hb : IsUnit b) : IsUnit (a, b) :=
  ⟨⟨(a, b), (↑ha.unit⁻¹, ↑hb.unit⁻¹), by simp, by simp⟩, rfl⟩

I tried to apply the lemma providing the two hypothesis it asks:

    have fs_unit : IsUnit (f (s, t)) := IsLocalization.map_units (Localization S) ⟨s, hs⟩
    have gs_unit : IsUnit (g (s, t)) := IsLocalization.map_units (Localization T) ⟨t, ht⟩
    apply units_mul fs_unit gs_unit

and I was told there is a type mismatch

application type mismatch
  units_mul fs_unit
argument
  fs_unit
has type
  IsUnit (f (s, t)) : Prop
but is expected to have type
  Type ?u.13085 : Type (?u.13085 + 1)

Then I changed it to applying the lemma with holes like:

    apply units_mul _ _
    exact fs_unit
    exact gs_unit

And surprisingly this time it worked. What is the difference between these two approaches? The complete code I have for now is also pasted for your reference:

import Mathlib

open Localization

variable (A B : Type*) [CommRing A] [CommRing B]
variable (S : Submonoid A) (T : Submonoid B)

lemma units_mul {a : A} {b : B} (ha : IsUnit a) (hb : IsUnit b) : IsUnit (a, b) :=
  ⟨⟨(a, b), (↑ha.unit⁻¹, ↑hb.unit⁻¹), by simp, by simp⟩, rfl⟩

noncomputable def localizationCommutesWithProduct :
    Localization (S.prod T) ≃ Localization S × Localization T :=
  let f : A × B →+* Localization S := (algebraMap A (Localization S)).comp (RingHom.fst A B)
  let g : A × B →+* Localization T := (algebraMap B (Localization T)).comp (RingHom.snd A B)
  let φ : A × B →+* Localization S × Localization T := RingHom.prod f g

  let hφ : ∀ (a : S.prod T), IsUnit (φ (a : A × B)) := by
    intro ⟨⟨s, t⟩, hs, ht⟩
    have fs_unit : IsUnit (f (s, t)) := IsLocalization.map_units (Localization S) ⟨s, hs⟩
    have gs_unit : IsUnit (g (s, t)) := IsLocalization.map_units (Localization T) ⟨t, ht⟩
    apply units_mul _ _
    exact fs_unit
    exact gs_unit

  sorry

[Aaron Liu]

In the second case what is happening is actually

    refine units_mul (Localization S) (Localization T) ?_ ?_
    exact fs_unit
    exact gs_unit