no goals
α : Type u_1
β : Type u_2
γ : Type ?u.100202
δ : Type ?u.100205
δ' : Type ?u.100208
ι : Sort uι
s t✝ u : Set α
m✝ : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
m : MeasurableSpace α
t : ℕ → Set β
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_disj : Pairwise (Disjoint on t)
g : ℕ → β → α
hg : ∀ (n : ℕ), Measurable (g n)
i j : ℕ
h : (Disjoint on t) i j
⊢ EqOn (g i) (g j) (t i ∩ t j)
simp only [h.inter_eq, eqOn_empty]