What does two dots mean in front of an identifier

Stream: new members

[Lars Ericson]

What does the last line of this mean, in particular the .. in ..induced_outer_measure :

def of_measurable {α} [measurable_space α]
  (m : Π (s : set α), is_measurable s → ennreal)
  (m0 : m ∅ is_measurable.empty = 0)
  (mU : ∀ {{f : ℕ → set α}} (h : ∀i, is_measurable (f i)),
    pairwise (disjoint on f) →
    m (⋃i, f i) (is_measurable.Union h) = (∑'i, m (f i) (h i))) :
  measure α :=
{ m_Union := λ f hf hd,
  show induced_outer_measure m _ m0 (Union f) =
      ∑' i, induced_outer_measure m _ m0 (f i), begin
    rw [induced_outer_measure_eq m0 mU, mU hf hd],
    congr, funext n, rw induced_outer_measure_eq m0 mU
  end,
  trimmed :=
  show (induced_outer_measure m _ m0).trim = induced_outer_measure m _ m0, begin
    unfold outer_measure.trim,
    congr, funext s hs,
    exact induced_outer_measure_eq m0 mU hs
  end,
  ..induced_outer_measure m _ m0 }

[Eric Wieser]

Unpack the fields of the structure to the right of the dots into the containing structure

[Bryan Gin-ge Chen]

This is called the "record update syntax" in 9.2 of TPiL.